new design for linear types + VCgen

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

1 files changed, 10 insertions, 0 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 730b1ce1..ec61e188 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -6,6 +6,16 @@ var {:qed} lock: X;
 var {:qed} currsize: int;

 var {:qed} newsize: int;

 

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

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

+{

+  MapConstBool(false)[x := true]

+}

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

+{

+  x

+}

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     0 <= currsize && currsize <= newsize &&