diff options
| -rw-r--r-- | driver/Driver.ml | 23 | ||||
| -rw-r--r-- | driver/Frontend.ml | 25 | ||||
| -rw-r--r-- | driver/Frontend.mli | 3 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 21 |
4 files changed, 30 insertions, 42 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 27a8edcc..d891cab7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -447,28 +447,7 @@ let _ = Gc.major_heap_increment = 4194304 (* 4M *) }; Printexc.record_backtrace true; - Machine.config := - begin match Configuration.arch with - | "powerpc" -> if Configuration.system = "linux" - then Machine.ppc_32_bigendian - else Machine.ppc_32_diab_bigendian - | "arm" -> if Configuration.is_big_endian - then Machine.arm_bigendian - else Machine.arm_littleendian - | "x86" -> if Configuration.model = "64" then - Machine.x86_64 - else - if Configuration.abi = "macosx" - then Machine.x86_32_macosx - else Machine.x86_32 - | "riscV" -> if Configuration.model = "64" - then Machine.rv64 - else Machine.rv32 - | _ -> assert false - end; - Builtins.set C2C.builtins; - Cutil.declare_attributes C2C.attributes; - CPragmas.initialize(); + Frontend.init (); parse_cmdline cmdline_actions; DebugInit.init (); (* Initialize the debug functions *) if nolink () && !option_o <> None && !num_source_files >= 2 then begin diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 148d0f74..2b9d5860 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -70,6 +70,31 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_if csyntax; csyntax +let init () = + Machine.config:= + begin match Configuration.arch with + | "powerpc" -> if Configuration.gnu_toolchain + then Machine.ppc_32_bigendian + else Machine.ppc_32_diab_bigendian + | "arm" -> if Configuration.is_big_endian + then Machine.arm_bigendian + else Machine.arm_littleendian + | "x86" -> if Configuration.model = "64" then + Machine.x86_64 + else + if Configuration.abi = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 + | "riscV" -> if Configuration.model = "64" + then Machine.rv64 + else Machine.rv32 + | _ -> assert false + end; + Builtins.set C2C.builtins; + Cutil.declare_attributes C2C.attributes; + CPragmas.initialize() + + (* Add gnu preprocessor list *) let gnu_prepro_opt_key key s = prepro_options := s::key::!prepro_options diff --git a/driver/Frontend.mli b/driver/Frontend.mli index d0514d01..39f0e612 100644 --- a/driver/Frontend.mli +++ b/driver/Frontend.mli @@ -22,3 +22,6 @@ val prepro_actions: (Commandline.pattern * Commandline.action) list val prepro_help: string (** Commandline help description *) + +val init: unit -> unit + (** Initialize the Frontend *) diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 9bac7a60..432346a5 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -206,26 +206,7 @@ let _ = Gc.major_heap_increment = 4194304 (* 4M *) }; Printexc.record_backtrace true; - Machine.config := - begin match Configuration.arch with - | "powerpc" -> Machine.ppc_32_bigendian - | "arm" -> if Configuration.is_big_endian - then Machine.arm_bigendian - else Machine.arm_littleendian - | "x86" -> if Configuration.model = "64" then - Machine.x86_64 - else - if Configuration.abi = "macosx" - then Machine.x86_32_macosx - else Machine.x86_32 - | "riscV" -> if Configuration.model = "64" - then Machine.rv64 - else Machine.rv32 - | _ -> assert false - end; - Builtins.set C2C.builtins; - Cutil.declare_attributes C2C.attributes; - CPragmas.initialize(); + Frontend.init (); parse_cmdline cmdline_actions; if !option_o <> None && !num_input_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; |