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/ticket.bpl b/Test/og/ticket.bpl
index fe56fb27..3404f8e0 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -11,6 +11,16 @@ var {:qed} s: int;
 var {:qed} cs: X;

 var {:qed} T: [int]bool;

 

+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} Inv1(tickets: [int]bool, ticket: int): (bool)

 {

     tickets == RightOpen(ticket)