private AssumptionSet updateVariableVersions ( AssumptionSet assumptions , LocalEnvironment original , LocalEnvironment updated ) { for ( Map . Entry < WyilFile . Decl . Variable , WyalFile . VariableDeclaration > e : updated . locals . entrySet ( ) ) { WyilFile . Decl . Variable var = e . getKey ( ) ; WyalFile . VariableDeclaration newVarVersionedName = e . getValue ( ) ; WyalFile . VariableDeclaration oldVarVersionedName = original . read ( var ) ; if ( ! oldVarVersionedName . equals ( newVarVersionedName ) ) { // indicates a version change of the given variable. Expr . VariableAccess oldVar = new Expr . VariableAccess ( oldVarVersionedName ) ; Expr . VariableAccess newVar = new Expr . VariableAccess ( newVarVersionedName ) ; assumptions = assumptions . add ( new Expr . Equal ( newVar , oldVar ) ) ; } } return assumptions ; }
Bring a given assumption set which is consistent with an original environment up - to - date with a new environment .