2 let process_filename ?is_lustre_file ?remove_lustre_externals file =
3 let temp_dir = Filename.dirname file in
4 let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
5 and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i"
6 and prepro_opts = [] in
8 (* Add CerCo's primitives *)
11 let oc = open_out tmp_file1 in
12 if is_lustre_file = Some true || remove_lustre_externals = Some true then
13 output_string oc "#include<string.h>";
14 output_string oc Primitive.prototypes ;
16 with Sys_error _ -> failwith "Error adding primitive prototypes." in
18 (Printf.sprintf "cat %s >> %s"
19 (Filename.quote file) (Filename.quote tmp_file1)) in
21 Misc.SysExt.safe_remove tmp_file1;
22 failwith "Error adding primitive prototypes."
26 Cparser.Builtins.set Cparser.GCC.builtins;
28 (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
29 (String.concat " " (List.map Filename.quote prepro_opts))
30 (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
32 Misc.SysExt.safe_remove tmp_file1;
33 Misc.SysExt.safe_remove tmp_file2;
34 failwith "Error calling gcc."
38 let ic = open_in tmp_file2 in
39 let lexbuf = Lexing.from_channel ic in
40 lexbuf.Lexing.lex_curr_p <- { lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = tmp_file2 };
41 let r = Cparser.Parse.preprocessed_file "CSf" file lexbuf in
44 | None -> failwith "Error during C parsing."
47 (match ClightFromC.convertProgram p with
48 | None -> failwith "Error during C to Clight pass."
50 Misc.SysExt.safe_remove tmp_file1;
51 Misc.SysExt.safe_remove tmp_file2;
52 if remove_lustre_externals = Some true then ClightLustre.simplify pp
55 let process_source name contents =
56 let lexbuf = Lexing.from_string contents in
57 let r = Cparser.Parse.preprocessed_file "CSf" name lexbuf in
59 | None -> failwith "Error during C parsing."
62 (match ClightFromC.convertProgram p with
63 | None -> failwith "Error during C to Clight pass."
67 let process ?is_lustre_file ?remove_lustre_externals = function
69 process_filename ?is_lustre_file ?remove_lustre_externals file
70 | `Source (name, contents) ->
71 process_source name contents