diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Asm.v | 4 | ||||
| -rw-r--r-- | arm/Asmgen.v | 4 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 4 |
3 files changed, 6 insertions, 6 deletions
@@ -615,11 +615,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfcvtsd r1 r2 => Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m | Pfldd r1 r2 n => - exec_load Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pflds r1 r2 n => exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m | Pfstd r1 r2 n => - exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m + exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m | Pfsts r1 r2 n => match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with | Next rs' m' => Next (rs'#FR6 <- Vundef) m' diff --git a/arm/Asmgen.v b/arm/Asmgen.v index b6cb2b3..fcc5061 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -542,7 +542,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_int Pldr mk_immed_mem_word dst addr args k | Mfloat32 => transl_memory_access_float Pflds mk_immed_mem_float dst addr args k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k | Mint64 => Error (msg "Asmgen.transl_load") @@ -563,7 +563,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) transl_memory_access_int Pstr mk_immed_mem_word src addr args k | Mfloat32 => transl_memory_access_float Pfsts mk_immed_mem_float src addr args k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => transl_memory_access_float Pfstd mk_immed_mem_float src addr args k | Mint64 => Error (msg "Asmgen.transl_store") diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 99dfa46..01b881f 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -350,7 +350,7 @@ let print_builtin_vload_common oc chunk args res = | Mfloat32, [IR addr], [FR res] -> fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 - | (Mfloat64 | Mfloat64al32), [IR addr], [FR res] -> + | Mfloat64, [IR addr], [FR res] -> fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 | _ -> assert false @@ -381,7 +381,7 @@ let print_builtin_vstore_common oc chunk args = | Mfloat32, [IR addr; FR src] -> fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 - | (Mfloat64 | Mfloat64al32), [IR addr; FR src] -> + | Mfloat64, [IR addr; FR src] -> fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1 | _ -> assert false |