From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Test/aitest1/Answer | 510 +++++++++++++++++++++++++++++++++++++++++++++++ Test/aitest1/Bound.bpl | 28 +++ Test/aitest1/Linear0.bpl | 10 + Test/aitest1/Linear1.bpl | 11 + Test/aitest1/Linear2.bpl | 11 + Test/aitest1/Linear3.bpl | 11 + Test/aitest1/Linear4.bpl | 15 ++ Test/aitest1/Linear5.bpl | 21 ++ Test/aitest1/Linear6.bpl | 21 ++ Test/aitest1/Linear7.bpl | 19 ++ Test/aitest1/Linear8.bpl | 42 ++++ Test/aitest1/Linear9.bpl | 29 +++ Test/aitest1/Output | 510 +++++++++++++++++++++++++++++++++++++++++++++++ Test/aitest1/ineq.bpl | 81 ++++++++ Test/aitest1/runtest.bat | 17 ++ 15 files changed, 1336 insertions(+) create mode 100644 Test/aitest1/Answer create mode 100644 Test/aitest1/Bound.bpl create mode 100644 Test/aitest1/Linear0.bpl create mode 100644 Test/aitest1/Linear1.bpl create mode 100644 Test/aitest1/Linear2.bpl create mode 100644 Test/aitest1/Linear3.bpl create mode 100644 Test/aitest1/Linear4.bpl create mode 100644 Test/aitest1/Linear5.bpl create mode 100644 Test/aitest1/Linear6.bpl create mode 100644 Test/aitest1/Linear7.bpl create mode 100644 Test/aitest1/Linear8.bpl create mode 100644 Test/aitest1/Linear9.bpl create mode 100644 Test/aitest1/Output create mode 100644 Test/aitest1/ineq.bpl create mode 100644 Test/aitest1/runtest.bat (limited to 'Test/aitest1') diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer new file mode 100644 index 00000000..4e5c8f27 --- /dev/null +++ b/Test/aitest1/Answer @@ -0,0 +1,510 @@ +-------------------- ineq.bpl -------------------- +procedure SimpleLoop(); + + + +implementation SimpleLoop() +{ + var i: int; + + start: + assume true; + i := 0; + assume i == 0; + goto test; + + test: // cut point + assume 0 <= i; + assume 0 <= i; + goto Then, Else; + + Then: + assume 0 <= i; + assume i < 10; + i := i + 1; + assume i <= 10 && 1 <= i; + goto test; + + Else: + assume 0 <= i; + assume !(i < 10); + assume 10 <= i; + return; +} + + + +procedure VariableBoundLoop(n: int); + + + +implementation VariableBoundLoop(n: int) +{ + var i: int; + + start: + assume true; + i := 0; + assume i == 0; + goto test; + + test: // cut point + assume 0 <= i; + assume 0 <= i; + goto Then, Else; + + Then: + assume 0 <= i; + assume i < n; + i := i + 1; + assume i <= n && 1 <= i; + goto test; + + Else: + assume 0 <= i; + assume !(i < n); + assume n <= i && 0 <= i; + return; +} + + + +procedure Foo(); + + + +implementation Foo() +{ + var i: int; + + start: + assume true; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume true; + return; +} + + + +procedure FooToo(); + + + +implementation FooToo() +{ + var i: int; + + start: + assume true; + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume 1 / 3 * i == 155; + return; +} + + + +procedure FooTooStepByStep(); + + + +implementation FooTooStepByStep() +{ + var i: int; + + L0: + assume true; + i := 5; + assume i == 5; + goto L1; + + L1: + assume i == 5; + i := 3 * i + 1; + assume i == 16; + goto L2; + + L2: + assume i == 16; + i := 3 * (i + 1); + assume 1 / 3 * i == 17; + goto L3; + + L3: + assume 1 / 3 * i == 17; + i := 1 + 3 * i; + assume i == 154; + goto L4; + + L4: + assume i == 154; + i := (i + 1) * 3; + assume 1 / 3 * i == 155; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear0.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear1.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x * x == y; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear2.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x == 8; + assume x == 8; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear3.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x < y; + assume x + 1 <= y; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear4.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + assume x < y; + assume x + 1 <= y; + goto B; + + B: + assume x + 1 <= y; + x := x * x; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear5.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + assume 0 - 1 <= x; + assume -1 <= x; + goto B; + + B: + assume -1 <= x; + assume x < y; + assume x + 1 <= y && -1 <= x; + goto C; + + C: + assume x + 1 <= y && -1 <= x; + x := x * x; + assume 0 <= y; + goto D; + + D: + assume 0 <= y; + x := y; + assume x == y && 0 <= y; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear6.bpl -------------------- +var x: int; + +var y: int; + +var z: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + x := 8; + assume x == 8; + goto B, C; + + B: + assume x == 8; + x := 9; + assume x == 9; + goto D; + + C: + assume x == 8; + x := 10; + assume x == 10; + goto D; + + D: + assume 9 <= x && x <= 10; + assume 9 <= x && x <= 10; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear7.bpl -------------------- +var x: int; + +var y: int; + +var z: int; + +procedure p(); + + + +implementation p() +{ + + A: + assume true; + assume true; + goto B, C; + + B: + assume true; + assume x <= 0; + assume x <= 0; + goto D; + + C: + assume true; + assume y <= 0; + assume y <= 0; + goto D; + + D: + assume true; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear8.bpl -------------------- +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + A: + assume true; + n := 0; + assume n == 0; + goto B; + + B: + assume n == 0; + j := 0; + assume j == 0 && n == 0; + goto C; + + C: + assume j == 0 && n == 0; + i := j + 1; + assume i == j + 1 && j == 0 && n == 0; + goto D; + + D: + assume i == j + 1 && j == 0 && n == 0; + i := i + 1; + assume i == j + 2 && j == 0 && n == 0; + goto E; + + E: + assume i == j + 2 && j == 0 && n == 0; + i := i + 1; + assume i == j + 3 && j == 0 && n == 0; + goto F; + + F: + assume i == j + 3 && j == 0 && n == 0; + i := i + 1; + assume i == j + 4 && j == 0 && n == 0; + goto G; + + G: + assume i == j + 4 && j == 0 && n == 0; + i := i + 1; + assume i == j + 5 && j == 0 && n == 0; + goto H; + + H: + assume i == j + 5 && j == 0 && n == 0; + j := j + 1; + assume i == j + 4 && j == 1 && n == 0; + goto I; + + I: + assume i == j + 4 && j == 1 && n == 0; + assume i == j + 4 && j == 1 && n == 0; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear9.bpl -------------------- +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + entry: + assume true; + assume n >= 4; + i := 0; + j := i + 1; + assume j == i + 1 && i == 0 && 4 <= n; + goto exit, loop0; + + loop0: // cut point + assume 4 <= n && 0 <= i && j == i + 1; + assume j <= n; + assume j <= n && 4 <= n && 0 <= i && j == i + 1; + goto loop1; + + loop1: + assume j <= n && 4 <= n && 0 <= i && j == i + 1; + i := i + 1; + assume 1 <= i && j == i && j <= n && 4 <= n; + goto loop2; + + loop2: + assume j <= n && 4 <= n && 1 <= i && j == i; + j := j + 1; + assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i; + 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; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Bound.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl new file mode 100644 index 00000000..02b2c460 --- /dev/null +++ b/Test/aitest1/Bound.bpl @@ -0,0 +1,28 @@ +const TEST: name; + +procedure P() +{ +var i: int; +var N: int; + +start: + assume N >= 0; + i := 0; + assert i <= N; + goto LoopHead; + +LoopHead: + goto LoopBody, AfterLoop; + +LoopBody: + assume i < N; + i := i + 1; + goto LoopHead; + +AfterLoop: + assume !(i < N); + assert i == N; + return; +} + +type name; \ No newline at end of file diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl new file mode 100644 index 00000000..7a11c803 --- /dev/null +++ b/Test/aitest1/Linear0.bpl @@ -0,0 +1,10 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() +{ + start: + return; +} diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl new file mode 100644 index 00000000..0cbb4a07 --- /dev/null +++ b/Test/aitest1/Linear1.bpl @@ -0,0 +1,11 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() +{ + start: + assume x*x == y; // not a linear condition + return; +} diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl new file mode 100644 index 00000000..9e02c9e2 --- /dev/null +++ b/Test/aitest1/Linear2.bpl @@ -0,0 +1,11 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() +{ + start: + assume x == 8; + return; +} diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl new file mode 100644 index 00000000..c6b7a441 --- /dev/null +++ b/Test/aitest1/Linear3.bpl @@ -0,0 +1,11 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() +{ + start: + assume x < y; + return; +} diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl new file mode 100644 index 00000000..c8c4605c --- /dev/null +++ b/Test/aitest1/Linear4.bpl @@ -0,0 +1,15 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() + modifies x; +{ + A: + assume x < y; + goto B; + B: + x := x*x; + return; +} diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl new file mode 100644 index 00000000..4f04999c --- /dev/null +++ b/Test/aitest1/Linear5.bpl @@ -0,0 +1,21 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; + +procedure p() + modifies x; +{ + A: + assume -1 <= x; + goto B; + B: + assume x < y; + goto C; + C: + x := x*x; + goto D; + D: + x := y; + return; +} diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl new file mode 100644 index 00000000..83e52a9a --- /dev/null +++ b/Test/aitest1/Linear6.bpl @@ -0,0 +1,21 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; +var z: int; + +procedure p() + modifies x; +{ +A: + x := 8; + goto B, C; +B: + x := 9; + goto D; +C: + x := 10; + goto D; +D: + return; +} diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl new file mode 100644 index 00000000..b1bcaaaf --- /dev/null +++ b/Test/aitest1/Linear7.bpl @@ -0,0 +1,19 @@ +// Simple test file for checking the inference of linear constraints. + +var x: int; +var y: int; +var z: int; + +procedure p() +{ +A: + goto B, C; +B: + assume x <= 0; + goto D; +C: + assume y <= 0; + goto D; +D: + return; +} diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl new file mode 100644 index 00000000..4bc3f887 --- /dev/null +++ b/Test/aitest1/Linear8.bpl @@ -0,0 +1,42 @@ + +procedure foo () returns () +{ + var i: int; + var j: int; + var n: int; + +A: // true + n := 0; + goto B; + +B: // n = 0 + j := 0; + goto C; + +C: // n = 0 AND j = 0 + i := j + 1; + goto D; + +D: // n = 0 AND j = 0 AND i = j + 1 + i := i + 1; + goto E; + +E: // n = 0 AND j = 0 AND i = j + 2 + i := i + 1; + goto F; + +F: // n = 0 AND j = 0 AND i = j + 3 + i := i + 1; + goto G; + +G: // n = 0 AND j = 0 AND i = j + 4 + i := i + 1; + goto H; + +H: // n = 0 AND j = 0 AND i = j + 1 + j := j + 1; + goto I; + +I: // n = 0 AND j = 1 AND i = j + 4 + return; +} diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl new file mode 100644 index 00000000..e48a7a0c --- /dev/null +++ b/Test/aitest1/Linear9.bpl @@ -0,0 +1,29 @@ +procedure foo () returns () +{ + var i: int; + var j: int; + var n: int; +entry: + assume n >= 4; + i := 0; + j := i + 1; + // n >= 4 AND i = 0 AND j = i+1 + goto exit, loop0; + +loop0: + // n >= 4 AND i >= 0 AND j = i+1 + assume j <= n; + goto loop1; +loop1: + // n >= 4 AND i >= 0 AND j = i+1 AND j <= n + i := i + 1; + goto loop2; +loop2: + j := j + 1; + // n >= 4 AND i >= 1 AND j = i+1 AND j <= n+1 + goto loop0, exit; + +exit: + // n >= 4 AND i >= 0 AND j = i+1 AND j <= n+1 + return; +} diff --git a/Test/aitest1/Output b/Test/aitest1/Output new file mode 100644 index 00000000..4e5c8f27 --- /dev/null +++ b/Test/aitest1/Output @@ -0,0 +1,510 @@ +-------------------- ineq.bpl -------------------- +procedure SimpleLoop(); + + + +implementation SimpleLoop() +{ + var i: int; + + start: + assume true; + i := 0; + assume i == 0; + goto test; + + test: // cut point + assume 0 <= i; + assume 0 <= i; + goto Then, Else; + + Then: + assume 0 <= i; + assume i < 10; + i := i + 1; + assume i <= 10 && 1 <= i; + goto test; + + Else: + assume 0 <= i; + assume !(i < 10); + assume 10 <= i; + return; +} + + + +procedure VariableBoundLoop(n: int); + + + +implementation VariableBoundLoop(n: int) +{ + var i: int; + + start: + assume true; + i := 0; + assume i == 0; + goto test; + + test: // cut point + assume 0 <= i; + assume 0 <= i; + goto Then, Else; + + Then: + assume 0 <= i; + assume i < n; + i := i + 1; + assume i <= n && 1 <= i; + goto test; + + Else: + assume 0 <= i; + assume !(i < n); + assume n <= i && 0 <= i; + return; +} + + + +procedure Foo(); + + + +implementation Foo() +{ + var i: int; + + start: + assume true; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume true; + return; +} + + + +procedure FooToo(); + + + +implementation FooToo() +{ + var i: int; + + start: + assume true; + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume 1 / 3 * i == 155; + return; +} + + + +procedure FooTooStepByStep(); + + + +implementation FooTooStepByStep() +{ + var i: int; + + L0: + assume true; + i := 5; + assume i == 5; + goto L1; + + L1: + assume i == 5; + i := 3 * i + 1; + assume i == 16; + goto L2; + + L2: + assume i == 16; + i := 3 * (i + 1); + assume 1 / 3 * i == 17; + goto L3; + + L3: + assume 1 / 3 * i == 17; + i := 1 + 3 * i; + assume i == 154; + goto L4; + + L4: + assume i == 154; + i := (i + 1) * 3; + assume 1 / 3 * i == 155; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear0.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear1.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x * x == y; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear2.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x == 8; + assume x == 8; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear3.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume true; + assume x < y; + assume x + 1 <= y; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear4.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + assume x < y; + assume x + 1 <= y; + goto B; + + B: + assume x + 1 <= y; + x := x * x; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear5.bpl -------------------- +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + assume 0 - 1 <= x; + assume -1 <= x; + goto B; + + B: + assume -1 <= x; + assume x < y; + assume x + 1 <= y && -1 <= x; + goto C; + + C: + assume x + 1 <= y && -1 <= x; + x := x * x; + assume 0 <= y; + goto D; + + D: + assume 0 <= y; + x := y; + assume x == y && 0 <= y; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear6.bpl -------------------- +var x: int; + +var y: int; + +var z: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume true; + x := 8; + assume x == 8; + goto B, C; + + B: + assume x == 8; + x := 9; + assume x == 9; + goto D; + + C: + assume x == 8; + x := 10; + assume x == 10; + goto D; + + D: + assume 9 <= x && x <= 10; + assume 9 <= x && x <= 10; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear7.bpl -------------------- +var x: int; + +var y: int; + +var z: int; + +procedure p(); + + + +implementation p() +{ + + A: + assume true; + assume true; + goto B, C; + + B: + assume true; + assume x <= 0; + assume x <= 0; + goto D; + + C: + assume true; + assume y <= 0; + assume y <= 0; + goto D; + + D: + assume true; + assume true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear8.bpl -------------------- +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + A: + assume true; + n := 0; + assume n == 0; + goto B; + + B: + assume n == 0; + j := 0; + assume j == 0 && n == 0; + goto C; + + C: + assume j == 0 && n == 0; + i := j + 1; + assume i == j + 1 && j == 0 && n == 0; + goto D; + + D: + assume i == j + 1 && j == 0 && n == 0; + i := i + 1; + assume i == j + 2 && j == 0 && n == 0; + goto E; + + E: + assume i == j + 2 && j == 0 && n == 0; + i := i + 1; + assume i == j + 3 && j == 0 && n == 0; + goto F; + + F: + assume i == j + 3 && j == 0 && n == 0; + i := i + 1; + assume i == j + 4 && j == 0 && n == 0; + goto G; + + G: + assume i == j + 4 && j == 0 && n == 0; + i := i + 1; + assume i == j + 5 && j == 0 && n == 0; + goto H; + + H: + assume i == j + 5 && j == 0 && n == 0; + j := j + 1; + assume i == j + 4 && j == 1 && n == 0; + goto I; + + I: + assume i == j + 4 && j == 1 && n == 0; + assume i == j + 4 && j == 1 && n == 0; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Linear9.bpl -------------------- +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + entry: + assume true; + assume n >= 4; + i := 0; + j := i + 1; + assume j == i + 1 && i == 0 && 4 <= n; + goto exit, loop0; + + loop0: // cut point + assume 4 <= n && 0 <= i && j == i + 1; + assume j <= n; + assume j <= n && 4 <= n && 0 <= i && j == i + 1; + goto loop1; + + loop1: + assume j <= n && 4 <= n && 0 <= i && j == i + 1; + i := i + 1; + assume 1 <= i && j == i && j <= n && 4 <= n; + goto loop2; + + loop2: + assume j <= n && 4 <= n && 1 <= i && j == i; + j := j + 1; + assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i; + 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; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors +-------------------- Bound.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl new file mode 100644 index 00000000..a417aaf3 --- /dev/null +++ b/Test/aitest1/ineq.bpl @@ -0,0 +1,81 @@ +// Test the polyhedra domain for linear inequalities + + +procedure SimpleLoop () +{ + var i : int; + + start: + i := 0; + goto test; + + test: + goto Then, Else; + + Then: + assume i < 10; + i := i + 1; + goto test; + + Else: + assume ! (i < 10); + return; +} + + +procedure VariableBoundLoop (n : int) +{ + var i : int; + + start: + i := 0; + goto test; + + test: + goto Then, Else; + + Then: + assume i < n; + i := i + 1; + goto test; + + Else: + assume ! (i < n); + return; +} + +procedure Foo () +{ + var i : int; + + start: + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3 ; + return; +} + +procedure FooToo () +{ + var i : int; + + start: + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3 ; + return; +} + +procedure FooTooStepByStep () +{ + var i : int; + + L0: i := 5; goto L1; + L1: i := 3 * i + 1; goto L2; + L2: i := 3 * (i + 1); goto L3; + L3: i := 1 + 3 * i; goto L4; + L4: i := (i + 1) * 3; return; +} diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat new file mode 100644 index 00000000..f2a4d3e5 --- /dev/null +++ b/Test/aitest1/runtest.bat @@ -0,0 +1,17 @@ +@echo off +setlocal + +set BGEXE=..\..\Binaries\Boogie.exe + +for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl + Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl + Linear7.bpl Linear8.bpl Linear9.bpl) do ( + echo -------------------- %%f -------------------- + %BGEXE% %* -infer:p -printInstrumented -noVerify %%f +) + +for %%f in (Bound.bpl) do ( + echo -------------------- %%f -------------------- + %BGEXE% %* -infer:p %%f +) + -- cgit v1.2.3