This PR changes the backtranslation of procedure contracts.
When backtranslating contracts from Boogie (which has modifies clauses to encode frame conditions) to C/ACSL (where our contracts currently do not have modifies or other features for frame conditions), we add conjuncts of the form x == \old(x) for variables that are not modifiable by the procedure.
To support this, we add a specialized method for contract backtranslation to the ITranslator interface.
This PR changes the backtranslation of procedure contracts.
modifiesclauses to encode frame conditions) to C/ACSL (where our contracts currently do not havemodifiesor other features for frame conditions), we add conjuncts of the formx == \old(x)for variables that are not modifiable by the procedure.ITranslatorinterface.