Module Transfer_logic

module Transfer_logic: sig .. end

Check the postcondition of kf for a given behavior b. This may result in splitting post_states if the postconditions contain disjunctions.

module type S = sig .. end

module Make: functor (Domain : Abstract_domain.S) -> functor (States : Partitioning.StateSet  with type state = Domain.t) -> S  with type state = Domain.t
       and type states = States.t