From dae202e121342b691585a78caaec8f4100c3123d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 1 Mar 2021 21:52:27 +0100 Subject: Proofs finished for expansion --- riscV/ExpansionOracle.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 39b8f367..41a2227b 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = insn :: (if normal' then Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] -- cgit