diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-05 17:54:36 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-05 17:54:36 +0100 |
| commit | 9e2184dc81f6375140114208bd8a2db89b905d38 (patch) | |
| tree | f27d9c21bcf7bb603e1f6e57efed237555f01336 /mppa_k1c/Asmblockgen.v | |
| parent | f30de37bdb8ef770f238cc968c29d1158c8d8f3f (diff) | |
| download | compcert-kvx-9e2184dc81f6375140114208bd8a2db89b905d38.tar.gz compcert-kvx-9e2184dc81f6375140114208bd8a2db89b905d38.zip | |
Début de MBcond
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a43b0485..f09e2a73 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -133,7 +133,7 @@ Definition transl_compl (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := Pcompl (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k. -(* Definition select_comp (n: int) (c: comparison) : option comparison := +Definition select_comp (n: int) (c: comparison) : option comparison := if Int.eq n Int.zero then match c with | Ceq => Some Ceq @@ -142,7 +142,7 @@ Definition transl_compl end else None - . *) + . Definition transl_opt_compuimm (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := |