Changes between Version 7 and Version 8 of ContractReduction

Timestamp:

07/01/14 22:47:34 (12 years ago)

Author:

siegel

Comment:

--

ContractReduction

@@ -9 +9 @@
 The following boolean expressions may be used as constituents in the boolean expression `e`:
 
-* `$reach(void * obj)`
- * holds iff the memory unit pointed to by `obj` is reachable from `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following array elements, struct members, and pointer dereferences.
-* `$reach_rec(void * obj)`
+* `$access(void * obj)`
+ * holds iff the memory unit pointed to by `obj` is reachable from `p`.  This means there is a path from the variables on the call stack of `p` to the memory unit, following array elements, struct members, and pointer dereferences, pointer arithmetic.
+* `$accessRegion(void * obj)`
  * holds iff any of the memory units reachable from `obj` (including the object pointed to by `obj` itself) is reachable from`p`
 * `$write(void * obj)`
  * holds iff the memory unit pointed to by `obj` is not only reachable from `p` but if it is possible that `p` (or a process spawned by `p`) could write to that memory unit at some point now or in the future.
-* `$write_rec(void * obj)`
+* `$writeRegion(void * obj)`
  * like above but true if any of the memory units in the reachable region specified by `obj` may be written to
 
+
+
+I think the following can be done just using the ternary operator `?`:
 
 Conditional amples set: `[COND] $ample{EXPR1} : $ample(EXPR2)`