module type S = sig
.. end
type
state
type
states
type
active_behaviors
val create : state ->
Cil_types.kernel_function -> active_behaviors
val check_fct_preconditions : Cil_types.kernel_function ->
active_behaviors ->
Cil_types.kinstr ->
state -> states Eval.or_bottom
val check_fct_postconditions : Cil_types.kernel_function ->
active_behaviors ->
Cil_types.termination_kind ->
init_state:state ->
post_states:states ->
result:Cil_types.varinfo option -> states Eval.or_bottom
val interp_annot : limit:int ->
record:bool ->
Cil_types.kernel_function ->
active_behaviors ->
Cil_types.stmt ->
Cil_types.code_annotation ->
initial_state:state ->
states -> states