Changes between Version 6 and Version 7 of ContractReduction
- Timestamp:
- 07/01/14 22:32:02 (12 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
ContractReduction
v6 v7 10 10 11 11 * `$reach(void * obj)` 12 * 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 followingarray elements, struct members, and pointer dereferences.12 * 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. 13 13 * `$reach_rec(void * obj)` 14 * holds iff any of the memory units reachable from the object pointed to by`obj` (including the object pointed to by `obj` itself) is reachable from`p`14 * holds iff any of the memory units reachable from `obj` (including the object pointed to by `obj` itself) is reachable from`p` 15 15 * `$write(void * obj)` 16 16 * 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.
