Function-environments
C function environments.
C code is executed in the context of function definitions in scope,
which may be referenced by the code.
Here we formalize a notion of function environment as a finite map
from function names (i.e. identifiers)
to information about the functions.
These function environments are used in the dynamic semantics.
Subtopics
- Init-fun-env
- Initialize the function environment for a translation unit.
- Fun-info
- Fixtype of information about a C function in an environment.
- Fun-info-option
- Fixtype of optional information about a C function in an environment.
- Fun-env-extend
- Extend a function environment with a function definition.
- Fun-env-result
- Fixtype of errors and function environments.
- Fun-env-lookup
- Look up a function in an environment by name.
- Fun-info-from-fundef
- Create information for a function definition.
- Fun-env
- Fixtype of function environments.
