propagate code attributes to written variables by corresponding statement

If the user puts some attribute to a loop statement or a call, then in the VC computation, such an attribute is propagated to the variables written by this statement.

A use case is for counterexample generated : variables representing the values after loops or after calls, for written variables, hold the corresponding attribute, making easier to identify at which statement this value corresponds.