diff options
| author |  rustanleino <unknown> | 2009-10-14 00:48:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-10-14 00:48:23 +0000 |
| commit | 2e2622a8746e85b8b704ec70adfd35d730e25c19 (patch) | |
| tree | cb8b9a6b9ff6d7dc09cc3513ed44fb42c62ffadb /Test | |
| parent | 5c93063429bf61461a0319c42823da49780a21a2 (diff) | |
Fixed bugs in inlining, and added a test case.
This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/inline/Answer | 15 | ||||
| -rw-r--r-- | Test/inline/test5.bpl | 36 |
2 files changed, 49 insertions, 2 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer index 62d9b677..43ec6740 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -881,8 +881,19 @@ Execution trace: Boogie program verifier finished with 0 verified, 4 errors
-------------------- test5.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
+test5.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ test5.bpl(34,10): anon0
+ test5.bpl(25,23): inline$P$0$Entry
+ test5.bpl(28,10): inline$P$0$anon0
+ test5.bpl(25,23): inline$P$0$Return
+ test5.bpl(34,10): anon0$1
+ test5.bpl(25,23): inline$P$1$Entry
+ test5.bpl(28,10): inline$P$1$anon0
+ test5.bpl(25,23): inline$P$1$Return
+ test5.bpl(34,10): anon0$2
+
+Boogie program verifier finished with 3 verified, 1 error
-------------------- test6.bpl --------------------
test6.bpl(1,22): Error: the inlined procedure is recursive, call stack: foo -> foo
test6.bpl(15,22): Error: the inlined procedure is recursive, call stack: foo2 -> foo3 -> foo1 -> foo2
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl index 0132f60a..629cb04c 100644 --- a/Test/inline/test5.bpl +++ b/Test/inline/test5.bpl @@ -18,3 +18,39 @@ procedure bar() assert x == 5;
}
+// -------------------------------------------------
+
+var Mem : [int]int;
+
+procedure {:inline 1} P(x:int)
+ modifies Mem;
+{
+ Mem[x] := 1;
+}
+
+procedure mainA()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 0; // error
+}
+
+procedure mainB()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 1; // good
+}
+
+procedure mainC()
+ modifies Mem;
+{
+ Mem[1] := 0;
+ call P(0);
+ call P(1);
+ assert Mem[1] == 1; // good
+}
|