diff --git a/domains/value_domain.ml b/domains/value_domain.ml index 0d2e342..d68edcb 100644 --- a/domains/value_domain.ml +++ b/domains/value_domain.ml @@ -158,8 +158,15 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct let rec revise_HC4 tree mapenv newval = match tree with | HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval)) - | HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in - meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) + | HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin + Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ " + V.print (get_abst sub1) + (Cfg_printer.string_of_int_binary_op bop) + V.print (get_abst sub2) + V.print (V.meet abst newval) + V.print (refined1) + V.print (refined2); + meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) end | HC4_int_var (v, abst) -> E (VMap.add v (V.meet abst newval) mapenv) | HC4_int_const (z,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv | HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv @@ -174,6 +181,13 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct | Bot -> Bot | E mapenv -> let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in ( + Format.printf "Refined comparison %a%s%a as %a%s%a@ " + V.print (get_abst hc4_1) + (Cfg_printer.string_of_compare_op cop) + V.print (get_abst hc4_2) + V.print newval1 + (Cfg_printer.string_of_compare_op cop) + V.print newval2; meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) ) let guard env boolexp = guard_noneg env (rm_negations boolexp)