2 try Sys.remove name with Sys_error _ -> ()
4 let 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
10 (* Add CerCo's primitives *)
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 ;*)
18 with Sys_error _ -> failwith "Error adding primitive prototypes." in
20 (Printf.sprintf "cat %s >> %s"
21 (Filename.quote file) (Filename.quote tmp_file1)) in
23 safe_remove tmp_file1;
24 failwith "Error adding primitive prototypes."
28 Cparser.Builtins.set Cparser.GCC.builtins;
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
34 safe_remove tmp_file1;
35 safe_remove tmp_file2;
36 failwith "Error calling gcc."
40 let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
42 | None -> failwith "Error during C parsing."
45 (match ClightFromC.convertProgram p with
46 | None -> failwith "Error during C to Clight pass."
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*)