Changes between Version 6 and Version 7 of Function_Contracts

Timestamp:

01/18/16 20:36:18 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ -15 +15 @@
 depends: 'depends' e (',' e)* ';' ;
 ...
-behavior: 'behavior' id ':' behaviorBody ;
+behavior: 'begin behavior' id ':' behaviorBody 'end behavior';
 behaviorBody: behaviorClause+;
 behaviorClause: assumes | requires | simple ;
@@ -27 +27 @@
 fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
   reads deref(buf);
-  behavior send:
+  begin behavior send:
     depends writes(buf);
     assigns nothing;
-  behavior receive:
+  end behavior
+  begin behavior receive:
     depends access(deref(buf));
     assigns deref(buf);
+  end behavior
 {
   begin choose
@@ -67 +69 @@
  * Note: `guards`, `depends` and `reads` are CIVL extension for ACSL
 * named behavior:
- * `behavior id : c0; c1; c2; ...`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
+ * `begin behavior id : c0; c1; c2; ... end behavior`, where `id` is the name of this behavior, `c0, c1, c2, ...` are behavior clauses
  * behavior clause: a clause that can be used in the body of a behavior, and could be one of the following:
   * assumes clause
@@ -110 +112 @@
 fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
   reads deref(buf);
-  behavior send:
+  begin behavior send:
     depends writes(buf);
     assigns nothing;
-  behavior receive:
+  end behavior
+  begin behavior receive:
     depends access(deref(buf));
     assigns deref(buf);
+  end behavior
 {
   begin choose