diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-18 13:22:09 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-18 13:22:09 +0100 |
| commit | 9c9d516ba5df536d15bc27bed0a84fd8170fcdc0 (patch) | |
| tree | d1b7765b8bc9d7ea245f206d9e72ba8502e80707 /riscV/Asmgenproof1.v | |
| parent | 1e06ebb8dd836a8c9c80769bc8c8cf42077a6eb5 (diff) | |
| download | compcert-kvx-9c9d516ba5df536d15bc27bed0a84fd8170fcdc0.tar.gz compcert-kvx-9c9d516ba5df536d15bc27bed0a84fd8170fcdc0.zip | |
Proof of Ocmp expansions without immediate and some drafts in comment
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |