diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-20 11:25:30 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-20 11:25:30 +0100 |
commit | cbf8434e44ebd6bc05022d1fbe0400267520184f (patch) | |
tree | a73d9d6d0601935cf514698cdc393d131df7a341 /driver/Configuration.mli | |
parent | 42e397bd80389c7e7259f962415769b06561bb5d (diff) | |
download | compcert-cbf8434e44ebd6bc05022d1fbe0400267520184f.tar.gz compcert-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.mli | 55 |
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 *) |