Module Backward_formals

module Backward_formals: sig .. end
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 : Cil_types.kernel_function -> Cil_datatype.Varinfo.Set.t
written_formals kf is an over-approximation of the formals of kf which may be internally overwritten by kf during its call.
val safe_argument : Cil_types.exp -> bool
safe_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.