Changeset 3020 for driver/acc.ml

Timestamp:

Mar 28, 2013, 5:28:48 PM (8 years ago)

Author:

sacerdot

Message:

• Options not used removed from the help/interface.
• More compliance with the untrusted prototype.

File:

• driver/acc.ml (modified) (1 diff)

driver/acc.ml

@@ -56 +56 @@
   match Extracted.Compiler.compile observe cl with
   | OK o -> o
-  | Error m -> failwith (Error.errormsg m)
-in
-let labelled = output.Extracted.Compiler.c_labelled_clight in
-let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
-let s_costmap = output.Extracted.Compiler.c_stack_cost in
-let style = Cost_instrumented (l_costmap,s_costmap) in
-let instrumented = ClightPrinter.print_program style labelled in
-let filename = Filename.chop_extension filename ^ "-instrumented.c" in
-let och = open_out filename in
-output_string och instrumented;
-close_out och
+  | Error m -> failwith (Error.errormsg m) in
+if Options.annotation_requested () then
+ begin
+  let labelled = output.Extracted.Compiler.c_labelled_clight in
+  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
+  let s_costmap = output.Extracted.Compiler.c_stack_cost in
+  let style = Cost_instrumented (l_costmap,s_costmap) in
+  let instrumented = ClightPrinter.print_program style labelled in
+  let filename = Filename.chop_extension filename ^ "-instrumented.c" in
+  let och = open_out filename in
+  output_string och instrumented;
+  close_out och
+ end
 ) (OptionsParsing.results ())