From a6038ae9bae41526224c2416332c719f26261812 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
Date: Thu, 11 Jan 2018 15:15:43 +0100
Subject: Move machine initialization to Frontend.init function. (#49)

The initialization of Machine.config, as well as the calls to various initialization functions for the C front-end, are now performed by the new `Frontend.init` function.
This avoids code duplication in driver/Driver.ml and exportclight/Clightgen.ml.
---
 driver/Driver.ml          | 23 +----------------------
 driver/Frontend.ml        | 25 +++++++++++++++++++++++++
 driver/Frontend.mli       |  3 +++
 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";
-- 
cgit