|
|
|---|
|
|
|
|---|
Execute an assignment expression.
(exec-expr-asg e compst fenv limit) → new-compst
This is only used for expressions that must be assignments: we check that the expression is an assignment.
The left-hand side must be a pure lvalue expressions, i.e. its evaluation must return an expression value with an object designator. The right-hand side must be a pure expression (lvalue or not), but if the left-hand side is just an identifier, then we allow the right-hand side to be also a function call.
The just mentioned restrictions on the subexpressions are motivated by the fact that [C] does not prescribe the order of evaluation of left-hand side and right-hand side of assignment expressions, just like for any other binary operator; there are no sequence points [C:5.1.2.3] within assignments. Thus, if both sides are pure, the order of evaluation does not matter, and we can evaluate them in any order. The case of a left-hand side that is an identifier (i.e. variable) and a right-hand side that is a function call is allowed here because, even though the function call could modify the variable, its value is not actually used to perform the assignment: it is overwritten by the result of the function call. A function call cannot put a named variable into of out of existence, because that depends on scoping; thus, the successful or unsuccessul retrieval of the object designator of the named variable is the same whether it is performed before or after the function call. Therefore it does not matter in which order we evaluate the subexpressions of the assignment, also in the case in which we assign a function call to a variable. We should formally prove the fact mentioned just above that the existence of a named variable is not affected by a function call; this may be actually part of a larger plan to model and support assignments with arbitrary expressions, where our model will cover all possible evaluation orders, as done in other formalizations of C in the literature.
If the right-hand side is a function call,
we require it to return a value,
i.e. not
We allow these assignment expressions as the full expressions [C:6.8/4] of expression statements. Thus, we discard the value of the assignment (which is the value written to the variable); this ACL2 function just returns an updated computation state.