Add support for enums with underlying type specifications to the parser #5431
Conversation
danpoe
changed the title
danpoe
force-pushed
the
feature/enums-with-underlying-type
branch
from
919a6c3 to
6abdb89
Compare
|
|
||
| int main() | ||
| { | ||
| enum my_enum2 : unsigned enum_var1; |
There was a problem hiding this comment.
Huh? Any ideas on what this means? Seems like clang allows this notation, but it appears to not actually mean anything, for instance
#include <stdio.h>
enum my_enum : signed char {
A, B
};
int main(void) {
enum my_enum : unsigned long long X = 255;
printf("%d\n", X);
}
Seems to compile just fine and works as if the second : unsigned long long wasn’t there.
There was a problem hiding this comment.
Yeah it seems to just be ignored by clang. My guess would be that it might have been overly complicated for clang to exclude this case in the grammar, which would also be true for cbmc. I think we should report this as an error during conversion/typechecking.
Codecov Report
@@ Coverage Diff @@
## develop #5431 +/- ##
===========================================
- Coverage 68.21% 67.36% -0.85%
===========================================
Files 1178 1178
Lines 97550 97551 +1
===========================================
- Hits 66544 65720 -824
- Misses 31006 31831 +825
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
Codecov Report
@@ Coverage Diff @@
## develop #5431 +/- ##
========================================
Coverage 68.21% 68.21%
========================================
Files 1178 1178
Lines 97550 97561 +11
========================================
+ Hits 66544 66554 +10
- Misses 31006 31007 +1
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
I think this looks OK, though its not my absolute area of expertise. I assume you've already taken a look at Parser::ParseEnumSpecifier in https://clang.llvm.org/doxygen/ParseDecl_8cpp_source.html to check what Clang is doing - though of course they have a hand-written parser which gives them a bit more flexibility.
danpoe
force-pushed
the
feature/enums-with-underlying-type
branch
2 times, most recently
from
f5bc54d to
cd77e54
Compare
src/util/irep_ids.def
Outdated
| @@ -212,6 +212,7 @@ IREP_ID_ONE(NULL) | |||
| IREP_ID_ONE(null) | |||
| IREP_ID_ONE(nullptr) | |||
| IREP_ID_ONE(c_enum) | |||
| IREP_ID_ONE(underlying_type) | |||
There was a problem hiding this comment.
Should this be something like enum_underlying_type or is there a reason is should not be specific to enums?
There was a problem hiding this comment.
No particular reason, I've changed it to enum_underlying_type.
danpoe
force-pushed
the
feature/enums-with-underlying-type
branch
from
cd77e54 to
ab2b220
Compare
danpoe
force-pushed
the
feature/enums-with-underlying-type
branch
from
ab2b220 to
0bb02be
Compare
danpoe
force-pushed
the
feature/enums-with-underlying-type
branch
from
0bb02be to
75f9c49
Compare
This adds support for parsing enums that specify the underlying type (a clang extension) to cbmc. For example, a usage would look like
enum enum1 : unsigned {X, Y}.The change to the grammar however introduces an additional shift/reduce conflict. The issue seems to be that the new syntax leads to ambiguity with the syntax for bitfields (where the bit portion also starts with a
:). That is, forenum enum1 : unsigned, whenenum enum1has been read and:becomes the lookahead token, there is a choice between reducing (thusenum enum1becomes the portion matched by theenum_namerule), or shifting, in which case: unsignedwill become part of the portion matched by the rule as well. Any suggestions on how or if this can be fixed would be appreciated.