Changeset 2874 for driver

Timestamp:

Mar 14, 2013, 10:46:38 PM (7 years ago)

Author:

sacerdot

Message:

Syntax fixed: ./cerco [-exec] filename annotationoption

File:

• driver/cerco.ml (modified) (3 diffs)

driver/cerco.ml

@@ -32 +32 @@
 
 let argv1 = Sys.argv.(1) in
-let do_print,filename =
+let do_print,filename,style =
  if argv1 = "-exec" then
-  true,Sys.argv.(2)
+  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
  else
-  false,argv1 in
+  false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
 let cl = ClightParser.process filename in
 let observe =
@@ -59 +59 @@
 let s_costmap = output.Extracted.Compiler.c_stack_cost in
 let style =
-  match try Sys.argv.(2) with _ -> "instrumented" with
+  match style with
   | "plain" -> Cost_plain
   | "numbered" -> Cost_numbered (l_costmap,s_costmap)
@@ -68 +68 @@
 print_newline ();
 print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
-