Frama-C API - Transfer_logic
val process_inactive_behaviors : Frama_c_kernel.Cil_types.kinstr -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.behavior list -> unitval check_calls_annotations : Frama_c_kernel.Cil_types.stmt -> (Frama_c_kernel.Cil_types.kernel_function * 'a) list -> (Frama_c_kernel.Cil_types.kernel_function * 'a) listmodule type LogicDomain = sig ... endmodule Make (Domain : LogicDomain) : Engine_sig.Transfer_logic with type state = Domain.t