new design for linear types + VCgen

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

1 files changed, 16 insertions, 0 deletions

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 84ed3a35..43758a91 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -1,5 +1,21 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

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

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

+{

+  MapConstBool(false)[x := true]

+}

+

+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

+{

+  x

+}

+

+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 ensures xls != 0;