Boogie:

* Added /mv flag as the start of a Boogie replacement for /cev
* Allow attributes on assume statements
* /mv looks for the assume-statement attribute :captureState with a string-literal argument

1 files changed, 26 insertions, 0 deletions

diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl
new file mode 100644
index 00000000..7c73c411
--- /dev/null
+++ b/Test/test15/CaptureState.bpl
@@ -0,0 +1,26 @@
+type Ref;

+type FieldName;

+var Heap: [Ref,FieldName]int;

+

+const unique F: FieldName;

+

+procedure P(this: Ref, x: int, y: int) returns (r: int)

+  ensures 0 <= r;

+{

+  var m: int;

+

+  assume {:captureState "top"} true;

+

+  m := Heap[this, F];

+  if (0 <= x) {

+    assume {:captureState "then"} true;

+    m := m + 1;

+    assume {:captureState "postUpdate0"} true;

+  } else {

+    assume {:captureState "else"} true;

+    m := (m + y) * (m + y);

+    assume {:captureState "postUpdate1"} true;

+  }

+  r := m + m;

+  assume {:captureState "end"} true;

+}