Changeset 3020 for driver

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.

Location:

driver

Files:

• acc.ml (modified) (1 diff)
• options.ml (modified) (8 diffs)
• options.mli (modified) (4 diffs)

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 ())

driver/options.ml

@@ -2 +2 @@
 let extra_doc s = "", Arg.Unit ignore, s
 
+(*
 let web_mode             = ref false
 let is_web_mode ()       = !web_mode
 let set_web_mode ()      = web_mode := true
+*)
 
+(*
 let default_choice       = "default"
 let option_settings_step = "during option settings"
 
-(*
 let language_from_string kind default s =
   try 
@@ -31 +33 @@
 *)
 
+(*
 let input_files                 = ref []
 let add_input_file f            = input_files := f :: !input_files
 let input_files ()              = !input_files
+*)
 
 let output_files                = ref None
@@ -43 +47 @@
 let annotation_requested ()     = !annotation_flag
 
+(*
 let interpretation_flag         = ref false
 let request_interpretation      = (:=) interpretation_flag
 let interpretation_requested () = !interpretation_flag
+*)
 
 let interpretations_flag         = ref false
@@ -51 +57 @@
 let interpretations_requested () = !interpretations_flag
 
+(*
 let debug_flag                  = ref false
 let set_debug                   = (:=) debug_flag
 let is_debug_enabled ()         = !debug_flag
+*)
 
+(*
 let asm_pretty_flag             = ref false
 let set_asm_pretty              = (:=) asm_pretty_flag
 let is_asm_pretty ()            = !asm_pretty_flag
+*)
 
 let lustre_flag                 = ref false
@@ -93 +103 @@
 *)
 
+(*
 let dev_test                    = ref false
 let set_dev_test                = (:=) dev_test
 let is_dev_test_enabled ()      = !dev_test
+*)
 
 let options = OptionsParsing.register [
@@ -113 +125 @@
   " Add cost annotations on the source code.";
 
+(*
   "-i", Arg.Set interpretation_flag,
   " Interpret the compiled code.";
+*)
 
   "-is", Arg.Set interpretations_flag,
-  " Interpret all the compilation passes.";
+  " Outputs and interprets all the compilation passes,";
+  extra_doc " showing the execution traces";
 
+(*
   "-d", Arg.Set debug_flag,
   " Debug mode.";
@@ -124 +140 @@
   extra_doc " Combined with an interpret option, shows the trace";
   extra_doc " of execution states.";
+*)
 
   "-o", Arg.String set_output_files,
   " Prefix of the output files.";
 
+(*
   "-asm-pretty", Arg.Set asm_pretty_flag,
   " Output a pretty-printed assembly file.";
+*)
 
   "-lustre", Arg.Set lustre_flag,
@@ -163 +182 @@
 *)
 
+(*
   "-dev", Arg.Set dev_test,
   " Playground for developers.";
+*)
 ]

driver/options.mli

@@ -11 +11 @@
 *)
 
+(*
 (** {2 Interpretation request} *)
 val request_interpretation   : bool -> unit
 val interpretation_requested : unit -> bool
+*)
 
 (** {2 Interpretation requests} *)
@@ -23 +25 @@
 val annotation_requested : unit -> bool
 
+(*
 (** {2 Input files} *)
 val add_input_file : string -> unit
 val input_files    : unit -> string list
+*)
 
 (** {2 Output files} *)
@@ -31 +35 @@
 val get_output_files : unit -> string option
 
+(*
 (** {2 Verbose mode} *)
 val is_debug_enabled : unit -> bool
+*)
 
+(*
 (** {2 Assembly pretty print} *)
 val set_asm_pretty : bool -> unit
 val is_asm_pretty  : unit -> bool
+*)
 
 (** {2 Lustre file} *)
@@ -71 +79 @@
 *)
 
+(*
 (** {2 Developers' playground} *)
 val is_dev_test_enabled : unit -> bool
+*)
 
+(*
 (** {2 Web application} *)
 val set_web_mode : unit -> unit
 val is_web_mode  : unit -> bool
+*)