mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-19 09:57:53 +03:00
Update expected stdout for test cases
This commit is contained in:
parent
01d8c1d32f
commit
f825abd2e1
@ -4,7 +4,7 @@ Loading module Main
|
||||
Loading dynamic library ffi-runtime-errors.so
|
||||
|
||||
numeric type argument to foreign function is too large: 18446744073709551616
|
||||
in type parameter n`899 of function Main::f
|
||||
in type parameter n`902 of function Main::f
|
||||
type arguments must fit in a C `size_t`
|
||||
-- Backtrace --
|
||||
Main::f called at ffi-runtime-errors.icry:4:1--4:2
|
||||
|
@ -35,23 +35,23 @@ Loading module Main
|
||||
When checking the type of 'Main::badFloatSizes'
|
||||
[error] at ffi-type-errors.cry:5:9--6:59:
|
||||
Type unsupported for FFI:
|
||||
[n`969] -> [n`969]([16], [16]) -> [n`969][4][8]{a : [n`969],
|
||||
[n`972] -> [n`972]([16], [16]) -> [n`972][4][8]{a : [n`972],
|
||||
b : [2]}
|
||||
Due to:
|
||||
Type unsupported for FFI:
|
||||
[n`969]
|
||||
[n`972]
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of
|
||||
(possibly multidimensional) sequences
|
||||
Type unsupported for FFI:
|
||||
[n`969]([16], [16])
|
||||
[n`972]([16], [16])
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of
|
||||
(possibly multidimensional) sequences
|
||||
Type unsupported for FFI:
|
||||
[n`969][4][8]{a : [n`969], b : [2]}
|
||||
[n`972][4][8]{a : [n`972], b : [2]}
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of
|
||||
@ -65,7 +65,7 @@ Loading module Main
|
||||
When checking the type of 'Main::notFunction'
|
||||
[error] at ffi-type-errors.cry:8:9--8:32:
|
||||
Kind of type variable unsupported for FFI:
|
||||
t`970 : *
|
||||
t`973 : *
|
||||
Only type variables of kind # are supported
|
||||
When checking the type of 'Main::badKind'
|
||||
[error] at ffi-type-errors.cry:9:9--9:43:
|
||||
|
@ -4,15 +4,15 @@ Loading module Main
|
||||
|
||||
[error] at T146.cry:11:10--11:12:
|
||||
The type ?b is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: fv`902
|
||||
It cannot depend on quantified variables: fv`905
|
||||
When checking signature variable 'fv'
|
||||
where
|
||||
?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
|
||||
fv`902 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
[error] at T146.cry:12:11--12:21:
|
||||
The type ?a is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: fv`902
|
||||
It cannot depend on quantified variables: fv`905
|
||||
When checking type of field 'v0'
|
||||
where
|
||||
?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
|
||||
fv`902 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
fv`905 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
|
@ -13,20 +13,20 @@ Loading module Main
|
||||
Unused name: g
|
||||
|
||||
[error] at issue1024a.cry:1:6--1:24:
|
||||
Illegal kind assigned to type variable: f`899
|
||||
Unexpected: # -> *
|
||||
where
|
||||
f`899 is signature variable 'f' at issue1024a.cry:1:13--1:14
|
||||
[error] at issue1024a.cry:2:6--2:24:
|
||||
Illegal kind assigned to type variable: f`900
|
||||
Unexpected: Prop
|
||||
where
|
||||
f`900 is signature variable 'f' at issue1024a.cry:2:15--2:16
|
||||
[error] at issue1024a.cry:4:13--4:49:
|
||||
Illegal kind assigned to type variable: f`902
|
||||
Unexpected: # -> *
|
||||
where
|
||||
f`902 is signature variable 'f' at issue1024a.cry:4:22--4:32
|
||||
f`902 is signature variable 'f' at issue1024a.cry:1:13--1:14
|
||||
[error] at issue1024a.cry:2:6--2:24:
|
||||
Illegal kind assigned to type variable: f`903
|
||||
Unexpected: Prop
|
||||
where
|
||||
f`903 is signature variable 'f' at issue1024a.cry:2:15--2:16
|
||||
[error] at issue1024a.cry:4:13--4:49:
|
||||
Illegal kind assigned to type variable: f`905
|
||||
Unexpected: # -> *
|
||||
where
|
||||
f`905 is signature variable 'f' at issue1024a.cry:4:22--4:32
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
0xffff
|
||||
|
@ -2,7 +2,7 @@ Loading module Cryptol
|
||||
|
||||
Run-time error: undefined
|
||||
-- Backtrace --
|
||||
Cryptol::error called at Cryptol:1043:13--1043:18
|
||||
Cryptol::error called at Cryptol:1062:13--1062:18
|
||||
Cryptol::undefined called at issue103.icry:1:9--1:18
|
||||
Using exhaustive testing.
|
||||
Testing... ERROR for the following inputs:
|
||||
|
@ -84,6 +84,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -84,6 +84,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -95,6 +95,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -97,6 +97,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -109,6 +109,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -65,6 +65,15 @@ Primitive Types
|
||||
Z : # -> *
|
||||
Zero : * -> Prop
|
||||
|
||||
Nominal Types
|
||||
=============
|
||||
|
||||
From Cryptol
|
||||
------------
|
||||
|
||||
enum Option a
|
||||
enum Result t e
|
||||
|
||||
Symbols
|
||||
=======
|
||||
|
||||
|
@ -17,9 +17,9 @@ Loading module Main
|
||||
at issue290v2.cry:2:1--2:19
|
||||
[error] at issue290v2.cry:2:8--2:11:
|
||||
Unsolved constraints:
|
||||
• n`899 == 1
|
||||
• n`902 == 1
|
||||
arising from
|
||||
checking a pattern: type of 1st argument of Main::minMax
|
||||
at issue290v2.cry:2:8--2:11
|
||||
where
|
||||
n`899 is signature variable 'n' at issue290v2.cry:1:11--1:12
|
||||
n`902 is signature variable 'n' at issue290v2.cry:1:11--1:12
|
||||
|
@ -10,9 +10,9 @@ Loading module Main
|
||||
assuming
|
||||
• fin k
|
||||
the following constraints hold:
|
||||
• k == n`899
|
||||
• k == n`902
|
||||
arising from
|
||||
matching types
|
||||
at issue723.cry:7:17--7:19
|
||||
where
|
||||
n`899 is signature variable 'n' at issue723.cry:1:6--1:7
|
||||
n`902 is signature variable 'n' at issue723.cry:1:6--1:7
|
||||
|
@ -5,5 +5,5 @@ Loading module T16::B
|
||||
|
||||
[error] at T16/B.cry:5:5--5:11
|
||||
Multiple definitions for symbol: update
|
||||
(at Cryptol:909:11--909:17, update)
|
||||
(at Cryptol:928:11--928:17, update)
|
||||
(at ./T16/A.cry:3:1--3:7, T16::A::update)
|
||||
|
@ -3,7 +3,7 @@ Counterexample
|
||||
(\x -> assert x "asdf" "asdf") False ~> ERROR
|
||||
Run-time error: asdf
|
||||
-- Backtrace --
|
||||
Cryptol::error called at Cryptol:1051:41--1051:46
|
||||
Cryptol::error called at Cryptol:1070:41--1070:46
|
||||
Cryptol::assert called at safety.icry:3:14--3:20
|
||||
<interactive>::it called at safety.icry:3:7--3:37
|
||||
Counterexample
|
||||
|
@ -84,19 +84,19 @@ Loading module Main
|
||||
|
||||
[error] at tc-errors-5.cry:2:1--2:7:
|
||||
Inferred type is not sufficiently polymorphic.
|
||||
Quantified variable: a`899
|
||||
Quantified variable: a`902
|
||||
cannot match type: [0]?a
|
||||
When checking the type of 'Main::f'
|
||||
where
|
||||
?a is type of sequence member at tc-errors-5.cry:2:5--2:7
|
||||
a`899 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
|
||||
a`902 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
[error] at tc-errors-6.cry:4:3--4:8:
|
||||
The type ?a is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: b`903
|
||||
It cannot depend on quantified variables: b`906
|
||||
When checking the type of 'g'
|
||||
where
|
||||
?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
|
||||
b`903 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
|
||||
b`906 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
|
||||
|
Loading…
Reference in New Issue
Block a user