Exec-block-item
Execute a block item.
- Signature
(exec-block-item item compst fenv limit)
→
(mv result new-compst)
- Arguments
- item — Guard (block-itemp item).
- compst — Guard (compustatep compst).
- fenv — Guard (fun-envp fenv).
- limit — Guard (natp limit).
- Returns
- result — Type (value-option-resultp result).
- new-compst — Type (compustatep new-compst).
Besides an optional value result,
we also return a possibly updated computation state.
If the block item is a declaration,
we ensure that it has no extern storage class specifier
(we do not support it in blocks),
then we execute the initializer (which we require here),
then we add the variable to the top scope of the top frame.
The initializer value must have the same type as the variable,
which automatically excludes the case of the variable being void,
since type-of-value never returns void
(under the guard).
For now we disallow array objects;
these will be supported later.
If the block item is a statement,
we execute it like any other statement.
