Changeset 3026


Ignore:
Timestamp:
Mar 28, 2013, 11:58:34 PM (4 years ago)
Author:
sacerdot
Message:

With -a we now produce also the .cerco file required by the plug-in.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/acc.ml

    r3025 r3026  
    6464  let style = Cost_instrumented (l_costmap,s_costmap) in
    6565  let instrumented = ClightPrinter.print_program style labelled in
    66   let filename =
     66  let basename =
    6767   (match Options.get_output_files () with
    6868      None -> Filename.chop_extension filename
    69     | Some s -> s) ^ "-instrumented.c" in
    70   let och = open_out filename in
     69    | Some s -> s) in
     70  let och = open_out (basename ^ "-instrumented.c") in
    7171  output_string och instrumented;
     72  close_out och;
     73  let och = open_out (basename ^ ".cerco") in
     74  output_string och "__cost\n";
     75  output_string och "__cost_incr\n";
    7276  close_out och
    7377 end
Note: See TracChangeset for help on using the changeset viewer.