Changes between Version 29 and Version 30 of ContractReduction

Timestamp:

12/07/15 14:02:00 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -21 +21 @@
 location ::= tset
 ensures-clause ::= ensures pred ;
+allocation-clause ::= allocates dyn-allocation-addresses ; | frees dyn-allocation-addresses ;
+dyn-allocation-addresses ::= location-addresses | \nothing
 reads-clause ::= $reads locations;
 depends-clause := $depends event (, event)*;