summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/aitest0/Answer38
-rw-r--r--Test/aitest0/Intervals.bpl19
-rw-r--r--Test/aitest0/runtest.bat1
-rw-r--r--Test/aitest1/Answer140
-rw-r--r--Test/dafny0/Answer28
5 files changed, 110 insertions, 116 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 58750460..e517aa18 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -18,34 +18,34 @@ implementation Join(b: bool)
var z: int;
start:
- assume true;
+ assume {:inferred} true;
GlobalFlag := true;
x := 3;
y := 4;
z := x + y;
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
goto Then, Else;
Then:
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
assume b <==> true;
x := x + 1;
- assume x == 4 && y == 4 && z == 7;
+ assume {:inferred} x == 4 && y == 4 && z == 7;
goto join;
Else:
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
assume b <==> false;
y := 4;
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
goto join;
join:
- assume y == 4 && z == 7;
+ assume {:inferred} y == 4 && z == 7;
assert y == 4;
assert z == 7;
assert GlobalFlag <==> true;
- assume y == 4 && z == 7;
+ assume {:inferred} y == 4 && z == 7;
return;
}
@@ -61,27 +61,27 @@ implementation Loop()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
c := 0;
i := 0;
- assume c == 0 && i == 0;
+ assume {:inferred} c == 0 && i == 0;
goto test;
test: // cut point
- assume c == 0;
- assume c == 0;
+ assume {:inferred} c == 0;
+ assume {:inferred} c == 0;
goto Then, Else;
Then:
- assume c == 0;
+ assume {:inferred} c == 0;
assume i < 10;
i := i + 1;
- assume c == 0;
+ assume {:inferred} c == 0;
goto test;
Else:
- assume c == 0;
- assume c == 0;
+ assume {:inferred} c == 0;
+ assume {:inferred} c == 0;
return;
}
@@ -96,16 +96,18 @@ implementation Evaluate()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume i == 465;
+ assume {:inferred} i == 465;
return;
}
Boogie program verifier finished with 0 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
new file mode 100644
index 00000000..49d27b1c
--- /dev/null
+++ b/Test/aitest0/Intervals.bpl
@@ -0,0 +1,19 @@
+const N: int;
+axiom 0 <= N;
+
+procedure P(K: int)
+ requires 0 <= K;
+{
+ var b: bool, x, k: int;
+
+ if (!b) {
+ b := !b;
+ }
+ x := if b then 13 else 10;
+ k := K;
+ while (k != 0) {
+ x := x + k;
+ k := k - 1;
+ }
+ assert 13 <= x;
+}
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index a4c12d8d..1cb7a60c 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -4,3 +4,4 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl
+%BGEXE% %* -infer:j Intervals.bpl
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index ca9ff22a..718e7171 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -8,27 +8,27 @@ implementation SimpleLoop()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 0;
- assume i == 0;
+ assume {:inferred} i == 0;
goto test;
test: // cut point
- assume 0 <= i;
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i;
goto Then, Else;
Then:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume i < 10;
i := i + 1;
- assume i <= 10 && 1 <= i;
+ assume {:inferred} i <= 10 && 1 <= i;
goto test;
Else:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume !(i < 10);
- assume 10 <= i;
+ assume {:inferred} 10 <= i;
return;
}
@@ -43,27 +43,27 @@ implementation VariableBoundLoop(n: int)
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 0;
- assume i == 0;
+ assume {:inferred} i == 0;
goto test;
test: // cut point
- assume 0 <= i;
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i;
goto Then, Else;
Then:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume i < n;
i := i + 1;
- assume i <= n && 1 <= i;
+ assume {:inferred} i <= n && 1 <= i;
goto test;
Else:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume !(i < n);
- assume n <= i && 0 <= i;
+ assume {:inferred} n <= i && 0 <= i;
return;
}
@@ -78,12 +78,12 @@ implementation Foo()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume true;
+ assume {:inferred} true;
return;
}
@@ -98,13 +98,13 @@ implementation FooToo()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume 1 / 3 * i == 155;
+ assume {:inferred} 1 / 3 * i == 155;
return;
}
@@ -119,13 +119,13 @@ implementation FooTooStepByStep()
var i: int;
L0:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume 1 / 3 * i == 155;
+ assume {:inferred} 1 / 3 * i == 155;
return;
}
@@ -145,8 +145,8 @@ implementation p()
{
start:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -166,9 +166,9 @@ implementation p()
{
start:
- assume true;
+ assume {:inferred} true;
assume x * x == y;
- assume true;
+ assume {:inferred} true;
return;
}
@@ -188,9 +188,9 @@ implementation p()
{
start:
- assume true;
- assume x == 8;
+ assume {:inferred} true;
assume x == 8;
+ assume {:inferred} x == 8;
return;
}
@@ -210,9 +210,9 @@ implementation p()
{
start:
- assume true;
+ assume {:inferred} true;
assume x < y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
return;
}
@@ -233,20 +233,20 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
assume x < y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
goto B, C;
B:
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
x := x * x;
- assume true;
+ assume {:inferred} true;
return;
C:
- assume x + 1 <= y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
return;
}
@@ -267,32 +267,32 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
assume 0 - 1 <= x;
- assume -1 <= x;
+ assume {:inferred} -1 <= x;
goto B, E;
B:
- assume -1 <= x;
+ assume {:inferred} -1 <= x;
assume x < y;
- assume x + 1 <= y && -1 <= x;
+ assume {:inferred} x + 1 <= y && -1 <= x;
goto C, E;
C:
- assume x + 1 <= y && -1 <= x;
+ assume {:inferred} x + 1 <= y && -1 <= x;
x := x * x;
- assume 0 <= y;
+ assume {:inferred} 0 <= y;
goto D, E;
D:
- assume 0 <= y;
+ assume {:inferred} 0 <= y;
x := y;
- assume x == y && 0 <= y;
+ assume {:inferred} x == y && 0 <= y;
return;
E:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -315,26 +315,26 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
x := 8;
- assume x == 8;
+ assume {:inferred} x == 8;
goto B, C;
B:
- assume x == 8;
+ assume {:inferred} x == 8;
x := 9;
- assume x == 9;
+ assume {:inferred} x == 9;
goto D;
C:
- assume x == 8;
+ assume {:inferred} x == 8;
x := 10;
- assume x == 10;
+ assume {:inferred} x == 10;
goto D;
D:
- assume 9 <= x && x <= 10;
- assume 9 <= x && x <= 10;
+ assume {:inferred} 9 <= x && x <= 10;
+ assume {:inferred} 9 <= x && x <= 10;
return;
}
@@ -356,25 +356,25 @@ implementation p()
{
A:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
goto B, C;
B:
- assume true;
- assume x <= 0;
+ assume {:inferred} true;
assume x <= 0;
+ assume {:inferred} x <= 0;
goto D;
C:
- assume true;
- assume y <= 0;
+ assume {:inferred} true;
assume y <= 0;
+ assume {:inferred} y <= 0;
goto D;
D:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -393,7 +393,7 @@ implementation foo()
var n: int;
A:
- assume true;
+ assume {:inferred} true;
n := 0;
j := 0;
i := j + 1;
@@ -402,7 +402,7 @@ implementation foo()
i := i + 1;
i := i + 1;
j := j + 1;
- assume i == j + 4 && j == 1 && n == 0;
+ assume {:inferred} i == j + 4 && j == 1 && n == 0;
return;
}
@@ -421,24 +421,24 @@ implementation foo()
var n: int;
entry:
- assume true;
+ assume {:inferred} true;
assume n >= 4;
i := 0;
j := i + 1;
- assume j == i + 1 && i == 0 && 4 <= n;
+ assume {:inferred} j == i + 1 && i == 0 && 4 <= n;
goto exit, loop0;
loop0: // cut point
- assume 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} 4 <= n && 0 <= i && j == i + 1;
assume j <= n;
i := i + 1;
j := j + 1;
- assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
+ assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
goto loop0, exit;
exit:
- assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
- assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
return;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..aab1990d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -307,7 +307,6 @@ Execution trace:
(0,0): anon0
Definedness.dfy(105,15): Error: possible division by zero
Execution trace:
- (0,0): anon0
Definedness.dfy(105,5): anon8_LoopHead
(0,0): anon8_LoopBody
Definedness.dfy(105,5): anon9_Else
@@ -799,13 +798,11 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
@@ -821,20 +818,17 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -842,7 +836,6 @@ Execution trace:
ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon81_Then
(0,0): anon38
(0,0): after_9
@@ -856,13 +849,11 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon68_Then
(0,0): after_5
(0,0): anon87_Then
@@ -876,20 +867,17 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -897,7 +885,6 @@ Execution trace:
ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon82_Then
(0,0): anon85_Then
(0,0): after_8
@@ -915,7 +902,6 @@ Execution trace:
Termination.dfy(105,3): anon8_Else
(0,0): anon3
Termination.dfy(105,3): anon9_Else
- (0,0): anon5
Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
@@ -925,7 +911,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(113,3): anon12_Else
- (0,0): anon7
Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
@@ -935,7 +920,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
@@ -945,7 +929,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
@@ -959,7 +942,6 @@ Execution trace:
Termination.dfy(291,3): anon11_Else
Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
- (0,0): anon8
Dafny program verifier finished with 45 verified, 6 errors
@@ -1131,7 +1113,6 @@ Execution trace:
TypeParameters.dfy(153,3): anon22_Else
(0,0): anon13
TypeParameters.dfy(153,3): anon24_Else
- (0,0): anon15
Dafny program verifier finished with 35 verified, 5 errors
@@ -1224,7 +1205,6 @@ Execution trace:
LoopModifies.dfy(14,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(14,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1233,7 +1213,6 @@ Execution trace:
LoopModifies.dfy(42,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(42,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1242,7 +1221,6 @@ Execution trace:
LoopModifies.dfy(57,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(57,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
Execution trace:
(0,0): anon0
@@ -1254,7 +1232,6 @@ Execution trace:
LoopModifies.dfy(90,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(90,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1263,13 +1240,11 @@ Execution trace:
LoopModifies.dfy(134,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(134,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(139,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(139,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(139,7): anon24_Else
- (0,0): anon14
LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1278,7 +1253,6 @@ Execution trace:
LoopModifies.dfy(193,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(193,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1287,13 +1261,11 @@ Execution trace:
LoopModifies.dfy(273,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(273,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(281,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(281,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(281,7): anon24_Else
- (0,0): anon14
Dafny program verifier finished with 23 verified, 9 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 13:57:07 +0000