diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-07 17:10:29 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 12:49:58 +0200 |
| commit | 17733e430b0c0a19853e1367ca38282a943e0c76 (patch) | |
| tree | f8751af259cf780873fd54be820228192111e845 /flocq | |
| parent | b371ea255077d700f848165a5834f104601e8253 (diff) | |
| download | compcert-17733e430b0c0a19853e1367ca38282a943e0c76.tar.gz compcert-17733e430b0c0a19853e1367ca38282a943e0c76.zip | |
Added a phantom parameter to [declaration].
This parameter is passed down in [declaration_specifiers(declaration(phantom))].
This allows us to distinguish between three calling contexts for [declaration_specifiers]:
- we are definitely in a parameter declaration;
- we are definitely in a declaration (e.g., in a block);
- we are in a declaration or in a function definition (i.e., at the top level).
This allows us to give better error messages.
For instance, when inside a block, we know that this cannot be the beginning
of a function definition.
Diffstat (limited to 'flocq')
0 files changed, 0 insertions, 0 deletions