Project

General

Profile

« Previous | Next » 

Revision 820616b1

Added by Pierre-Loïc Garoche 8 months ago

Tiny verifier: better control of the print commands

View differences:

src/tools/tiny/tiny_verifier.ml
8 8

  
9 9
              
10 10
let quiet () = Tiny.Report.verbosity := 0
11
             
11
let report = Tiny_utils.report
12
               
12 13
let print_tiny_help () =
13 14
  let open Format in
14 15
  Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
......
57 58
  let mems = m.mmemory in
58 59
  if !output then (
59 60
    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
    report ~level:2 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
61 62
    let out = open_out destname in
62 63
    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.Var.Set.pp env; 
64 65
    Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast; 
65 66
    close_out out;
66 67
  
67 68
  
68 69
  );
69
  Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
70
  report ~level:1 (fun fmt -> Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast); 
70 71
  
71 72
  let dom =
72 73
     let open Tiny.Load_domains in
......
78 79
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
79 80
   let m = Results.results in
80 81
   (* if !Tiny.Report.verbosity > 1 then *)
81
   PrintResults.print m env ast None (* no !output_file *);
82
   report ~level:1 (PrintResults.print m env ast)
83
   (* no !output_file *);
82 84
        (* else PrintResults.print_invariants m ast !output_file *)
83 85

  
84 86
   ()

Also available in: Unified diff