new design for linear types + VCgen

ported all the examples
added the QED examples to runtest.bat

1 files changed, 6 insertions, 0 deletions

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 047d25a6..161171bf 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -10,6 +10,12 @@ var {:qed} lock : [int]X;
 var {:qed} owner : [int]X;

 const max : int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 axiom (max > 0);

 

 procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);