diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-23 15:32:36 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | c81c303db03ba732bda8612381e8569db181a541 (patch) | |
| tree | ecff2a29321170d2eda10667c62d843ffd464f43 /mppa_k1c/Asmgen.v | |
| parent | 447ceed8642e2ed000a20036298adb8448ac594b (diff) | |
| download | compcert-kvx-c81c303db03ba732bda8612381e8569db181a541.tar.gz compcert-kvx-c81c303db03ba732bda8612381e8569db181a541.zip | |
MPPA - mppa_call branch cleaning
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 8dd23041..c6f7ef11 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -707,7 +707,7 @@ Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. - + Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := match ty, preg_of src with | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs k) @@ -719,7 +719,6 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : | _, _ => Error (msg "Asmgen.storeind") end. - Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) := indexed_memory_access (Pld dst) base ofs k. |