diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 19:52:27 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 19:52:27 +0200 |
| commit | 74d06cfedc4a57fbb0be8772431033120b553ab2 (patch) | |
| tree | e923f3bd697e21d75a45885fe6b482d4571a9e5e /backend/CSEproof.v | |
| parent | f440208c6b6159fd83dd6c365e194fe39b30d794 (diff) | |
| download | compcert-kvx-74d06cfedc4a57fbb0be8772431033120b553ab2.tar.gz compcert-kvx-74d06cfedc4a57fbb0be8772431033120b553ab2.zip | |
ValueDomain.aptr_of_aval: be more conservative with pointers synthesized from numbers.
For example: *((int *) 0x10000) = 0. This write used to be treated as not interfering with any load. With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame.
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 74e3ceca..b59078d4 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -696,7 +696,7 @@ Proof. rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). { intros until i. unfold aaddr; subst approx. intros. - specialize (H5 r). rewrite H6 in H5. rewrite match_aptr_of_aval in H5. + specialize (H5 r). rewrite H6 in H5. apply match_aptr_of_aval in H5. rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. } exploit (A rsrc); eauto. intros [P Q]. |