Changeset 2993 for driver/cerco.ml
- Timestamp:
- Mar 28, 2013, 9:56:26 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
driver/cerco.ml
r2964 r2993 34 34 35 35 let argv1 = Sys.argv.(1) in 36 let do_ print,filename,style =36 let do_exec,filename,style = 37 37 if argv1 = "-exec" then 38 38 true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented") … … 41 41 let cl = ClightParser.process filename in 42 42 let observe = 43 if do_print then 44 let rec infinity = Extracted.Nat.S infinity in 45 (fun pass prog -> 46 print_string (Printer.print_program pass prog); 43 let rec infinity = Extracted.Nat.S infinity in 44 (fun pass prog -> 45 if do_exec || pass = Extracted.Compiler.Clight_label_pass || 46 pass = Extracted.Compiler.Object_code_pass then 47 Printer.print_program filename pass prog; 48 if do_exec then 47 49 Extracted.Semantics.run_and_print pass prog infinity 48 (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); Extracted.Types.It) 49 (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It) 50 (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It) 51 (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It)) 52 else (fun _ _ -> Extracted.Types.It) 50 (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout; 51 Extracted.Types.It) 52 (fun evn -> print_string (string_of_intensional_event evn); flush stdout; 53 Extracted.Types.It) 54 (fun msg -> print_endline (Error.errormsg msg); flush stdout; 55 Extracted.Types.It) 56 (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n)); 57 flush stdout; Extracted.Types.It) 58 else 59 Extracted.Types.It) 53 60 in 54 61 let output =
Note: See TracChangeset
for help on using the changeset viewer.