diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-06 15:54:56 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-06 15:54:56 +0100 |
| commit | 3811d877943c0724dc3abf03709849942e912aa9 (patch) | |
| tree | a1e71beceb1416dced360a707bc312b2158450ab /mppa_k1c/Asmblockgen.v | |
| parent | 9e2184dc81f6375140114208bd8a2db89b905d38 (diff) | |
| download | compcert-kvx-3811d877943c0724dc3abf03709849942e912aa9.tar.gz compcert-kvx-3811d877943c0724dc3abf03709849942e912aa9.zip | |
MBcond true proved (but a small change needs to be done to Asmblockgenproof1)
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f09e2a73..e16c701f 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -61,6 +61,7 @@ Definition make_immed64 (val: int64) := Imm64_single val. Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity). Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity). Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity). +Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity). (** Smart constructors for arithmetic operations involving a 32-bit or 64-bit integer constant. Depending on whether the @@ -156,6 +157,10 @@ Definition transl_opt_compuimm loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k) . +(* Definition transl_opt_compuimm + (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := + loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k). *) + (* match select_comp n c with | Some Ceq => Pcbu BTweqz r1 lbl ::g k | Some Cne => Pcbu BTwnez r1 lbl ::g k |