blob: 41325368a3afcee2e33e738a9031a0693326f03e (
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
open Printf
(* Locate the .ini file, which is either in the same directory as
the executable or in the directory ../share *)
let ini_file_name =
try
Sys.getenv "COMPCERT_CONFIG"
with Not_found ->
let exe_dir = Filename.dirname Sys.executable_name in
let share_dir =
Filename.concat (Filename.concat exe_dir Filename.parent_dir_name)
"share" in
let share_compcert_dir =
Filename.concat share_dir "compcert" in
let search_path = [exe_dir;share_dir;share_compcert_dir] in
let files = List.map (fun s -> Filename.concat s "compcert.ini") search_path in
try
List.find Sys.file_exists files
with Not_found ->
begin
eprintf "Cannot find compcert.ini configuration file.\n";
exit 2
end
(* Read in the .ini file *)
let _ =
try
Readconfig.read_config_file ini_file_name
with
| Readconfig.Error(file, lineno, msg) ->
eprintf "Error reading configuration file %s.\n" ini_file_name;
eprintf "%s:%d:%s\n" file lineno msg;
exit 2
| Sys_error msg ->
eprintf "Error reading configuration file %s.\n" ini_file_name;
eprintf "%s\n" msg;
exit 2
let get_config key =
match Readconfig.key_val key with
| Some v -> v
| None -> eprintf "Configuration option `%s' is not set\n" key; exit 2
let bad_config key vl =
eprintf "Invalid value `%s' for configuration option `%s'\n"
(String.concat " " vl) key;
exit 2
let get_config_string key =
match get_config key with
| [v] -> v
| vl -> bad_config key vl
let get_config_list key =
match get_config key with
| [] -> bad_config key []
| vl -> vl
let prepro = get_config_list "prepro"
let asm = get_config_list "asm"
let linker = get_config_list "linker"
let arch =
match get_config_string "arch" with
| "powerpc"|"arm"|"ia32" as a -> a
| v -> bad_config "arch" [v]
let model = get_config_string "model"
let abi = get_config_string "abi"
let system = get_config_string "system"
let has_runtime_lib =
match get_config_string "has_runtime_lib" with
| "true" -> true
| "false" -> false
| v -> bad_config "has_runtime_lib" [v]
let has_standard_headers =
match get_config_string "has_standard_headers" with
| "true" -> true
| "false" -> false
| v -> bad_config "has_standard_headers" [v]
let stdlib_path =
if has_runtime_lib then
get_config_string "stdlib_path"
else
""
let asm_supports_cfi =
match get_config_string "asm_supports_cfi" with
| "true" -> true
| "false" -> false
| v -> bad_config "asm_supports_cfi" [v]
let advanced_debug =
match get_config_string "advanced_debug" with
| "true" -> true
| "false" -> false
| v -> bad_config "advanced_debug" [v]
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]
|
