diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-23 15:01:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-23 15:01:54 +0000 |
| commit | 4297fcb821c3188449b64184af73e41491a6118f (patch) | |
| tree | 3f31e0bd4bcfa107a345c1670e65290e785ee091 /cfrontend/Cminorgenproof.v | |
| parent | 7c9500e438384c6c0ce478c8c73b3887137ac924 (diff) | |
| download | compcert-kvx-4297fcb821c3188449b64184af73e41491a6118f.tar.gz compcert-kvx-4297fcb821c3188449b64184af73e41491a6118f.zip | |
- 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
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7b18d8fb..ea5d68e1 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. |