diff --git a/src/dune b/src/dune index 6b3766013..09b365c02 100644 --- a/src/dune +++ b/src/dune @@ -4,7 +4,7 @@ (public_name goblint-cil) (name goblintCil) (libraries zarith findlib dynlink unix str stdlib-shims) - (modules (:standard \ main ciloptions machdepConfigure modelConfigure)) + (modules (:standard \ main ciloptions machdepConfigure machdepArchConfigure modelConfigure)) ) (executable @@ -21,6 +21,21 @@ (target machdep-ml.exe) (action (run %{read-lines:../bin/real-gcc} -D_GNUCC machdep-ml.c -o %{target}))) +(executable + (name machdepArchConfigure) + (modules machdepArchConfigure) + (libraries dune-configurator)) + +(rule + (deps machdep-config.h machdep-ml.c) + (target machdep32) + (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 32)))) + +(rule + (deps machdep-config.h machdep-ml.c) + (target machdep64) + (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64)))) + ; for Cilly.pm (executable (name modelConfigure) @@ -40,6 +55,7 @@ (action (with-stdout-to %{target} (run ./modelConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64)))) (rule + (deps machdep32 machdep64) (target machdep.ml) (action (run %{bin:cppo} -V OCAML:%{ocaml_version} %{dep:machdep.cppo.ml} -x machdep:./%{dep:machdep-ml.exe} diff --git a/src/machdep.cppo.ml b/src/machdep.cppo.ml index 45d734e93..b00ef8cfc 100644 --- a/src/machdep.cppo.ml +++ b/src/machdep.cppo.ml @@ -56,4 +56,11 @@ let gcc = { #ext machdep #endext } + +let gcc32 = +#include "machdep32" + +let gcc64 = +#include "machdep64" + let theMachine : mach ref = ref gcc diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml new file mode 100644 index 000000000..ebf4ee0e7 --- /dev/null +++ b/src/machdepArchConfigure.ml @@ -0,0 +1,20 @@ +module C = Configurator.V1 + +let () = + let real_gcc = ref "" in + let m = ref "" in + let args = Arg.[ + ("--real-gcc", Set_string real_gcc, ""); + ("-m", Set_string m, ""); + ] + in + C.main ~name:"model" ~args (fun c -> + let exe = "./machdep-ml" ^ !m ^ ".exe" in + let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in + if exit_code = 0 then ( + let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in + Printf.printf "Some {%s}" stdout + ) + else + Printf.printf "None" + )