diff options
| author |  rustanleino <unknown> | 2009-11-19 18:51:13 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-19 18:51:13 +0000 |
| commit | 8a3d35545386c74864db0662faa5c1d68cd71f01 (patch) | |
| tree | f8a033f8b7cac985a5b7f25ee6e7ddee728e679d /Test/inline/test5.bpl | |
| parent | eaf052fa512f87a16d16cbb6b4c78e7fbaaf85b8 (diff) | |
Fixed bug in inlining (procedure *definitions* had been traversed by StandardVisitor while visiting commands).
This solves Issue #6266.
Diffstat (limited to 'Test/inline/test5.bpl')
| -rw-r--r-- | Test/inline/test5.bpl | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Test/inline/test5.bpl b/Test/inline/test5.bpl index 629cb04c..6460232c 100644 --- a/Test/inline/test5.bpl +++ b/Test/inline/test5.bpl @@ -54,3 +54,26 @@ procedure mainC() call P(1);
assert Mem[1] == 1; // good
}
+
+// -------------------------------------------------
+
+type ref;
+var xyz: ref;
+
+procedure xyzA();
+ modifies xyz;
+ ensures old(xyz) == xyz;
+
+procedure {:inline 1} xyzB()
+ modifies xyz;
+{
+ call xyzA();
+}
+
+procedure xyzMain()
+ modifies xyz;
+{
+ call xyzA();
+ assert old(xyz) == xyz;
+ call xyzB();
+}
|