More faithful semantics for volatile reads and writes.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 8 insertions, 0 deletions

diff --git a/common/Values.v b/common/Values.v
index 056cffb..236a5ae 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1029,6 +1029,14 @@ Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:=
 
 Hint Resolve val_nil_inject val_cons_inject.
 
+Lemma val_load_result_inject:
+  forall f chunk v1 v2,
+  val_inject f v1 v2 ->
+  val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
+Proof.
+  intros. inv H; destruct chunk; simpl; econstructor; eauto.
+Qed.
+
 (** Monotone evolution of a memory injection. *)
 
 Definition inject_incr (f1 f2: meminj) : Prop :=