Changes between Version 2 and Version 3 of Function_Contracts

Timestamp:

01/11/16 16:56:17 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ -21 +21 @@
             | 'Disjoint' (id (',' id)*)? 
             ;
+}}}
+
+Example
+{{{
+fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
+  Reads deref(buf);
+  Behavior send:
+    Depends writes(buf);
+    Assigns nothing;
+  Behavior receive:
+    Depends access(deref(buf));
+    Assigns deref(buf);
+{
+  begin choose
+  when eq(cmd, 0)
+     do CALL send, <buf, ...>; goto L1;
+  when eq(cmd, 1)
+    do CALL recv, <buf, ...>; goto L1;
+  when and(neq(cmd, 0), neq(cmd, 1))
+    do NOOP; goto L1;
+  end choose
+L1:
+}
+
 }}}