diff options
Diffstat (limited to 'Test/inline/test5.bpl')
| -rw-r--r-- | Test/inline/test5.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
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
+}
|