Frama-C API - Inout
val expr_inputs : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Locations.Zone.tReturns the memory zone needed to evaluate the given expression at the given statement.
val stmt_inputs : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Locations.Zone.tReturns the memory zone read by the given statement.
val stmt_outputs : Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Locations.Zone.tReturns the memory zone modified by the given statement.
val kf_inputs : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Locations.Zone.tReturns the memory zone read by the given function, including its local and formal variables.
val kf_external_inputs : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Locations.Zone.tReturns the memory zone read by the given function, without its local and formal variables.
val kf_outputs : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Locations.Zone.tReturns the memory zone modified by the given function, including its local and formal variables.
val kf_external_outputs : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Locations.Zone.tReturns the memory zone modified by the given function, without its local and formal variables.
val get_precise_inout : ?stmt:Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Inout_type.tReturns the inputs/outputs computed for the given function. If stmt is specified and is a possible call to the given function, returns the inputs/outputs for this call specifically.
val self : Frama_c_kernel.State.t