blob: 3fe22fac2d7905129cfbc350adfcc959136782bc (
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Printf
open Clflags
(* Invocation of external tools *)
let rec waitpid_no_intr pid =
try Unix.waitpid [] pid
with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid
let command ?stdout args =
if !option_v then begin
eprintf "+ %s" (String.concat " " args);
begin match stdout with
| None -> ()
| Some f -> eprintf " > %s" f
end;
prerr_endline ""
end;
let argv = Array.of_list args in
assert (Array.length argv > 0);
try
let fd_out =
match stdout with
| None -> Unix.stdout
| Some f ->
Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
let pid =
Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
let (_, status) =
waitpid_no_intr pid in
if stdout <> None then Unix.close fd_out;
match status with
| Unix.WEXITED rc -> rc
| Unix.WSIGNALED n | Unix.WSTOPPED n ->
eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
with Unix.Unix_error(err, fn, param) ->
eprintf "Error executing '%s': %s: %s %s\n"
argv.(0) fn (Unix.error_message err) param;
-1
let command_error n exc =
eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc
let safe_remove file =
try Sys.remove file with Sys_error _ -> ()
(* Determine names for output files. We use -o option if specified
and if this is the final destination file (not a dump file).
Otherwise, we generate a file in the current directory. *)
let output_filename ?(final = false) source_file source_suffix output_suffix =
match !option_o with
| Some file when final -> file
| _ ->
Filename.basename (Filename.chop_suffix source_file source_suffix)
^ output_suffix
(* A variant of [output_filename] where the default output name is fixed *)
let output_filename_default default_file =
match !option_o with
| Some file -> file
| None -> default_file
(* All input files should exist *)
let ensure_inputfile_exists name =
if not (Sys.file_exists name) then begin
eprintf "error: no such file or directory: '%s'\n" name;
exit 2
end
(* Printing of error messages *)
let print_error oc msg =
let print_one_error = function
| Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
| Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
| Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
in
List.iter print_one_error msg;
output_char oc '\n'
let gnu_system = Configuration.system <> "diab"
(* Command-line parsing *)
let explode_comma_option s =
match Str.split (Str.regexp ",") s with
| [] -> assert false
| _ :: tl -> tl
(* Record actions to be performed after parsing the command line *)
let actions : ((string -> string) * string) list ref = ref []
let push_action fn arg =
actions := (fn, arg) :: !actions
let push_linker_arg arg =
push_action (fun s -> s) arg
let perform_actions () =
let rec perform = function
| [] -> []
| (fn, arg) :: rem -> let res = fn arg in res :: perform rem
in perform (List.rev !actions)
|
