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/new1.bpl b/Test/og/new1.bpl
index 6ebb9cf1..64144ae9 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,6 +2,12 @@ function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
 

 var g:int;

 

+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

+{

+  x

+}

+

+

 var {:linear "Perm"} Permissions: [int]bool;

 

 procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);