diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 10:34:34 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 10:34:34 +0200 |
| commit | 61289bf034eebcfcaf04e833876d583e47aef659 (patch) | |
| tree | e4cd9199eaabd097c91e3588db03a6886728ca67 /mppa_k1c/Asmblock.v | |
| parent | 4adb0af96c3c0523438e86275f9e23ffdc69e4ba (diff) | |
| download | compcert-kvx-61289bf034eebcfcaf04e833876d583e47aef659.tar.gz compcert-kvx-61289bf034eebcfcaf04e833876d583e47aef659.zip | |
Small refactoring and renaming of Stores and Loads
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 3656b91f..9d7b372e 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -244,7 +244,7 @@ Inductive cf_instruction : Type := . (** Loads **) -Inductive load_name_rro : Type := +Inductive load_name : Type := | Plb (**r load byte *) | Plbu (**r load byte unsigned *) | Plh (**r load half word *) @@ -258,15 +258,15 @@ Inductive load_name_rro : Type := . Inductive ld_instruction : Type := - | PLoadRRO (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset) - | PLoadRRR (i: load_name_rro) (rd: ireg) (ra: ireg) (rofs: ireg) + | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . -Coercion PLoadRRO: load_name_rro >-> Funclass. -Coercion PLoadRRR: load_name_rro >-> Funclass. +Coercion PLoadRRO: load_name >-> Funclass. +Coercion PLoadRRR: load_name >-> Funclass. (** Stores **) -Inductive store_name_rro : Type := +Inductive store_name : Type := | Psb (**r store byte *) | Psh (**r store half byte *) | Psw (**r store int32 *) @@ -278,12 +278,12 @@ Inductive store_name_rro : Type := . Inductive st_instruction : Type := - | PStoreRRO (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset) - | PStoreRRR (i: store_name_rro) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) + | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) . -Coercion PStoreRRO: store_name_rro >-> Funclass. -Coercion PStoreRRR: store_name_rro >-> Funclass. +Coercion PStoreRRO: store_name >-> Funclass. +Coercion PStoreRRR: store_name >-> Funclass. (** Arithmetic instructions **) Inductive arith_name_r : Type := |