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_utils.ml
1
let report = Log.report ~plugin:"tiny"
1 2

  
3
           
2 4
module Ast = Tiny.Ast
3 5

  
4 6
let gen_loc () = Tiny.Location.dummy ()
......
163 165
                                over-approximate behavior *)
164 166
       in
165 167
       if (match init_var, te.Ast.expr_desc with
166
           | Some v, Var v2 -> Format.eprintf "Building init (possibly if %b)@." (v=v2); v = v2
167
           | _ -> Format.eprintf "Building if init def? %b @." (match init_var with None -> false | _ -> true); false) then 
168
           | Some v, Var v2 ->
169
              (* Format.eprintf "Building init (possibly if %b)@." (v=v2);  *)v = v2
170
           | _ ->
171
              (* Format.eprintf "Building if init def? %b @." (match init_var with None -> false | _ -> true);
172
               *)
173
              false
174
          )
175
       then 
168 176
         instrl_to_stm (
169 177
             if init then
170 178
               (List.assoc "true" guarded_instrs)
......
267 275
  
268 276
let machine_to_env m =
269 277
  List.fold_left (fun accu v ->
270
      Format.eprintf "Adding variable %a to env@." Printers.pp_var v;
278
      report ~level:3 (fun fmt -> Format.fprintf fmt "Adding variable %a to env@." Printers.pp_var v);
271 279
      let typ =
272 280
        ltyp_to_ttyp (v.Lustre_types.var_type)
273 281
      in
274
      Ast.VarSet.add (v.var_id, typ) accu)
275
    Ast.VarSet.empty
282
      Ast.Var.Set.add (v.var_id, typ) accu)
283
    Ast.Var.Set.empty
276 284
    (Machine_code_common.machine_vars m)
277 285

  
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