From 4297fcb821c3188449b64184af73e41491a6118f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 23 Jul 2012 15:01:54 +0000 Subject: - Revised non-overflow constraints on memory injections so that injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7b18d8f..ea5d68e 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1753,6 +1753,8 @@ Proof. inv B; auto. inv H0; auto. constructor. auto. (* float64 *) exists va; auto. + (* float64al32 *) + exists va; auto. Qed. Lemma storev_mapped_content_inject: @@ -2069,8 +2071,7 @@ Lemma var_set_self_correct_array: val_inject f v tv -> Mem.inject f m tm -> PTree.get id e = Some(b, Varray sz al) -> - extcall_memcpy_sem sz (Zmin al 4) ge - (Vptr b Int.zero :: v :: nil) m E0 Vundef m' -> + extcall_memcpy_sem sz al ge (Vptr b Int.zero :: v :: nil) m E0 Vundef m' -> te!(for_var id) = Some tv -> exists f', exists tm', star step tge (State fn a k (Vptr sp Int.zero) te tm) @@ -2087,7 +2088,7 @@ Proof. (* var_stack_array *) unfold var_set_self in VS. rewrite <- H in VS. inv VS. exploit match_callstack_match_globalenvs; eauto. intros [hi' MG]. - assert (external_call (EF_memcpy sz0 (Zmin al0 4)) ge (Vptr b0 Int.zero :: v :: nil) m E0 Vundef m'). + assert (external_call (EF_memcpy sz0 al0) ge (Vptr b0 Int.zero :: v :: nil) m E0 Vundef m'). assumption. exploit external_call_mem_inject; eauto. eapply inj_preserves_globals; eauto. -- cgit v1.2.3