source: driver/clightParser.ml @ 3094

Last change on this file since 3094 was 3013, checked in by sacerdot, 7 years ago

Temporary parsing files removed.

File size: 1.7 KB
Line 
1let safe_remove name =
2 try Sys.remove name with Sys_error _ -> ()
3
4let process ?is_lustre_file ?remove_lustre_externals file = 
5  let temp_dir = Filename.dirname file in
6  let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
7  and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i" 
8  and prepro_opts = [] in
9
10  (* Add CerCo's primitives *)
11  let _ =
12    try
13      let oc = open_out tmp_file1 in
14      if is_lustre_file = Some true || remove_lustre_externals = Some true then
15        output_string oc "#include<string.h>";
16      (* FIXME output_string oc Primitive.prototypes ;*)
17      close_out oc
18    with Sys_error _ -> failwith "Error adding primitive prototypes." in
19  let rc = Sys.command
20    (Printf.sprintf "cat %s >> %s"
21       (Filename.quote file) (Filename.quote tmp_file1)) in
22  if rc <> 0 then (
23    safe_remove tmp_file1;
24    failwith "Error adding primitive prototypes."
25  );
26
27  (* Preprocessing *)
28  Cparser.Builtins.set Cparser.GCC.builtins;
29  let rc = Sys.command
30    (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
31       (String.concat " " (List.map Filename.quote prepro_opts))
32       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
33  if rc <> 0 then (
34    safe_remove tmp_file1;
35    safe_remove tmp_file2;
36    failwith "Error calling gcc."
37  );
38
39  (* C to Cil *)
40  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
41  match r with
42    | None -> failwith "Error during C parsing."
43    | Some p ->
44      (* Cil to Clight *)
45      (match ClightFromC.convertProgram p with
46        | None -> failwith "Error during C to Clight pass."
47        | Some(pp) ->
48          safe_remove tmp_file1;
49          safe_remove tmp_file2;
50          if remove_lustre_externals = Some true then failwith "not implemented yet" (*ClightLustre.simplify pp*)
51          else pp)
Note: See TracBrowser for help on using the repository browser.