From 74d06cfedc4a57fbb0be8772431033120b553ab2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 18 Jul 2015 19:52:27 +0200 Subject: 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. --- backend/CSEproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/CSEproof.v') 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]. -- cgit