diff options
Diffstat (limited to 'riscV/Asmexpand.ml')
| -rw-r--r-- | riscV/Asmexpand.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 945974e0..3e734747 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -23,7 +23,7 @@ open Asm open Asmexpandaux open AST open Camlcoq -open Integers +open !Integers exception Error of string @@ -468,7 +468,8 @@ let expand_builtin_inline name args res = (fun rl -> emit (Pmulw (rl, X a, X b)); emit (Pmulhuw (rh, X a, X b))) - + | "__builtin_nop", [], _ -> + emit Pnop (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -598,10 +599,7 @@ let preg_to_dwarf = function let expand_function id fn = try set_current_function fn; - if !Clflags.option_g then - expand_debug id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code - else - List.iter expand_instruction fn.fn_code; + expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) |