diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index e55f199..383a69c 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -29,29 +29,30 @@ end = struct (* init state *) let init_state widen_delay rp = - let f = Formula.eliminate_not (Transform.f_of_prog rp false) in - let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in - let env = List.fold_left (fun env (_, id, ty) -> E.addvar env id ty) E.init rp.all_vars in - let init_f = Transform.init_f_of_prog rp in - let guarantees = Transform.guarantees_of_prog rp in + Format.printf "Vars: @[<hov>%a@]@.@." + (Ast_printer.print_list Ast_printer.print_typed_var ", ") + rp.all_vars; + let init_f = Transform.init_f_of_prog rp in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; - Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; - Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g; - - Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars; + let guarantees = Transform.guarantees_of_prog rp in Format.printf "Guarantees:@."; List.iter (fun (id, f) -> Format.printf " %s: %a@." id Formula_printer.print_expr f) guarantees; Format.printf "@."; + let f = Formula.eliminate_not (Transform.f_of_prog rp false) in + let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g; + let env = E.set_disjunct env "/exit" DNever in let env = E.apply_f env init_f in |