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.