summaryrefslogtreecommitdiff
path: root/Test/dafny0/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Answer')
-rw-r--r--Test/dafny0/Answer136
1 files changed, 133 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index efcfa8bb..d997cba1 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -403,6 +403,22 @@ Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -422,7 +438,9 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc
ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-20 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(252,2): Error: duplicate label
+38 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -597,8 +615,120 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-
-Dafny program verifier finished with 15 verified, 6 errors
+ControlStructures.dfy(218,18): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ (0,0): anon74_Then
+ (0,0): anon29
+ControlStructures.dfy(235,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon81_Then
+ (0,0): anon38
+ (0,0): after_9
+ (0,0): anon86_Then
+ (0,0): anon53
+ControlStructures.dfy(238,30): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon68_Then
+ (0,0): after_5
+ (0,0): anon87_Then
+ (0,0): anon88_Then
+ (0,0): anon58
+ControlStructures.dfy(241,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon82_Then
+ (0,0): anon85_Then
+ (0,0): after_8
+ (0,0): anon89_Then
+ (0,0): anon61
+
+Dafny program verifier finished with 18 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 00:18:04 +0000