source: Deliverables/D2.2/8051/cparser/Main.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 3.3 KB
RevLine 
[486]1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Wrapper around gcc to parse, transform, pretty-print, and call gcc on result *)
17
18let transfs = ref ""
19
20let safe_remove name =
21  try Sys.remove name with Sys_error _ -> ()
22
23let process_c_file prepro_opts name =
24  let ppname = Filename.temp_file "cparser" ".i" in
25  let cpname = Filename.chop_suffix name ".c" ^ ".i" in
26  let rc =
27    Sys.command
28      (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
29                      (String.concat " " (List.map Filename.quote prepro_opts))
30                      (Filename.quote name) (Filename.quote ppname)) in
31  if rc <> 0 then begin
32    safe_remove ppname;
33    exit 2
34  end;
35  let r = Parse.preprocessed_file !transfs name ppname in
36  safe_remove ppname;
37  match r with
38  | None -> exit 2
39  | Some p -> 
40      let oc = open_out cpname in
41      let oform = Format.formatter_of_out_channel oc in
42      Cprint.program oform p;
43      close_out oc;
44      cpname
45
46let starts_with pref s =
47  String.length s >= String.length pref
48  && String.sub s 0 (String.length pref) = pref
49
50let ends_with suff s =
51  String.length s >= String.length suff
52  && String.sub s (String.length s - String.length suff) (String.length suff)
53     = suff
54
55let rec parse_cmdline prepro args i =
56  if i >= Array.length Sys.argv then List.rev args else begin
57    (* should skip arguments more cleanly... *)
58    let s = Sys.argv.(i) in
59    if s = "-Xsimplif" && i + 1 < Array.length Sys.argv then begin
60      transfs := Sys.argv.(i+1);
61      parse_cmdline prepro args (i+2)
62    end else if (s = "-I" || s = "-D" || s = "-U") 
63             && i + 1 < Array.length Sys.argv then 
64      parse_cmdline (Sys.argv.(i+1) :: s :: prepro) args (i+2)
65    else if starts_with "-I" s
66             || starts_with "-D" s
67             || starts_with "-U" s then
68      parse_cmdline (s :: prepro) args (i + 1)
69    else if s = "-Wall" then
70      parse_cmdline prepro ("-Wno-parentheses" :: "-Wall" :: args) (i+1)
71    else if ends_with ".c" s then begin
72      let s' = process_c_file (List.rev prepro) s in
73      parse_cmdline prepro (s' :: args) (i + 1)
74    end else
75      parse_cmdline prepro (s :: args) (i + 1)
76  end
77
78let _ =
79  Builtins.set GCC.builtins;
80  let args = parse_cmdline [] [] 1 in
81  let cmd = "gcc " ^ String.concat " " (List.map Filename.quote args) in
82  let rc = Sys.command cmd in
83  exit rc
Note: See TracBrowser for help on using the repository browser.