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