diff options
Diffstat (limited to 'Test/og/new1.bpl')
-rw-r--r-- | Test/og/new1.bpl | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index 472e64c6..6ebb9cf1 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -9,7 +9,7 @@ modifies Permissions; requires Permissions == mapconstbool(true);
ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);
-procedure PB({:linear "Perm"} permVar_in:[int]bool)
+procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)
requires permVar_in[0] && g == 0;
{
var {:linear "Perm"} permVar_out: [int]bool;
@@ -26,7 +26,8 @@ requires permVar_in[0] && g == 0; assert g == 1;
}
-procedure{:entrypoint} Main()
+procedure{:entrypoint} {:yields} Main()
+modifies g, Permissions;
requires Permissions == mapconstbool(true);
{
var {:linear "Perm"} permVar_out: [int]bool;
|