diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-02 18:30:25 +0200 |
commit | 71c58a8d494eafd847776446b0c246229b2bc9cf (patch) | |
tree | 7570087588f24b3b340baeed5871b398bf7fc390 /mppa_k1c/Op.v | |
parent | dc8b24fa2dd7ede561dd75458899cf42e9be09d2 (diff) | |
download | compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.tar.gz compcert-kvx-71c58a8d494eafd847776446b0c246229b2bc9cf.zip |
avancement (il faut utiliser Vundef visiblement)
Diffstat (limited to 'mppa_k1c/Op.v')
-rw-r--r-- | mppa_k1c/Op.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 815d3958..f3ee0577 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -1649,6 +1649,27 @@ Proof. - apply Val.offset_ptr_inject; auto. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *. + 1,2: inv Hinjvl; trivial; + inv H0; trivial; + inv H2; trivial; + discriminate. + 2,3: inv Hinjvl; trivial; discriminate. + inv Hinjvl; trivial; inv H0; trivial; + inv H; trivial; discriminate. +Qed. + End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1755,6 +1776,24 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. + +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *. + 1, 2, 4, 5: inv Hlessdef; trivial; + inv H0; trivial; + inv H2; trivial; + discriminate. + inv Hlessdef; trivial. + inv H0; trivial. + discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) |