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.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 : Cil_types.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.