Skip to content

Commit d213ece

Browse files
Hannes SteffenhagenChristopher Wagner
Hannes Steffenhagen
authored and
Christopher Wagner
committed
Add support for postfix attributes for functions
With postfix attributes we mean something like int f() __attribute__((in this position)); This is used in Apple's CoreFoundation framework so our inability to parse this was limiting CBMC usability for code written for Apple operating systems.
1 parent a4b5abb commit d213ece

File tree

3 files changed

+28
-2
lines changed

3 files changed

+28
-2
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
inline int inline_function_with_postfix_attributes(void)
2+
__attribute__((not_a_real_attribute))
3+
{
4+
return 0;
5+
}
6+
7+
int non_inline_with_postfix_attributes(void)
8+
__attribute__((not_a_real_attribute))
9+
{
10+
return 0;
11+
}
12+
13+
int main(void)
14+
{
15+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE gcc-only
2+
test.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^PARSING ERROR$
8+
--
9+
gcc doesn't support postfix attributes but clang does, and Apples CoreFoundation framework makes use of this for availability macros.
10+
11+
Testing both the inline and non-inline variants because these are different cases in our parser.

src/ansi-c/parser.y

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3003,14 +3003,14 @@ function_head:
30033003
PARSER.add_declarator(parser_stack($$), parser_stack($1));
30043004
create_function_scope($$);
30053005
}
3006-
| declaration_specifier declarator
3006+
| declaration_specifier declarator post_declarator_attributes_opt
30073007
{
30083008
init($$, ID_declaration);
30093009
parser_stack($$).type().swap(parser_stack($1));
30103010
PARSER.add_declarator(parser_stack($$), parser_stack($2));
30113011
create_function_scope($$);
30123012
}
3013-
| type_specifier declarator
3013+
| type_specifier declarator post_declarator_attributes_opt
30143014
{
30153015
init($$, ID_declaration);
30163016
parser_stack($$).type().swap(parser_stack($1));

0 commit comments

Comments
 (0)