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 --- backend/Machtyping.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Machtyping.v') diff --git a/backend/Machtyping.v b/backend/Machtyping.v index c2e797ae..b0673ca8 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -285,7 +285,7 @@ Proof. apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. - generalize (external_call_well_typed _ _ _ _ _ _ H). + generalize (external_call_well_typed _ _ _ _ _ _ _ H). unfold proj_sig_res, Conventions.loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. -- cgit