From 25d43e57763cc7d5de12a4d02d817f39a9080655 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Apr 2015 12:55:43 +0200 Subject: Ccompuimm now depends on the memory, this is needed to proof the Lemma op_depends_on_memory_correct. --- powerpc/Op.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'powerpc/Op.v') 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 *) -- cgit