Module Transfer_logic

module Transfer_logic: sig .. end

Check the postcondition of kf for the list of behaviors. This may result in splitting post_states if the postconditions contain disjunctions.

module type Domain = sig .. end

module ActiveBehaviors: sig .. end

val process_inactive_behaviors : Cil_types.kernel_function ->
       Cil_types.kinstr -> ActiveBehaviors.t -> unit

val process_inactive_postconds : Cil_types.kernel_function -> Cil_types.behavior list -> unit

module type S = sig .. end

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