From de9be69954d167a71c74ff68dd27e8cc96ba9c12 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 7 Feb 2014 15:18:39 -0800
Subject: new design for linear types + VCgen ported all the examples added the
 QED examples to runtest.bat

---
 Test/linear/Answer   | 4 +---
 Test/linear/list.bpl | 5 +++++
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'Test/linear')

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 2934d690..9219497b 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -1,7 +1,5 @@
 
 -------------------- typecheck.bpl --------------------
-typecheck.bpl(6,22): Error: Linear domain A must be consistently attached to variables of one type
-typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type
 typecheck.bpl(31,9): Error: Only simple assignment allowed on linear variable b
 typecheck.bpl(33,6): Error: Only variable can be assigned to linear variable a
 typecheck.bpl(35,6): Error: Only linear variable can be assigned to linear variable a
@@ -17,7 +15,7 @@ typecheck.bpl(67,0): Error: Output variable d must be available at a return
 typecheck.bpl(76,0): Error: Global variable g must be available at a return
 typecheck.bpl(81,7): Error: unavailable source for a linear read
 typecheck.bpl(82,0): Error: Output variable r must be available at a return
-17 type checking errors detected in typecheck.bpl
+15 type checking errors detected in typecheck.bpl
 
 -------------------- list.bpl --------------------
 
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index f4badca9..b0caa9e1 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -2,6 +2,11 @@ type X;
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
 function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
 
+function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool
+{
+  xs
+}
+
 var head: X;
 var tail: X;
 var {:linear "Mem"} D: [X]bool;
-- 
cgit v1.2.3