Frama-C API - Transfer_logic
Interpretation of logic assertions, built by functor Transfer_logic.Make.
val create : state -> Frama_c_kernel.Cil_types.kernel_function -> Active_behaviors.tval create_from_spec : state -> Frama_c_kernel.Cil_types.spec -> 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 -> Alarmset.status -> state list -> state listval check_fct_preconditions : Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.kernel_function -> 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 -> Alarmset.status -> pre_state:state -> post_states:state list -> result:Eva_ast_types.varinfo option -> state listval check_fct_postconditions : Frama_c_kernel.Cil_types.kernel_function -> Active_behaviors.t -> Frama_c_kernel.Cil_types.termination_kind -> pre_state:state -> post_states:state list -> result:Eva_ast_types.varinfo option -> state listval evaluate_assumes_of_behavior : state -> Frama_c_kernel.Cil_types.behavior -> Alarmset.statusval interp_annot : record:bool -> Frama_c_kernel.Cil_types.kernel_function -> Active_behaviors.t -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.code_annotation -> initial_state:state -> state list -> state list