From 0f5087bea45be49e105727d6cee4194598474fee Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 5 Jul 2011 04:13:33 +0000 Subject: 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 --- common/Memdata.v | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index c0e1f500..16adb237 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. -- cgit