private Context translateArrayAssign ( WyilFile . Expr . ArrayAccess lval , Expr rval , Context context ) { // Translate src and index expressions Pair < Expr , Context > p1 = translateExpressionWithChecks ( lval . getFirstOperand ( ) , null , context ) ; Pair < Expr , Context > p2 = translateExpressionWithChecks ( lval . getSecondOperand ( ) , null , p1 . second ( ) ) ; Expr source = p1 . first ( ) ; Expr index = p2 . first ( ) ; // Emit verification conditions to check access in bounds checkExpressionPreconditions ( lval , p2 . second ( ) ) ; // Construct array update for "pass thru" Expr . Operator update = new Expr . ArrayUpdate ( source , index , rval ) ; return translateSingleAssignment ( ( LVal ) lval . getFirstOperand ( ) , update , p2 . second ( ) ) ; }
Translate an assignment to an array element .