Stmt-value
Fixtype of statement values.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :none → stmt-value-none
- :return → stmt-value-return
In our dynamic semantics,
a statement may end its execution
by moving to the next statement without yielding a value,
by returning no value,
or by returning a value;
in full C, there are other ways in which a statement may end its execution,
but here we only focus on our formalized subset.
We capture this notion as a statement value,
i.e. the value yielded by a statement.
Note the distinction between yielding no value without a return,
e.g. after executing a null or expression statement (e.g. assignment),
and returning without a value,
i.e. with a return without expression.
The distinction affects how execution proceeds
just after the statement in question.
Subtopics
- Stmt-value-case
- Case macro for the different kinds of stmt-value structures.
- Stmt-value-fix
- Fixing function for stmt-value structures.
- Stmt-value-equiv
- Basic equivalence relation for stmt-value structures.
- Stmt-value-return
- Stmt-valuep
- Recognizer for stmt-value structures.
- Stmt-value-none
- Stmt-value-kind
- Get the kind (tag) of a stmt-value structure.
