Changes between Version 36 and Version 37 of ContractReduction

Timestamp:

12/11/15 13:25:53 (10 years ago)

Author:

zmanchun

Comment:

--

ContractReduction

@@ -253 +253 @@
 /*@ requires scope <= $root && gbarrier!=\null && place >= 0;
  *@ ensures $gbarrier_process_at(gbarrier, place)==$self;
- *@ $depends $calls($barrier_create, $everything, gbarrier, place);
+ *@ depends \calls($barrier_create, $everything, gbarrier, place);
  *@ assigns \nothing;
  *@ behavior success:
@@ -281 +281 @@
 {{{
 /* Calls the barrier associated with this local barrier object.*/
-/*@ $depends \nothing;
+/*@ depends \nothing;
   @ assigns \nothing; // although the barrier records is updated but it gets cleaned up when the method returns
   @*/