Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 years ago)
Author:
ayache
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r818 r1462  
    1 let process file =
    2   let tmp_file1 = Filename.temp_file "cparser1" ".c"
    3   and tmp_file2 = Filename.temp_file "cparser2" ".i"
     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"
    46  and prepro_opts = [] in
    57
     
    810    try
    911      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>";
    1014      output_string oc Primitive.prototypes ;
    1115      close_out oc
     
    1519       (Filename.quote file) (Filename.quote tmp_file1)) in
    1620  if rc <> 0 then (
     21    (*
    1722    Misc.SysExt.safe_remove tmp_file1;
     23    *)
    1824    failwith "Error adding primitive prototypes."
    1925  );
     
    2632       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    2733  if rc <> 0 then (
     34    (*
    2835    Misc.SysExt.safe_remove tmp_file1;
    2936    Misc.SysExt.safe_remove tmp_file2;
     37    *)
    3038    failwith "Error calling gcc."
    3139  );
     
    3341  (* C to Cil *)
    3442  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;
    3743  match r with
    3844    | None -> failwith "Error during C parsing."
     
    4147      (match ClightFromC.convertProgram p with
    4248        | None -> failwith "Error during C to Clight pass."
    43         | Some(pp) -> pp
    44       )
     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 TracChangeset for help on using the changeset viewer.