diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
commit | e67c951ad9c5c637e36a6f025ba3d6e3ad945416 (patch) | |
tree | 0cfb5c339602e4bdebf4bf97f3f0ccc3923c14d1 /Test/hofs/Naked.dfy.expect | |
parent | 000aa762e1fee4b9bd83ec3d7c8b61fd203e2c9d (diff) | |
parent | df5c5f547990c1f80ab7594a1f9287ee03a61754 (diff) |
Merge commit 'df5c5f5'
Diffstat (limited to 'Test/hofs/Naked.dfy.expect')
-rw-r--r-- | Test/hofs/Naked.dfy.expect | 48 |
1 files changed, 22 insertions, 26 deletions
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect index 62c035b2..9794478d 100644 --- a/Test/hofs/Naked.dfy.expect +++ b/Test/hofs/Naked.dfy.expect @@ -1,50 +1,46 @@ -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): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
-Naked.dfy(12,8): 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
(0,0): anon9_Else
-Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+ (0,0): anon10_Else
+ (0,0): anon11_Then
+Naked.dfy(12,7): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
- (0,0): anon5_Else
- (0,0): anon6_Else
-Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+ (0,0): anon9_Else
+ (0,0): anon10_Else
+ (0,0): anon11_Else
+Naked.dfy(17,52): 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.
+ (0,0): anon7_Else
+ (0,0): anon8_Else
+Naked.dfy(22,12): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause
+Naked.dfy(26,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
- (0,0): anon3_Else
-Naked.dfy(29,30): 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): anon3_Else
-Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+ (0,0): anon4_Else
+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): anon3_Else
-Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
+ (0,0): anon4_Else
+Naked.dfy(48,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 1 verified, 12 errors
+Dafny program verifier finished with 2 verified, 11 errors
|