setup_precondition_proxy kf p creates a new property for p at each syntactic call site of kf, representing the status of p at this particular call. p is considered proven if and only if all its instances are themselves proven.

setup_all_preconditions_proxies kf is equivalent to calling setup_precondition_proxy on all the requires of kf.

property_at_call kf p stmt returns the property corresponding to the status of the precondition p at the call stmt. If stmt is a call through a pointer, the property at this call is created automatically if needed. For direct calls, setup_precondition_proxy must have been called before.

all_call_preconditions_at create kf stmt returns the copies of all the requires of kf for the call statement at stmt. The first property in the tuple is the require, the second the copy at the call point. If warn_missing is true and a copy has not yet been created an error is raised.

Returns the set of functions that can be called at the given statement and for which a precondition has been specialized at this call. Those functions are registered when the function precondition_at_call is called.

replace_for_call pre stmt pre_at_call states that pre_at_call is the property corresponding to the status of pre at call stmt. The previous property, if any, is removed. Beware that this may also remove some already proved statuses