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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 1.4 KB
Line 
1let process file = 
2  let tmp_file1 = Filename.temp_file "cparser1" ".c"
3  and tmp_file2 = Filename.temp_file "cparser2" ".i" 
4  and prepro_opts = [] in
5
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
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))
26       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
27  if rc <> 0 then (
28    Misc.SysExt.safe_remove tmp_file1;
29    Misc.SysExt.safe_remove tmp_file2;
30    failwith "Error calling gcc."
31  );
32
33  (* C to Cil *)
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;
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
44      ) 
Note: See TracBrowser for help on using the repository browser.