diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-05-04 19:52:43 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-05-04 19:52:43 +0200 |
commit | f0857720ae2be7f73c43f462a4a0f47ad20b5750 (patch) | |
tree | 5d1ea4909252c9475f2e85268d19b7605cf9a2d8 /backend/Inliningproof.v | |
parent | 338bbeace6ee351962e42172fd7c7acbcf5e785c (diff) | |
download | compcert-f0857720ae2be7f73c43f462a4a0f47ad20b5750.tar.gz compcert-f0857720ae2be7f73c43f462a4a0f47ad20b5750.zip |
Check that variables declared in 'for' loops are local variables (#104)
* Check for static and extern variables in for
The declaration inside of a for statement is not allowed to have
static or extern storage duration.
Bug 23330
* Also check that the declared variables don't have function types.
* Also checks that no typedefs occur in 'for' declarations.
* Simplify the `elab_declarations` function. It's used only to elaborate the whole program, and the resulting declarations and environment are ignored. So, replace `elab_declarations` by a simpler iteration over the program in `elab_program`.
Diffstat (limited to 'backend/Inliningproof.v')
0 files changed, 0 insertions, 0 deletions