fixed a bug in desugaring of linear variables

5 files changed, 27 insertions, 10 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index c8cb1844..8408bf83 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -72,6 +72,7 @@ namespace Microsoft.Boogie
                 HashSet<Variable> vars = new HashSet<Variable>();

                 foreach (Variable var in this.availableLinearVars[absy])

                 {

+                    if (var is GlobalVariable) continue;

                     string domainName = FindDomainName(var);

                     if (this.linearDomains.ContainsKey(domainName))

                     {

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 9219497b..9fabc440 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -45,3 +45,10 @@ Boogie program verifier finished with 0 verified, 1 error
 -------------------- f3.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

+

+-------------------- bug.bpl --------------------

+bug.bpl(13,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    bug.bpl(12,3): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl
new file mode 100644
index 00000000..b7a6a238
--- /dev/null
+++ b/Test/linear/bug.bpl
@@ -0,0 +1,14 @@
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }

+

+var {:linear ""} g:int;

+

+procedure A()

+{

+}

+

+procedure B()

+{

+  call A();

+  assert false;

+}

diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index c8d3dc62..bd32d250 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (typecheck.bpl) do (
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

 )

 

-for %%f in (list.bpl allocator.bpl f1.bpl f2.bpl f3.bpl) do (

+for %%f in (list.bpl allocator.bpl f1.bpl f2.bpl f3.bpl bug.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 64144ae9..3ba0840d 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -7,13 +7,9 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x

 }

 

-

-var {:linear "Perm"} Permissions: [int]bool;

-

-procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);

-modifies Permissions;

+procedure Allocate_Perm({:linear "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);

 requires Permissions == mapconstbool(true);

-ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);

+ensures xls == mapconstbool(true);

 

 procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)

 requires permVar_in[0] && g == 0;

@@ -32,13 +28,12 @@ requires permVar_in[0] && g == 0;
   assert g == 1;

 }

 

-procedure{:entrypoint} {:yields} Main()

-modifies g, Permissions;

+procedure{:entrypoint} {:yields} Main({:linear "Perm"} Permissions: [int]bool)

 requires Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

 

-  call permVar_out := Allocate_Perm();

+  call permVar_out := Allocate_Perm(Permissions);

 

   g := 0;

   async call PB(permVar_out);