changed type checking of yield procedures so that they can only call other yielding procedures

1 files changed, 5 insertions, 13 deletions

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index f0de76d5..5bc75324 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -10,33 +10,25 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x

 }

 

-procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);

-  ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

-

-

 procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)

-   free requires {:layer 1} permVar_in == ch_mapconstbool(true);

-   free requires {:layer 1} permVar_in[0];

-   free requires {:layer 1} x == 0;

+   requires {:layer 1} permVar_in == ch_mapconstbool(true);

+   requires {:layer 1} x == 0;

 {

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

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

 

     permVar_out := permVar_in;

 

     yield;

     assert {:layer 1} x == 0;

-    assert {:layer 1} permVar_out[0];

     assert {:layer 1} permVar_out == ch_mapconstbool(true);

 

-    call permVar_out, permVarOut2 := Split(permVar_out);

-    async call foo(permVarOut2);

+    async call foo(permVar_out);

     yield;

 }

 

 procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 

-  free requires {:layer 1} permVar_in != ch_mapconstbool(false);

-  free requires {:layer 1} permVar_in[1];

+  requires {:layer 1} permVar_in != ch_mapconstbool(false);

+  requires {:layer 1} permVar_in[1];

   requires {:layer 1} x == 0;

 {

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