From 7999c9ee1f09f7d555e3efc39f030564f76a3354 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 10 May 2010 15:35:02 +0000 Subject: - Extended traces so that pointers within globals are supported as event values. - Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Complements.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Complements.v b/driver/Complements.v index b76a99f..a67d61e 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -64,7 +64,9 @@ Proof. congruence. assert (ef0 = ef) by congruence. subst ef0. assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0. - exploit external_call_determ. eexact H4. eexact H9. auto. + exploit external_call_determ. + instantiate (1 := Genv.find_symbol ge). exact (Genv.genv_vars_inj ge). + eexact H4. eexact H9. auto. intros [A [B C]]. subst. intuition congruence. Qed. -- cgit v1.2.3