diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 2 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b9300fd7..4fb38ff8 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -864,7 +864,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pisel rd r1 r2 bit => let v := match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1 + | Vint n => if Int.eq n Int.zero then rs#r2 else (gpr_or_zero rs r1) | _ => Vundef end in Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 884d5366..20cf9c1d 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1284,7 +1284,9 @@ Proof. reflexivity. + Simpl. rewrite <- (C r1), <- (C r2) by auto. - rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + rewrite B, gpr_or_zero_not_zero. + destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + destruct dir; intros e; subst; discriminate. + intros. Simpl. Qed. |