Changes between Version 27 and Version 28 of ContractReduction

Timestamp:

12/07/15 13:04:31 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -3 +3 @@
 == ACSL function contract grammar with CIVL-C extension (starting with `$`) ==
 {{{
-function-contract ::= requires-clause∗ terminates-clause? decreases-clause?
+function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause?
                       simple-clause∗  named-behavior∗ completeness-clause∗ 
 requires-clause ::= requires pred ;
 terminates-clause ::= terminates pred ;
 decreases-clause  ::= decreases term (for id)? ;
+guards-clause ::= $guards pred ;
 simple-clause ::= assigns-clause | ensures-clause 
                 | allocation-clause | abrupt-clause-fn
@@ -172 +173 @@
 
 {{{
-$guard {bool-expr}
+$guard bool-expr
 }}}