new design for linear types + VCgen

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

1 files changed, 6 insertions, 1 deletions

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 5985b6d6..a263467c 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,9 +1,14 @@
 type X;

-

 const nil: X;

 var l: X;

 var x: int;

 

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

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

+{

+  MapConstBool(false)[x := true]

+}

+

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

 ensures xls != nil;