Project

General

Profile

Revision 25537a17 src/tools/tiny/tiny_verifier.ml

View differences:

src/tools/tiny/tiny_verifier.ml
4 4
let tiny_help = ref false
5 5
let descending = ref 1
6 6
let unrolling = ref 0
7

  
7
let output = ref false
8 8

  
9 9
              
10 10
let quiet () = Tiny.Report.verbosity := 0
......
55 55
  let bounds_inputs = [] in
56 56
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
57 57
  let mems = m.mmemory in
58
  if !output then (
59
    let destname = !Options.dest_dir ^ "/" ^ basename ^ "_" ^ node_name ^ ".tiny" in
60
    Log.report ~plugin:"tiny" ~level:1 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
61
    let out = open_out destname in
62
    let fmt = Format.formatter_of_out_channel out in
63
    Format.fprintf fmt "%a@." Tiny.Ast.VarSet.pp env; 
64
    Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast; 
65
    close_out out;
58 66
  
59
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
60

  
61
   let dom =
67
  
68
  );
69
  Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
70
  
71
  let dom =
62 72
     let open Tiny.Load_domains in
63 73
     prepare_domains (List.map get_domain !domains)
64 74
   in
......
68 78
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
69 79
   let m = Results.results in
70 80
   (* if !Tiny.Report.verbosity > 1 then *)
71
   PrintResults.print m ast None (* no !output_file *);
81
   PrintResults.print m env ast None (* no !output_file *);
72 82
        (* else PrintResults.print_invariants m ast !output_file *)
73 83

  
74 84
   ()
......
116 126
         * is reached (default is 1)"); *)
117 127
      ("-unrolling", Arg.Set_int unrolling,
118 128
       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
129
      ("-output", Arg.Set output,
130
       "<n>  Export resulting tiny file as <name>_<mainnode>.tiny");
119 131
      (* (\* ("-u", Arg.Set_int unrolling,
120 132
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
121 133
       "-help", Arg.Set tiny_help, "tiny help and usage";

Also available in: Unified diff