|
|
|---|
|
|
|
|---|
Implementation environments for C.
Some aspects of the syntax and semantics of C are implementation-dependent. [C:5] introduces the notion of translation and execution environments, which specify those aspects. In our formalization, we introduce a notion of implementation environment, which puts together the translation and execution environments in [C]. That is, an implementation environment specifies the implementation-dependent aspects of C. We prefer to formalize one (implementation) environment, instead of two (translation and execution) environments, because the latter two share several aspects (e.g. integer sizes), and therefore it seems simpler to have one notion.
We start by capturing some aspects of the C implementation environment. More will be added in the future.
Initially, our formalization of implementation environments is not used in other parts of the C formalization; furthermore, it captures notions already captured elsewhere, such as the integer formats. But we plan to update the rest of the formalization to use this, also removing those then-redundant parts.