diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 14:07:14 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 14:07:14 +0100 |
commit | d382f4e5274554df3e39c272b46a7721bc3d4716 (patch) | |
tree | 4842bff575cbe6afa739066027366450d4e2c90d /arm | |
parent | 707b8ef8e12ed033655161271512f962dd8906d4 (diff) | |
download | compcert-kvx-d382f4e5274554df3e39c272b46a7721bc3d4716.tar.gz compcert-kvx-d382f4e5274554df3e39c272b46a7721bc3d4716.zip |
cond_depends_on
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Op.v | 14 |
1 files changed, 7 insertions, 7 deletions
@@ -718,7 +718,7 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) -Definition condition_depends_on_memory (c: condition) : bool := +Definition cond_depends_on_memory (c: condition) : bool := match c with | Ccompu _ | Ccompushift _ _| Ccompuimm _ _ => true | _ => false @@ -726,14 +726,14 @@ Definition condition_depends_on_memory (c: condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp c => condition_depends_on_memory c - | Osel c ty => condition_depends_on_memory c + | Ocmp c => cond_depends_on_memory c + | Osel c ty => cond_depends_on_memory c | _ => false end. -Lemma condition_depends_on_memory_correct: +Lemma cond_depends_on_memory_correct: forall c args m1 m2, - condition_depends_on_memory c = false -> + cond_depends_on_memory c = false -> eval_condition c args m1 = eval_condition c args m2. Proof. intros. destruct c; simpl; auto; discriminate. @@ -745,9 +745,9 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence; intros C. -- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- f_equal; f_equal; apply cond_depends_on_memory_correct; auto. - destruct args; auto. destruct args; auto. - rewrite (condition_depends_on_memory_correct c args m1 m2 C). + rewrite (cond_depends_on_memory_correct c args m1 m2 C). auto. Qed. |