Frama-C API - Backward_formals
Functions related to the backward propagation of the value of formals at the end of a call. When possible, this value is propagated to the actual parameter.
val written_formals : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_datatype.Varinfo.Set.twritten_formals kf is an over-approximation of the formals of kf which may be internally overwritten by kf during its call.
val safe_argument : Eva_ast.exp -> boolsafe_argument e returns true if e (which is supposed to be an actual parameter) is guaranteed to evaluate in the same way before and after the call.