aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Configuration.mli
blob: f82ce213b60fedbd5d3b82c2d7086c18b8fd4783 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
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 has_standard_headers: bool
  (** True if CompCert's standard header files is available. *)
val advanced_debug: bool
  (** True if advanced debug is implement for the Target *)


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 *)