diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 21:52:27 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-01 21:52:27 +0100 |
| commit | dae202e121342b691585a78caaec8f4100c3123d (patch) | |
| tree | 3b5e333a0e5fa81794cbd6c2254ae87fcfeafdcd /riscV/ExpansionOracle.ml | |
| parent | 9d0ae4730abbad616991c5df5813bd1e8a981f5e (diff) | |
| download | compcert-kvx-dae202e121342b691585a78caaec8f4100c3123d.tar.gz compcert-kvx-dae202e121342b691585a78caaec8f4100c3123d.zip | |
Proofs finished for expansion
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 ] |