Changes between Version 42 and Version 43 of ContractReduction

Timestamp:

12/14/15 10:44:25 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -12 +12 @@
 * `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 is used
+* wildcard term: `\everything`
 
 {{{
@@ -315 +316 @@
 
 {{{
-/*@ depends \read(q->owner)+\write(q->owner);
+/*@ depends \read(q->owner), \write(q->owner);
   @ assigns q->owner;
 */
 $atomic_f _Bool lock(cqueue* q)
-  $depends {$access(q->owner)}
-  $assigns {q->owner}
 {
   if(q->owner==$self)
@@ -333 +332 @@
 
 {{{
-/*@ depends \calls(enqueue, q, ...)+$calls(dequeue,q, ...);
+/*@ depends \calls(enqueue, q, ...), $calls(dequeue,q, ...);
   @ reads q->data;
   @ assigns \nothing;
@@ -347 +346 @@
   @ behavior success:
   @   assumes q->owner==$self;
-  @   $depends $access(q->owner);
+  @   depends \access(q->owner);
   @   assigns q->owner;
   @ behavior failure:
   @   assumes q->owner!=$self;
-  @   $depends \nothing;
+  @   depends \nothing;
   @   assigns \nothing;
   @*/