Revision 820616b1
Added by Pierre-Loïc Garoche almost 4 years ago
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
Tiny verifier: better control of the print commands