diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 510bf93..6e45240 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -929,6 +929,10 @@ end = struct let dc = pass_cycle e d2 in let y = edd_join_star_widen e x dc in + if e.opt.vverbose_ci then + Format.printf "d2 %a@. dc %a@. y %a@." + edd_print d2 edd_print dc edd_print y; + if e.opt.verbose_ci then Format.printf " -> %a@." edd_print y; @@ -945,7 +949,13 @@ end = struct let f i = let i = edd_meet path i in let i' = edd_meet i path_target in - let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in + let j = edd_apply_cl i' e.cl in + + if e.opt.vverbose_ci then + Format.printf "i %a@.i' %a@.j %a@." + edd_print i edd_print i' edd_print j; + + let q = edd_join start (pass_cycle e j) in edd_meet path q in |