From 64d8963508ce048d00db3766f4ca597b792c1b95 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Sat, 18 May 2013 21:15:20 -0700
Subject: reworked the linear and og implementation based on available
 variables theory

---
 Test/linear/allocator.bpl | 2 +-
 Test/linear/f1.bpl        | 6 ++----
 Test/linear/f2.bpl        | 3 ++-
 Test/linear/typecheck.bpl | 6 ++++++
 4 files changed, 11 insertions(+), 6 deletions(-)

(limited to 'Test/linear')

diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index 4b162a83..d723cbed 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -3,7 +3,7 @@ procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
 
 procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 
 {
-  assume i == i';
+  i := i';
   call i := A(i);
   assert false;
 }
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
index 0d9189ab..1f451daf 100644
--- a/Test/linear/f1.bpl
+++ b/Test/linear/f1.bpl
@@ -24,9 +24,7 @@ procedure {:entrypoint} main({:linear "1"} x_in: [int]bool)
   requires b1 ==> x_in != mapconstbool(false);
 {
    var {:linear "1"} x: [int] bool;
-   assume x == x_in;
-
-   assume x == mapconstbool(true);
+   x := x_in;
 
    call foo(x);
    
@@ -40,7 +38,7 @@ procedure foo({:linear "1"} x_in: [int]bool)
   requires b3 ==> x_in != mapconstbool(false);
 {
    var {:linear "1"} x: [int] bool;
-   assume x == x_in;
+   x := x_in;
 
    assert b4 ==> x == mapconstbool(true);
    assert b5 ==> x != mapconstbool(false);
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 4e4bfbcf..82871466 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -4,6 +4,7 @@ function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
 procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
 ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
 
+procedure Allocate() returns ({:linear "1"} x: [int]bool);
 
 procedure {:entrypoint} main() 
 {
@@ -11,7 +12,7 @@ procedure {:entrypoint} main()
    var {:linear "1"} x1: [int] bool;
    var {:linear "1"} x2: [int] bool;
 
-   havoc x;
+   call x := Allocate();
    assume x == mapconstbool(true);
 
    call x1, x2 := Split(x);
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index ff2d7da4..7bdb339e 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -74,3 +74,9 @@ procedure G(i:int) returns({:linear "x"} r:int)
 {
   r := g;
 }
+
+procedure H(i:int) returns({:linear "x"} r:int)
+modifies g;
+{
+  g := r;
+}
-- 
cgit v1.2.3