diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
| commit | 35febfa5b231a71234a1b32c128169352e96eaca (patch) | |
| tree | 5401681c76c8e45e9c1e6128d313851582e6fc9f /arm/Asmgen.v | |
| parent | 046c24d29796a3bb130c94fe464e54e8a7aa2eb3 (diff) | |
| download | compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.tar.gz compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.zip | |
fixes for ARM
Diffstat (limited to 'arm/Asmgen.v')
| -rw-r--r-- | arm/Asmgen.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 1a1e7f2f..016a1c5a 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -689,8 +689,12 @@ Definition transl_memory_access_float None mk_immed addr args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => match chunk with | Mint8signed => transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k @@ -708,6 +712,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -747,8 +752,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_int IR13 f.(fn_link_ofs) IR12 c) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl arg) => |