# 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 [C: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 things 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.

[C] 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.