Changes between Version 31 and Version 32 of ContractReduction

Timestamp:

12/08/15 09:44:17 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -6 +6 @@
 * `$depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
 * `$reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
+* additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope `$root` is used
 
 {{{
@@ -20 +21 @@
 tsets ::= location (, location) ∗
 ensures-clause ::= ensures pred ;
-allocation-clause ::= allocates tsets ; | frees tsets ;
+allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ;
 reads-clause ::= $reads tsets;
 depends-clause := $depends event (, event)*;