diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
| commit | 0f5087bea45be49e105727d6cee4194598474fee (patch) | |
| tree | 6155d21f87a98b34ad232504d1124657ec4ed359 /common/Memdata.v | |
| parent | 1b21b6d72a4cdeb07ad646e7573983faaae47399 (diff) | |
Back from Oregon commit.
powerpc/*: better compilation of some comparisons; revised asmgenproof1.
common/*: added Mem.storebytes; used to give semantics to memcpy builtin.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index c0e1f50..16adb23 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -69,10 +69,10 @@ Qed. multiple of the natural alignment for the chunk being addressed. This natural alignment is defined by the following [align_chunk] function. Some target architectures - (e.g. the PowerPC) have no alignment constraints, which we could + (e.g. PowerPC and x86) have no alignment constraints, which we could reflect by taking [align_chunk chunk = 1]. However, other architectures have stronger alignment requirements. The following definition is - appropriate for PowerPC and ARM. *) + appropriate for PowerPC, ARM and x86. *) Definition align_chunk (chunk: memory_chunk) : Z := match chunk with @@ -1053,9 +1053,12 @@ Proof. constructor. Qed. -Lemma memval_inject_id: - forall mv, memval_inject inject_id mv mv. +Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. + +Lemma memval_lessdef_refl: + forall mv, memval_lessdef mv mv. Proof. - destruct mv; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. + red. destruct mv; econstructor. + unfold inject_id; reflexivity. rewrite Int.add_zero; auto. Qed. |