diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Configuration.ml | 28 | ||||
| -rw-r--r-- | driver/Configuration.mli | 21 | ||||
| -rw-r--r-- | driver/Frontend.ml | 6 |
3 files changed, 5 insertions, 50 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 48f8abde..972fd295 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -143,34 +143,6 @@ let stdlib_path = "" let asm_supports_cfi = get_bool_config "asm_supports_cfi" - -type struct_passing_style = - | SP_ref_callee (* by reference, callee takes copy *) - | SP_ref_caller (* by reference, caller takes copy *) - | SP_split_args (* by value, as a sequence of ints *) - -type struct_return_style = - | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) - | SR_int1to4 (* return by content if size is <= 4 *) - | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference - given as extra argument *) - -let struct_passing_style = - match get_config_string "struct_passing_style" with - | "ref-callee" -> SP_ref_callee - | "ref-caller" -> SP_ref_caller - | "ints" -> SP_split_args - | v -> bad_config "struct_passing_style" [v] - -let struct_return_style = - match get_config_string "struct_return_style" with - | "int1248" -> SR_int1248 - | "int1-4" -> SR_int1to4 - | "int1-8" -> SR_int1to8 - | "ref" -> SR_ref - | v -> bad_config "struct_return_style" [v] - type response_file_style = | Gnu (* responsefiles in gnu compatible syntax *) | Diab (* responsefiles in diab compatible syntax *) diff --git a/driver/Configuration.mli b/driver/Configuration.mli index b918c169..a71da72d 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -46,27 +46,6 @@ val has_runtime_lib: bool val has_standard_headers: bool (** True if CompCert's standard header files is available. *) - -type struct_passing_style = - | SP_ref_callee (* by reference, callee takes copy *) - | SP_ref_caller (* by reference, caller takes copy *) - | SP_split_args (* by value, as a sequence of ints *) - -type struct_return_style = - | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) - | SR_int1to4 (* return by content if size is <= 4 *) - | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference - given as extra argument *) - -val struct_passing_style: struct_passing_style - (** Calling conventions to use for passing structs and unions as - first-class values *) - -val struct_return_style: struct_return_style - (** Calling conventions to use for returning structs and unions as - first-class values *) - type response_file_style = | Gnu (* responsefiles in gnu compatible syntax *) | Diab (* responsefiles in diab compatible syntax *) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 2bc4f844..209e72e9 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -65,7 +65,9 @@ let init () = Machine.config:= begin match Configuration.arch with | "powerpc" -> if Configuration.gnu_toolchain - then Machine.ppc_32_bigendian + then if Configuration.abi = "linux" + then Machine.ppc_32_linux_bigendian + else Machine.ppc_32_bigendian else Machine.ppc_32_diab_bigendian | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian @@ -75,6 +77,8 @@ let init () = else if Configuration.abi = "macosx" then Machine.x86_32_macosx + else if Configuration.system = "bsd" + then Machine.x86_32_bsd else Machine.x86_32 | "riscV" -> if Configuration.model = "64" then Machine.rv64 |