diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 12:55:43 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 12:55:43 +0200 |
| commit | 25d43e57763cc7d5de12a4d02d817f39a9080655 (patch) | |
| tree | de7b990c5379a17bfcb14472b6d0bf2f0036f2c8 /powerpc/Op.v | |
| parent | 95ba79b10e832025bbc9843f9d14614f7dff0fcb (diff) | |
| download | compcert-kvx-25d43e57763cc7d5de12a4d02d817f39a9080655.tar.gz compcert-kvx-25d43e57763cc7d5de12a4d02d817f39a9080655.zip | |
Ccompuimm now depends on the memory, this is needed to proof the Lemma op_depends_on_memory_correct.
Diffstat (limited to 'powerpc/Op.v')
| -rw-r--r-- | powerpc/Op.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v index 3d5b1fc5..4c1168cd 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -569,6 +569,7 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true + | Ocmp (Ccompuimm _ _) => true | _ => false end. @@ -577,8 +578,8 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; auto; discriminate. + intros until m2. destruct op; simpl; try congruence. unfold eval_condition. + destruct c; simpl; auto; try discriminate. Qed. (** Global variables mentioned in an operation or addressing mode *) |