From 9c9d516ba5df536d15bc27bed0a84fd8170fcdc0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 18 Feb 2021 13:22:09 +0100 Subject: Proof of Ocmp expansions without immediate and some drafts in comment --- riscV/Asmgenproof1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 0b1abe2a..35c5b9d6 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -377,7 +377,7 @@ Proof. rewrite <- Float32.cmp_swap. auto. Qed. -(* TODO UNUSUED ? Remark branch_on_X31: +(* TODO gourdinl UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = -- cgit