diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-03 16:01:20 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-07 08:57:22 +0100 |
commit | 35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5 (patch) | |
tree | c89a0466e9ab0c68baa7d4d41e21549b0c02ef88 /riscV/Archi.v | |
parent | aba0e740f25ffa5c338dfa76cab71144802cebc2 (diff) | |
download | compcert-35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5.tar.gz compcert-35e2b11db8d5b79a09e6d69dd68b54d3a51ba2d5.zip |
Ignore and warn about pragmas inside functions
Pragmas can occur either outside external declarations, at the top level
of a compilation unit, or within a compound statement, inside a function
definition.
The parse tree in cparse/C.mli cannot represent pragmas occuring within
a compound statement.
In this case, the elaborator used to silently move the pragma to top
level, just before the function definition where the pragma occurs.
It looks safer to just ignore pragmas occurring inside a function
definition, and emit a specific warning.
Diffstat (limited to 'riscV/Archi.v')
0 files changed, 0 insertions, 0 deletions