1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
-------------------- Snapshots0.dfy --------------------
Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
>>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
>>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
>>> MarkAsPartiallyVerified
Snapshots0.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 2 verified, 1 error
-------------------- Snapshots1.dfy --------------------
Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Processing command (at Snapshots1.v0.dfy(12,3)) assert true;
>>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Snapshots1.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 3 verified, 1 error
-------------------- Snapshots2.dfy --------------------
Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(14,11)) assert true;
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
>>> DoNothingToAssert
Dafny program verifier finished with 6 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
>>> added after: a##post##0 := a##post##0 && false;
Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
Snapshots2.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
>>> DoNothingToAssert
Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Dafny program verifier finished with 5 verified, 1 error
-------------------- Snapshots3.dfy --------------------
Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);
>>> DoNothingToAssert
Snapshots3.v0.dfy(9,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
Dafny program verifier finished with 1 verified, 1 error
Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);
>>> DoNothingToAssert
Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);
>>> RecycleError
Snapshots3.v0.dfy(9,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
Dafny program verifier finished with 1 verified, 1 error
-------------------- Snapshots4.dfy --------------------
Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);
>>> DoNothingToAssert
Dafny program verifier finished with 2 verified, 0 errors
Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);
>>> DoNothingToAssert
Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);
>>> MarkAsFullyVerified
Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);
>>> DoNothingToAssert
Snapshots4.v1.dfy(5,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
Snapshots4.v1.dfy(10,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
Dafny program verifier finished with 1 verified, 2 errors
-------------------- Snapshots5.dfy --------------------
Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> DoNothingToAssert
Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;
>>> MarkAsFullyVerified
Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;
>>> DoNothingToAssert
Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;
>>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
-------------------- Snapshots6.dfy --------------------
Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);
>>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);
>>> DoNothingToAssert
Snapshots6.v1.dfy(20,14): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 3 verified, 1 error
-------------------- Snapshots7.dfy --------------------
Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);
>>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);
>>> DoNothingToAssert
Snapshots7.v1.dfy(19,14): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 3 verified, 1 error
|
