From 8ac64d0cc88dc65859d2cd579d2917b05e931c07 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 18:55:10 +0100 Subject: Enable Linear inequality lit tests. --- Test/aitest1/Answer | 8 +-- Test/aitest1/Bound.bpl | 4 +- Test/aitest1/Bound.bpl.expect | 7 +++ Test/aitest1/Linear0.bpl | 2 + Test/aitest1/Linear0.bpl.expect | 20 ++++++ Test/aitest1/Linear1.bpl | 2 + Test/aitest1/Linear1.bpl.expect | 21 +++++++ Test/aitest1/Linear2.bpl | 2 + Test/aitest1/Linear2.bpl.expect | 21 +++++++ Test/aitest1/Linear3.bpl | 2 + Test/aitest1/Linear3.bpl.expect | 21 +++++++ Test/aitest1/Linear4.bpl | 2 + Test/aitest1/Linear4.bpl.expect | 33 ++++++++++ Test/aitest1/Linear5.bpl | 2 + Test/aitest1/Linear5.bpl.expect | 45 ++++++++++++++ Test/aitest1/Linear6.bpl | 2 + Test/aitest1/Linear6.bpl.expect | 41 +++++++++++++ Test/aitest1/Linear7.bpl | 2 + Test/aitest1/Linear7.bpl.expect | 39 ++++++++++++ Test/aitest1/Linear8.bpl | 2 + Test/aitest1/Linear8.bpl.expect | 27 ++++++++ Test/aitest1/Linear9.bpl | 2 + Test/aitest1/Linear9.bpl.expect | 35 +++++++++++ Test/aitest1/ineq.bpl | 2 + Test/aitest1/ineq.bpl.expect | 133 ++++++++++++++++++++++++++++++++++++++++ 25 files changed, 472 insertions(+), 5 deletions(-) create mode 100644 Test/aitest1/Bound.bpl.expect create mode 100644 Test/aitest1/Linear0.bpl.expect create mode 100644 Test/aitest1/Linear1.bpl.expect create mode 100644 Test/aitest1/Linear2.bpl.expect create mode 100644 Test/aitest1/Linear3.bpl.expect create mode 100644 Test/aitest1/Linear4.bpl.expect create mode 100644 Test/aitest1/Linear5.bpl.expect create mode 100644 Test/aitest1/Linear6.bpl.expect create mode 100644 Test/aitest1/Linear7.bpl.expect create mode 100644 Test/aitest1/Linear8.bpl.expect create mode 100644 Test/aitest1/Linear9.bpl.expect create mode 100644 Test/aitest1/ineq.bpl.expect (limited to 'Test') diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index 880e587b..f5b5de90 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -446,10 +446,10 @@ implementation foo() Boogie program verifier finished with 0 verified, 0 errors -------------------- Bound.bpl -------------------- -Bound.bpl(24,3): Error BP5001: This assertion might not hold. +Bound.bpl(26,3): Error BP5001: This assertion might not hold. Execution trace: - Bound.bpl(8,1): start - Bound.bpl(14,1): LoopHead - Bound.bpl(22,1): AfterLoop + Bound.bpl(10,1): start + Bound.bpl(16,1): LoopHead + Bound.bpl(24,1): AfterLoop Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl index 02b2c460..7df27414 100644 --- a/Test/aitest1/Bound.bpl +++ b/Test/aitest1/Bound.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j %s > %t +// RUN: %diff %s.expect %t const TEST: name; procedure P() @@ -25,4 +27,4 @@ AfterLoop: return; } -type name; \ No newline at end of file +type name; diff --git a/Test/aitest1/Bound.bpl.expect b/Test/aitest1/Bound.bpl.expect new file mode 100644 index 00000000..46c18d30 --- /dev/null +++ b/Test/aitest1/Bound.bpl.expect @@ -0,0 +1,7 @@ +Bound.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Bound.bpl(10,1): start + Bound.bpl(16,1): LoopHead + Bound.bpl(24,1): AfterLoop + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl index 7a11c803..3a74b1e9 100644 --- a/Test/aitest1/Linear0.bpl +++ b/Test/aitest1/Linear0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear0.bpl.expect b/Test/aitest1/Linear0.bpl.expect new file mode 100644 index 00000000..5950e8d1 --- /dev/null +++ b/Test/aitest1/Linear0.bpl.expect @@ -0,0 +1,20 @@ +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume {:inferred} true; + assume {:inferred} true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl index 0cbb4a07..505d1a11 100644 --- a/Test/aitest1/Linear1.bpl +++ b/Test/aitest1/Linear1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear1.bpl.expect b/Test/aitest1/Linear1.bpl.expect new file mode 100644 index 00000000..5e2c8d04 --- /dev/null +++ b/Test/aitest1/Linear1.bpl.expect @@ -0,0 +1,21 @@ +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume {:inferred} true; + assume x * x == y; + assume {:inferred} true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl index 9e02c9e2..de1da8a1 100644 --- a/Test/aitest1/Linear2.bpl +++ b/Test/aitest1/Linear2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear2.bpl.expect b/Test/aitest1/Linear2.bpl.expect new file mode 100644 index 00000000..6d8b9403 --- /dev/null +++ b/Test/aitest1/Linear2.bpl.expect @@ -0,0 +1,21 @@ +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume {:inferred} true; + assume x == 8; + assume {:inferred} x == 8; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl index c6b7a441..4b91bd0f 100644 --- a/Test/aitest1/Linear3.bpl +++ b/Test/aitest1/Linear3.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear3.bpl.expect b/Test/aitest1/Linear3.bpl.expect new file mode 100644 index 00000000..e65b3971 --- /dev/null +++ b/Test/aitest1/Linear3.bpl.expect @@ -0,0 +1,21 @@ +var x: int; + +var y: int; + +procedure p(); + + + +implementation p() +{ + + start: + assume {:inferred} true; + assume x < y; + assume {:inferred} true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl index 2207debe..c3e908f2 100644 --- a/Test/aitest1/Linear4.bpl +++ b/Test/aitest1/Linear4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear4.bpl.expect b/Test/aitest1/Linear4.bpl.expect new file mode 100644 index 00000000..29b3c226 --- /dev/null +++ b/Test/aitest1/Linear4.bpl.expect @@ -0,0 +1,33 @@ +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume {:inferred} true; + assume x < y; + assume {:inferred} true; + goto B, C; + + C: + assume {:inferred} true; + assume {:inferred} true; + return; + + B: + assume {:inferred} true; + x := x * x; + assume {:inferred} true; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl index 199cb6f2..69cbb7a7 100644 --- a/Test/aitest1/Linear5.bpl +++ b/Test/aitest1/Linear5.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear5.bpl.expect b/Test/aitest1/Linear5.bpl.expect new file mode 100644 index 00000000..fcd1ab08 --- /dev/null +++ b/Test/aitest1/Linear5.bpl.expect @@ -0,0 +1,45 @@ +var x: int; + +var y: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume {:inferred} true; + assume -1 <= x; + assume {:inferred} -1 <= x; + goto B, E; + + E: + assume {:inferred} true; + assume {:inferred} true; + return; + + B: + assume {:inferred} -1 <= x; + assume x < y; + assume {:inferred} -1 <= x && 0 <= y; + goto C, E; + + C: + assume {:inferred} -1 <= x && 0 <= y; + x := x * x; + assume {:inferred} x < 2 && 0 <= y; + goto D, E; + + D: + assume {:inferred} x < 2 && 0 <= y; + x := y; + assume {:inferred} 0 <= x && 0 <= y; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl index 83e52a9a..7d066435 100644 --- a/Test/aitest1/Linear6.bpl +++ b/Test/aitest1/Linear6.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear6.bpl.expect b/Test/aitest1/Linear6.bpl.expect new file mode 100644 index 00000000..1cb757b0 --- /dev/null +++ b/Test/aitest1/Linear6.bpl.expect @@ -0,0 +1,41 @@ +var x: int; + +var y: int; + +var z: int; + +procedure p(); + modifies x; + + + +implementation p() +{ + + A: + assume {:inferred} true; + x := 8; + assume {:inferred} x == 8; + goto B, C; + + C: + assume {:inferred} x == 8; + x := 10; + assume {:inferred} x == 10; + goto D; + + D: + assume {:inferred} 9 <= x && x < 11; + assume {:inferred} 9 <= x && x < 11; + return; + + B: + assume {:inferred} x == 8; + x := 9; + assume {:inferred} x == 9; + goto D; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl index b1bcaaaf..45514a67 100644 --- a/Test/aitest1/Linear7.bpl +++ b/Test/aitest1/Linear7.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Simple test file for checking the inference of linear constraints. var x: int; diff --git a/Test/aitest1/Linear7.bpl.expect b/Test/aitest1/Linear7.bpl.expect new file mode 100644 index 00000000..513b97dd --- /dev/null +++ b/Test/aitest1/Linear7.bpl.expect @@ -0,0 +1,39 @@ +var x: int; + +var y: int; + +var z: int; + +procedure p(); + + + +implementation p() +{ + + A: + assume {:inferred} true; + assume {:inferred} true; + goto B, C; + + C: + assume {:inferred} true; + assume y <= 0; + assume {:inferred} y < 1; + goto D; + + D: + assume {:inferred} true; + assume {:inferred} true; + return; + + B: + assume {:inferred} true; + assume x <= 0; + assume {:inferred} x < 1; + goto D; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl index 4bc3f887..14f396ad 100644 --- a/Test/aitest1/Linear8.bpl +++ b/Test/aitest1/Linear8.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t procedure foo () returns () { diff --git a/Test/aitest1/Linear8.bpl.expect b/Test/aitest1/Linear8.bpl.expect new file mode 100644 index 00000000..f93f5770 --- /dev/null +++ b/Test/aitest1/Linear8.bpl.expect @@ -0,0 +1,27 @@ +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + A: + assume {:inferred} true; + n := 0; + j := 0; + i := j + 1; + i := i + 1; + i := i + 1; + i := i + 1; + i := i + 1; + j := j + 1; + assume {:inferred} i == 5 && j == 1 && n == 0; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl index e48a7a0c..1352bfb0 100644 --- a/Test/aitest1/Linear9.bpl +++ b/Test/aitest1/Linear9.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t procedure foo () returns () { var i: int; diff --git a/Test/aitest1/Linear9.bpl.expect b/Test/aitest1/Linear9.bpl.expect new file mode 100644 index 00000000..23ac1698 --- /dev/null +++ b/Test/aitest1/Linear9.bpl.expect @@ -0,0 +1,35 @@ +procedure foo(); + + + +implementation foo() +{ + var i: int; + var j: int; + var n: int; + + entry: + assume {:inferred} true; + assume n >= 4; + i := 0; + j := i + 1; + assume {:inferred} i == 0 && j == 1 && 4 <= n; + goto exit, loop0; + + loop0: // cut point + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; + assume j <= n; + i := i + 1; + j := j + 1; + assume {:inferred} 1 <= i && 2 <= j && 4 <= n; + goto loop0, exit; + + exit: + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; + assume {:inferred} 0 <= i && 1 <= j && 4 <= n; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl index a417aaf3..030c435c 100644 --- a/Test/aitest1/ineq.bpl +++ b/Test/aitest1/ineq.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify %s > %t +// RUN: %diff %s.expect %t // Test the polyhedra domain for linear inequalities diff --git a/Test/aitest1/ineq.bpl.expect b/Test/aitest1/ineq.bpl.expect new file mode 100644 index 00000000..d6c36bdd --- /dev/null +++ b/Test/aitest1/ineq.bpl.expect @@ -0,0 +1,133 @@ +procedure SimpleLoop(); + + + +implementation SimpleLoop() +{ + var i: int; + + start: + assume {:inferred} true; + i := 0; + assume {:inferred} i == 0; + goto test; + + test: // cut point + assume {:inferred} 0 <= i && i < 11; + assume {:inferred} 0 <= i && i < 11; + goto Then, Else; + + Else: + assume {:inferred} 0 <= i && i < 11; + assume !(i < 10); + assume {:inferred} 0 <= i && i < 11; + return; + + Then: + assume {:inferred} 0 <= i && i < 11; + assume i < 10; + i := i + 1; + assume {:inferred} 1 <= i && i < 11; + goto test; +} + + + +procedure VariableBoundLoop(n: int); + + + +implementation VariableBoundLoop(n: int) +{ + var i: int; + + start: + assume {:inferred} true; + i := 0; + assume {:inferred} i == 0; + goto test; + + test: // cut point + assume {:inferred} 0 <= i; + assume {:inferred} 0 <= i; + goto Then, Else; + + Else: + assume {:inferred} 0 <= i; + assume !(i < n); + assume {:inferred} 0 <= i; + return; + + Then: + assume {:inferred} 0 <= i; + assume i < n; + i := i + 1; + assume {:inferred} 1 <= i && 1 <= n; + goto test; +} + + + +procedure Foo(); + + + +implementation Foo() +{ + var i: int; + + start: + assume {:inferred} true; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume {:inferred} true; + return; +} + + + +procedure FooToo(); + + + +implementation FooToo() +{ + var i: int; + + start: + assume {:inferred} true; + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume {:inferred} i == 465; + return; +} + + + +procedure FooTooStepByStep(); + + + +implementation FooTooStepByStep() +{ + var i: int; + + L0: + assume {:inferred} true; + i := 5; + i := 3 * i + 1; + i := 3 * (i + 1); + i := 1 + 3 * i; + i := (i + 1) * 3; + assume {:inferred} i == 465; + return; +} + + + +Boogie program verifier finished with 0 verified, 0 errors -- cgit v1.2.3