Frama-C API - Transfer_logic
type state = Dom.tval create : state -> Frama_c_kernel.Cil_types.kernel_function -> Eva__.Active_behaviors.tval create_from_spec : state -> Frama_c_kernel.Cil_types.spec -> Eva__.Active_behaviors.tval check_fct_preconditions_for_behaviors : Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.behavior list -> Frama_c_kernel.Abstract_interp.Comp.result -> state list -> state listval check_fct_preconditions : Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.kernel_function -> Eva__.Active_behaviors.t -> state -> state listval check_fct_postconditions_for_behaviors : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.behavior list -> Frama_c_kernel.Abstract_interp.Comp.result -> pre_state:state -> post_states:state list -> result:Frama_c_kernel.Cil_types.varinfo option -> state listval check_fct_postconditions : Frama_c_kernel.Cil_types.kernel_function -> Eva__.Active_behaviors.t -> Frama_c_kernel.Cil_types.termination_kind -> pre_state:state -> post_states:state list -> result:Frama_c_kernel.Cil_types.varinfo option -> state listval evaluate_assumes_of_behavior : state -> Frama_c_kernel.Cil_types.behavior -> Frama_c_kernel.Abstract_interp.Comp.resultval interp_annot : record:bool -> Frama_c_kernel.Cil_types.kernel_function -> Eva__.Active_behaviors.t -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.code_annotation -> initial_state:state -> state list -> state list