Merge branch 'master' into dwarf

Conflicts:
	Makefile
	driver/Driver.ml

1 files changed, 57 insertions, 0 deletions

diff --git a/driver/Configuration.mli b/driver/Configuration.mli
new file mode 100644
index 00000000..20c45518
--- /dev/null
+++ b/driver/Configuration.mli
@@ -0,0 +1,57 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 advanced_debug: bool
+  (** True if advanced debug is implement for the Target *)
+
+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 *)