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

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

32 and 16 bits operations support in D2.2/8051

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