		Search-engine friendly clone of the ACL2 documentation.

Values

Expr-value

Fixtype of expression values.

This is a product type introduced by fty::defprod.

Fields

value — value
object — objdesign-option

An expression may yield a value or designate an object [C17:6.5/1] (unless the expression has void type). In our model, we have object designators to designate objects; see objdesign. When an expression designates an object, that object should exist: in our defensive dynamic semantics of C, we want in fact to ensure that that is the case: thus, when we evaluate an expression that designates an object (as opposed to an expression that just returns a value), in our dynamic semantics we also retrieve the value, to ensure that it exists, and to ensure that any subsequent operation is type-safe.

Thus, we introduce a notion of expression value as the thing returned by evaluating an expression in our dynamic semantics. An expression value consists of a value and an optional object designator: an expression that returns just a value in C returns an expression value without object designator in our model; an expression that designates an object in C returns an expression value with an object designator in our model, along with the value of the object. Having the value, in addition to the object designator, makes it convenient to access the value, without having to read it from the computation state.

[C17] does not provide a specific term to denote something returned by an expression, i.e. something that is either a value or an object designator. In our model, we formalize that as an expression value, which is essentially an extended notion of value as it pertains to expressions, which includes values proper and object designators.

Subtopics

Expr-value-fix: Fixing function for expr-value structures.
Expr-value-equiv: Basic equivalence relation for expr-value structures.
Expr-valuep: Recognizer for expr-value structures.
Make-expr-value: Basic constructor macro for expr-value structures.
Expr-value->object: Get the object field from a expr-value.
Expr-value->value: Get the value field from a expr-value.
Change-expr-value: Modifying constructor for expr-value structures.