aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-03-20 11:25:30 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-03-20 11:25:30 +0100
commitcbf8434e44ebd6bc05022d1fbe0400267520184f (patch)
treea73d9d6d0601935cf514698cdc393d131df7a341 /driver/Configuration.mli
parent42e397bd80389c7e7259f962415769b06561bb5d (diff)
downloadcompcert-kvx-cbf8434e44ebd6bc05022d1fbe0400267520184f.tar.gz
compcert-kvx-cbf8434e44ebd6bc05022d1fbe0400267520184f.zip
Improvements in the StructReturn transformation (ABI conformance for passing composites).
- Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
Diffstat (limited to 'driver/Configuration.mli')
-rw-r--r--driver/Configuration.mli55
1 files changed, 55 insertions, 0 deletions
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
new file mode 100644
index 00000000..875bd692
--- /dev/null
+++ b/driver/Configuration.mli
@@ -0,0 +1,55 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
+(* is distributed under the terms of the INRIA Non-Commercial *)
+(* License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+val arch: string
+ (** Target architecture *)
+val model: string
+ (** Sub-model for this architecture *)
+val abi: string
+ (** ABI to use *)
+val system: string
+ (** Flavor of operating system that runs CompCert *)
+
+val prepro: string list
+ (** How to invoke the external preprocessor *)
+val asm: string list
+ (** How to invoke the external assembler *)
+val linker: string list
+ (** How to invoke the external linker *)
+val asm_supports_cfi: bool
+ (** True if the assembler supports Call Frame Information *)
+val stdlib_path: string
+ (** Path to CompCert's library *)
+val has_runtime_lib: bool
+ (** True if CompCert's library is available. *)
+
+val version: string
+ (** CompCert version string *)
+
+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 *)