src/clight/clightParser.ml

   1
   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
   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     Misc.SysExt.safe_remove tmp_file1;
  22     failwith "Error adding primitive prototypes."
  23   );
  24
  25   (* Preprocessing *)
  26   Cparser.Builtins.set Cparser.GCC.builtins;
  27   let rc = Sys.command
  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
  31   if rc <> 0 then (
  32     Misc.SysExt.safe_remove tmp_file1;
  33     Misc.SysExt.safe_remove tmp_file2;
  34     failwith "Error calling gcc."
  35   );
  36
  37   (* C to Cil *)
  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
  42   close_in ic;
  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)
  54
  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
  58   match r with
  59     | None -> failwith "Error during C parsing."
  60     | Some p ->
  61       (* Cil to Clight *)
  62       (match ClightFromC.convertProgram p with
  63         | None -> failwith "Error during C to Clight pass."
  64         | Some (pp) ->
  65           pp)
  66
  67 let process ?is_lustre_file ?remove_lustre_externals = function
  68   | `Filename file ->
  69     process_filename ?is_lustre_file ?remove_lustre_externals file
  70   | `Source (name, contents) ->
  71     process_source name contents
  72