From 64d8963508ce048d00db3766f4ca597b792c1b95 Mon Sep 17 00:00:00 2001 From: Unknown Date: Sat, 18 May 2013 21:15:20 -0700 Subject: reworked the linear and og implementation based on available variables theory --- Test/og/new1.bpl | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 Test/og/new1.bpl (limited to 'Test/og/new1.bpl') diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl new file mode 100644 index 00000000..472e64c6 --- /dev/null +++ b/Test/og/new1.bpl @@ -0,0 +1,38 @@ +function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool; + +var g:int; + +var {:linear "Perm"} Permissions: [int]bool; + +procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool); +modifies Permissions; +requires Permissions == mapconstbool(true); +ensures xls == mapconstbool(true) && Permissions == mapconstbool(false); + +procedure PB({:linear "Perm"} permVar_in:[int]bool) +requires permVar_in[0] && g == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert permVar_out[0]; + assert g == 0; + + g := g + 1; + + yield; + assert permVar_out[0]; + assert g == 1; +} + +procedure{:entrypoint} Main() +requires Permissions == mapconstbool(true); +{ + var {:linear "Perm"} permVar_out: [int]bool; + + call permVar_out := Allocate_Perm(); + + g := 0; + async call PB(permVar_out); +} -- cgit v1.2.3