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

  

Also available in: Unified diff