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 ActiveBehaviors: sig .. end
val process_inactive_behaviors : Cil_types.kinstr ->
Cil_types.kernel_function -> Cil_types.behavior list -> unit
module type S = sig .. end
module type LogicDomain = sig .. end
module Make: 
functor (Domain : LogicDomain) ->
functor (States : Powerset.S with type state = Domain.t) -> S with type state = Domain.t and type states = States.t