Frama-C API - Inout
val register_call_hook : (Frama_c_kernel.Inout_type.t -> unit) -> unitRegisters a hook to be called on the inputs/outputs computed by the Inout plugin for each function call.
val kf_inputs : Frama_c_kernel.Kernel_function.t -> Frama_c_kernel.Locations.Zone.tReturns the memory zone read by the given function (including local and formal variables). Returns Top if the inout plugin is missing.
val kf_outputs : Frama_c_kernel.Kernel_function.t -> Frama_c_kernel.Locations.Zone.tReturns the memory zone modified by the given function (including local and formal variables). Returns Top if the inout plugin is missing.
val stmt_outputs : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Locations.Zone.tReturns the memory zone modified by the given statement. Returns Top if the inout plugin is missing.