Changeset 3020 for driver/acc.ml


Ignore:
Timestamp:
Mar 28, 2013, 5:28:48 PM (7 years ago)
Author:
sacerdot
Message:
  • Options not used removed from the help/interface.
  • More compliance with the untrusted prototype.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/acc.ml

    r3015 r3020  
    5656  match Extracted.Compiler.compile observe cl with
    5757  | OK o -> o
    58   | Error m -> failwith (Error.errormsg m)
    59 in
    60 let labelled = output.Extracted.Compiler.c_labelled_clight in
    61 let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
    62 let s_costmap = output.Extracted.Compiler.c_stack_cost in
    63 let style = Cost_instrumented (l_costmap,s_costmap) in
    64 let instrumented = ClightPrinter.print_program style labelled in
    65 let filename = Filename.chop_extension filename ^ "-instrumented.c" in
    66 let och = open_out filename in
    67 output_string och instrumented;
    68 close_out och
     58  | Error m -> failwith (Error.errormsg m) in
     59if Options.annotation_requested () then
     60 begin
     61  let labelled = output.Extracted.Compiler.c_labelled_clight in
     62  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
     63  let s_costmap = output.Extracted.Compiler.c_stack_cost in
     64  let style = Cost_instrumented (l_costmap,s_costmap) in
     65  let instrumented = ClightPrinter.print_program style labelled in
     66  let filename = Filename.chop_extension filename ^ "-instrumented.c" in
     67  let och = open_out filename in
     68  output_string och instrumented;
     69  close_out och
     70 end
    6971) (OptionsParsing.results ())
Note: See TracChangeset for help on using the changeset viewer.