source: Deliverables/D2.2/8051/src/clight/clightParser.ml

Last change on this file was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 1.7 KB
Line 
1
2let process ?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
7
8  (* Add CerCo's primitives *)
9  let _ =
10    try
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 ;
15      close_out oc
16    with Sys_error _ -> failwith "Error adding primitive prototypes." in
17  let rc = Sys.command
18    (Printf.sprintf "cat %s >> %s"
19       (Filename.quote file) (Filename.quote tmp_file1)) in
20  if rc <> 0 then (
21    (*
22    Misc.SysExt.safe_remove tmp_file1;
23    *)
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    (*
35    Misc.SysExt.safe_remove tmp_file1;
36    Misc.SysExt.safe_remove tmp_file2;
37    *)
38    failwith "Error calling gcc."
39  );
40
41  (* C to Cil *)
42  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
43  match r with
44    | None -> failwith "Error during C parsing."
45    | Some p ->
46      (* Cil to Clight *)
47      (match ClightFromC.convertProgram p with
48        | None -> failwith "Error during C to Clight pass."
49        | Some(pp) ->
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
53          else pp)
Note: See TracBrowser for help on using the repository browser.