diff options
Diffstat (limited to 'Test/hofs')
| -rw-r--r-- | Test/hofs/Apply.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/hofs/Classes.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/hofs/Field.dfy.expect | 8 | ||||
| -rw-r--r-- | Test/hofs/FnRef.dfy.expect | 8 | ||||
| -rw-r--r-- | Test/hofs/Frame.dfy.expect | 14 | ||||
| -rw-r--r-- | Test/hofs/Lambda.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/hofs/LambdaParsefail.dfy.expect | 10 | ||||
| -rw-r--r-- | Test/hofs/LambdaParsefail2.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/hofs/Naked.dfy.expect | 24 | ||||
| -rw-r--r-- | Test/hofs/OneShot.dfy.expect | 6 | ||||
| -rw-r--r-- | Test/hofs/ReadsReads.dfy.expect | 16 | ||||
| -rw-r--r-- | Test/hofs/Simple.dfy.expect | 12 | ||||
| -rw-r--r-- | Test/hofs/Twice.dfy.expect | 4 |
13 files changed, 56 insertions, 56 deletions
diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect index 77d34c4c..0a923143 100644 --- a/Test/hofs/Apply.dfy.expect +++ b/Test/hofs/Apply.dfy.expect @@ -1,4 +1,4 @@ -Apply.dfy(27,16): Error: assertion violation
+Apply.dfy(27,15): Error: assertion violation
Execution trace:
(0,0): anon0
Apply.dfy(26,27): anon15_Else
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 1c9e31f0..a5b33522 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,7 +1,7 @@ -Classes.dfy(64,12): Error: assertion violation
+Classes.dfy(64,11): Error: assertion violation
Execution trace:
(0,0): anon0
-Classes.dfy(40,6): Error: possible violation of function precondition
+Classes.dfy(40,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon7_Else
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect index 9f6998f5..0859d83c 100644 --- a/Test/hofs/Field.dfy.expect +++ b/Test/hofs/Field.dfy.expect @@ -1,13 +1,13 @@ -Field.dfy(12,12): Error: possible violation of function precondition
+Field.dfy(12,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(12,15): Error: assertion violation
+Field.dfy(12,14): Error: assertion violation
Execution trace:
(0,0): anon0
-Field.dfy(21,12): Error: possible violation of function precondition
+Field.dfy(21,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,14): Error: assertion violation
+Field.dfy(21,13): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect index 0f6f2aa9..e665c830 100644 --- a/Test/hofs/FnRef.dfy.expect +++ b/Test/hofs/FnRef.dfy.expect @@ -1,19 +1,19 @@ -FnRef.dfy(17,45): Error: possible violation of function precondition
+FnRef.dfy(17,44): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
FnRef.dfy(15,12): anon5_Else
(0,0): anon6_Then
-FnRef.dfy(32,8): Error: possible violation of function precondition
+FnRef.dfy(32,7): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
FnRef.dfy(26,12): anon9_Else
FnRef.dfy(28,8): anon10_Else
-FnRef.dfy(46,12): Error: assertion violation
+FnRef.dfy(46,11): Error: assertion violation
Execution trace:
(0,0): anon0
FnRef.dfy(43,12): anon7_Else
(0,0): anon9_Then
-FnRef.dfy(65,14): Error: assertion violation
+FnRef.dfy(65,13): Error: assertion violation
Execution trace:
(0,0): anon0
FnRef.dfy(56,12): anon8_Else
diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect index 0ee2eadb..9964deb4 100644 --- a/Test/hofs/Frame.dfy.expect +++ b/Test/hofs/Frame.dfy.expect @@ -1,35 +1,35 @@ -Frame.dfy(23,16): Error: assertion violation
+Frame.dfy(23,15): Error: assertion violation
Execution trace:
(0,0): anon0
Frame.dfy(19,12): anon5_Else
(0,0): anon6_Then
-Frame.dfy(37,14): Error: assertion violation
+Frame.dfy(37,13): Error: assertion violation
Execution trace:
(0,0): anon0
Frame.dfy(33,12): anon3_Else
-Frame.dfy(63,23): Error: assertion violation
+Frame.dfy(63,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon13_Then
Frame.dfy(55,12): anon14_Else
(0,0): anon15_Then
(0,0): anon5
-Frame.dfy(66,19): Error: insufficient reads clause to read array element
+Frame.dfy(66,18): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon16_Then
(0,0): anon17_Then
-Frame.dfy(68,28): Error: insufficient reads clause to read array element
+Frame.dfy(68,27): Error: insufficient reads clause to read array element
Execution trace:
(0,0): anon0
(0,0): anon16_Else
(0,0): anon18_Then
-Frame.dfy(123,14): Error: possible violation of function precondition
+Frame.dfy(123,13): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Else
-Frame.dfy(123,19): Error: assertion violation
+Frame.dfy(123,18): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect index 4fe8275f..ab57fbe0 100644 --- a/Test/hofs/Lambda.dfy.expect +++ b/Test/hofs/Lambda.dfy.expect @@ -1,4 +1,4 @@ -Lambda.dfy(24,12): Error: assertion violation
+Lambda.dfy(24,11): Error: assertion violation
Execution trace:
(0,0): anon0
Lambda.dfy(6,24): anon31_Else
diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect index 11deb9b0..a72fc978 100644 --- a/Test/hofs/LambdaParsefail.dfy.expect +++ b/Test/hofs/LambdaParsefail.dfy.expect @@ -1,6 +1,6 @@ -LambdaParsefail.dfy(5,19): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(6,19): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(7,21): error: this symbol not expected in VarDeclStatement
-LambdaParsefail.dfy(8,15): error: cannot declare identifier beginning with underscore
-LambdaParsefail.dfy(9,17): error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(5,18): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(6,18): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(7,20): Error: this symbol not expected in VarDeclStatement
+LambdaParsefail.dfy(8,14): Error: cannot declare identifier beginning with underscore
+LambdaParsefail.dfy(9,16): Error: this symbol not expected in VarDeclStatement
5 parse errors detected in LambdaParsefail.dfy
diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect index 0c9ecb83..1a6a65dc 100644 --- a/Test/hofs/LambdaParsefail2.dfy.expect +++ b/Test/hofs/LambdaParsefail2.dfy.expect @@ -1,2 +1,2 @@ -LambdaParsefail2.dfy(6,39): error: invalid LambdaArrow
+LambdaParsefail2.dfy(6,38): Error: invalid LambdaArrow
1 parse errors detected in LambdaParsefail2.dfy
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect index 514952a1..9794478d 100644 --- a/Test/hofs/Naked.dfy.expect +++ b/Test/hofs/Naked.dfy.expect @@ -1,45 +1,45 @@ -Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(9,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Else
(0,0): anon11_Then
-Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(12,7): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon10_Else
(0,0): anon11_Else
-Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(17,52): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
-Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(22,12): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(26,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(30,45): Error: possible violation of function precondition
-Naked.dfy(32,14): Related location
+Naked.dfy(30,44): Error: possible violation of function precondition
+Naked.dfy(32,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(32,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(38,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(38,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(42,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(42,9): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause
+Naked.dfy(45,29): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+Naked.dfy(48,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect index 91b931b8..0b4a2bb8 100644 --- a/Test/hofs/OneShot.dfy.expect +++ b/Test/hofs/OneShot.dfy.expect @@ -1,16 +1,16 @@ -OneShot.dfy(20,12): Error: possible violation of function precondition
+OneShot.dfy(20,11): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
OneShot.dfy(13,8): anon5_Else
(0,0): anon6_Then
-OneShot.dfy(22,12): Error: assertion violation
+OneShot.dfy(22,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
OneShot.dfy(13,8): anon5_Else
(0,0): anon6_Else
-OneShot.dfy(22,13): Error: possible violation of function precondition
+OneShot.dfy(22,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon5_Then
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index cd013630..0a374c44 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -1,33 +1,33 @@ -ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(31,6): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(36,4): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(47,11): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function
+ReadsReads.dfy(58,6): Error: insufficient reads clause to invoke function
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-ReadsReads.dfy(87,50): Error: assertion violation
+ReadsReads.dfy(87,49): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon16_Then
-ReadsReads.dfy(89,29): Error: assertion violation
+ReadsReads.dfy(89,28): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon18_Then
-ReadsReads.dfy(99,37): Error: assertion violation
+ReadsReads.dfy(99,36): Error: assertion violation
Execution trace:
(0,0): anon0
ReadsReads.dfy(96,14): anon15_Else
(0,0): anon19_Then
-ReadsReads.dfy(101,29): Error: assertion violation
+ReadsReads.dfy(101,28): Error: assertion violation
Execution trace:
(0,0): anon0
ReadsReads.dfy(96,14): anon15_Else
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect index e2f16ef3..c0123c80 100644 --- a/Test/hofs/Simple.dfy.expect +++ b/Test/hofs/Simple.dfy.expect @@ -1,26 +1,26 @@ -Simple.dfy(14,10): Error: possible division by zero
+Simple.dfy(14,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(27,10): Error: possible division by zero
+Simple.dfy(27,9): Error: possible division by zero
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Then
-Simple.dfy(37,9): Error: possible violation of function precondition
+Simple.dfy(37,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
Simple.dfy(35,13): anon5_Else
-Simple.dfy(49,9): Error: possible violation of function precondition
+Simple.dfy(49,8): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-Simple.dfy(61,10): Error: possible violation of function precondition
+Simple.dfy(61,9): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Simple.dfy(73,10): Error: assertion violation
+Simple.dfy(73,9): Error: assertion violation
Execution trace:
(0,0): anon0
Simple.dfy(72,38): anon5_Else
diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect index 2476b945..0ce2450c 100644 --- a/Test/hofs/Twice.dfy.expect +++ b/Test/hofs/Twice.dfy.expect @@ -1,8 +1,8 @@ -Twice.dfy(27,22): Error: assertion violation
+Twice.dfy(27,21): Error: assertion violation
Execution trace:
(0,0): anon0
Twice.dfy(23,12): anon3_Else
-Twice.dfy(35,32): Error: possible violation of function precondition
+Twice.dfy(35,31): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
(0,0): anon10_Else
|