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