clightParser.ml

   1 let safe_remove name =
   2  try Sys.remove name with Sys_error _ -> ()
   3
   4 let process ?is_lustre_file ?remove_lustre_externals file =
   5   let temp_dir = Filename.dirname file in
   6   let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
   7   and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i"
   8   and prepro_opts = [] in
   9
  10   (* Add CerCo's primitives *)
  11   let _ =
  12     try
  13       let oc = open_out tmp_file1 in
  14       if is_lustre_file = Some true || remove_lustre_externals = Some true then
  15         output_string oc "#include<string.h>";
  16       (* FIXME output_string oc Primitive.prototypes ;*)
  17       close_out oc
  18     with Sys_error _ -> failwith "Error adding primitive prototypes." in
  19   let rc = Sys.command
  20     (Printf.sprintf "cat %s >> %s"
  21        (Filename.quote file) (Filename.quote tmp_file1)) in
  22   if rc <> 0 then (
  23     safe_remove tmp_file1;
  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     safe_remove tmp_file1;
  35     safe_remove tmp_file2;
  36     failwith "Error calling gcc."
  37   );
  38
  39   (* C to Cil *)
  40   let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
  41   match r with
  42     | None -> failwith "Error during C parsing."
  43     | Some p ->
  44       (* Cil to Clight *)
  45       (match ClightFromC.convertProgram p with
  46         | None -> failwith "Error during C to Clight pass."
  47         | Some(pp) ->
  48           safe_remove tmp_file1;
  49           safe_remove tmp_file2;
  50           if remove_lustre_externals = Some true then failwith "not implemented yet" (*ClightLustre.simplify pp*)
  51           else pp)