Lines Matching refs:post
1032 the w-post-bounded relation defined below in the PLAIN ACCESSES AND
2458 "post-bounded" by X and E is "pre-bounded" by Y.
2461 "r-post-bounded" by X. Similarly, E would be "r-pre-bounded" or
2466 say that a marked access pre-bounds and post-bounds itself (e.g., if R
2484 w-pre-bounded or w-post-bounded by a marked access, it also requires
2485 the store to be r-pre-bounded or r-post-bounded, so as to handle cases
2545 is definitely w-post-bounded before the store to ptr, and the two
2579 not need to be w-post-bounded: when it is separated from the other
2616 isn't w-post-bounded by any marked accesses.
2622 w-post-bounded ; vis ; w-pre-bounded
2626 r-post-bounded ; xb* ; w-pre-bounded
2630 w-post-bounded ; vis ; r-pre-bounded
2635 r-post-bounded ; xb* ; w-pre-bounded
2639 w-post-bounded ; vis ; r-pre-bounded
2646 sequence with no post-bounding, and in every case the LKMM also allows