reworked the linear and og implementation based on available variables theory

4 files changed, 11 insertions, 6 deletions

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;

+}