private Context translateVariableAssign ( WyilFile . Expr . VariableAccess lval , Expr rval , Context context ) { WyilFile . Decl . Variable decl = lval . getVariableDeclaration ( ) ; context = context . havoc ( decl ) ; WyalFile . VariableDeclaration nVersionedVar = context . read ( decl ) ; Expr . VariableAccess var = new Expr . VariableAccess ( nVersionedVar ) ; return context . assume ( new Expr . Equal ( var , rval ) ) ; }
Translate an assignment to a variable