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