mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Update expected test output.
Some error messages changed due to the new definition in Cryptol.cry.
This commit is contained in:
parent
d1883caa6a
commit
869deb1354
@ -791,7 +791,7 @@ Here are Cryptol's responses:
|
||||
[]
|
||||
invalid sequence index: 12
|
||||
-- Backtrace --
|
||||
(Cryptol::@) called at Cryptol:870:14--870:20
|
||||
(Cryptol::@) called at Cryptol:875:14--875:20
|
||||
(Cryptol::@@) called at <interactive>:9:1--9:28
|
||||
[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
|
||||
9
|
||||
|
@ -4,15 +4,15 @@ Loading module Main
|
||||
|
||||
[error] at T146.cry:1:18--6:10:
|
||||
The type ?a is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: fv`828
|
||||
It cannot depend on quantified variables: fv`829
|
||||
When checking type of field 'v0'
|
||||
where
|
||||
?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
|
||||
fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
fv`829 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
[error] at T146.cry:5:19--5:24:
|
||||
The type ?b is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: fv`828
|
||||
It cannot depend on quantified variables: fv`829
|
||||
When checking signature variable 'fv'
|
||||
where
|
||||
?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
|
||||
fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
|
||||
fv`829 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:11:
|
||||
Illegal kind assigned to type variable: f`825
|
||||
Illegal kind assigned to type variable: f`826
|
||||
Unexpected: # -> *
|
||||
where
|
||||
f`825 is signature variable 'f' at issue1024a.cry:1:12--1:24
|
||||
f`826 is signature variable 'f' at issue1024a.cry:1:12--1:24
|
||||
[error] at issue1024a.cry:2:6--2:13:
|
||||
Illegal kind assigned to type variable: f`826
|
||||
Illegal kind assigned to type variable: f`827
|
||||
Unexpected: Prop
|
||||
where
|
||||
f`826 is signature variable 'f' at issue1024a.cry:2:14--2:24
|
||||
f`827 is signature variable 'f' at issue1024a.cry:2:14--2:24
|
||||
[error] at issue1024a.cry:4:13--4:49:
|
||||
Illegal kind assigned to type variable: f`828
|
||||
Illegal kind assigned to type variable: f`829
|
||||
Unexpected: # -> *
|
||||
where
|
||||
f`828 is signature variable 'f' at issue1024a.cry:4:22--4:32
|
||||
f`829 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:1040:13--1040:18
|
||||
Cryptol::error called at Cryptol:1045:13--1045:18
|
||||
Cryptol::undefined called at issue103.icry:1:9--1:18
|
||||
Using exhaustive testing.
|
||||
Testing... ERROR for the following inputs:
|
||||
|
@ -207,6 +207,7 @@ Symbols
|
||||
tail : {n, a} [1 + n]a -> [n]a
|
||||
take : {front, back, a} [front + back]a -> [front]a
|
||||
toInteger : {a} (Integral a) => a -> Integer
|
||||
toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer
|
||||
trace : {n, a, b} (fin n) => String n -> a -> b -> b
|
||||
traceVal : {n, a} (fin n) => String n -> a -> a
|
||||
transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
|
||||
|
@ -4,9 +4,9 @@ Loading module Main
|
||||
|
||||
[error] at issue290v2.cry:2:1--2:19:
|
||||
Unsolved constraints:
|
||||
• n`825 == 1
|
||||
• n`826 == 1
|
||||
arising from
|
||||
checking a pattern: type of 1st argument of Main::minMax
|
||||
at issue290v2.cry:2:8--2:11
|
||||
where
|
||||
n`825 is signature variable 'n' at issue290v2.cry:1:11--1:12
|
||||
n`826 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`825
|
||||
• k == n`826
|
||||
arising from
|
||||
matching types
|
||||
at issue723.cry:7:17--7:19
|
||||
where
|
||||
n`825 is signature variable 'n' at issue723.cry:1:6--1:7
|
||||
n`826 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:894:11--894:17, update)
|
||||
(at Cryptol:899:11--899: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:1048:41--1048:46
|
||||
Cryptol::error called at Cryptol:1053:41--1053:46
|
||||
Cryptol::assert called at safety.icry:3:14--3:20
|
||||
<interactive>::it called at safety.icry:3:7--3:37
|
||||
Counterexample
|
||||
|
@ -83,19 +83,19 @@ Loading module Main
|
||||
|
||||
[error] at tc-errors-5.cry:2:5--2:7:
|
||||
Inferred type is not sufficiently polymorphic.
|
||||
Quantified variable: a`825
|
||||
Quantified variable: a`826
|
||||
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`825 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
|
||||
a`826 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:7--4:8:
|
||||
The type ?a is not sufficiently polymorphic.
|
||||
It cannot depend on quantified variables: b`829
|
||||
It cannot depend on quantified variables: b`830
|
||||
When checking the type of 'g'
|
||||
where
|
||||
?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
|
||||
b`829 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
|
||||
b`830 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
|
||||
|
Loading…
Reference in New Issue
Block a user