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.

Author: Hannes Steffenhagen

regression/ansi-c/function_with_postfix_attributes/test.c

@@ -0,0 +1,15 @@
+inline int inline_function_with_postfix_attributes(void)
+  __attribute__((not_a_real_attribute))
+{
+  return 0;
+}
+
+int non_inline_with_postfix_attributes(void)
+  __attribute__((not_a_real_attribute))
+{
+  return 0;
+}
+
+int main(void)
+{
+}

regression/ansi-c/function_with_postfix_attributes/test.desc

@@ -0,0 +1,11 @@
+CORE gcc-only
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^PARSING ERROR$
+--
+gcc doesn't support postfix attributes but clang does, and Apples CoreFoundation framework makes use of this for availability macros.
+
+Testing both the inline and non-inline variants because these are different cases in our parser.

src/ansi-c/parser.y

@@ -3003,14 +3003,14 @@ function_head:
           PARSER.add_declarator(parser_stack($$), parser_stack($1));
           create_function_scope($$);
         }
-        | declaration_specifier declarator
+        | declaration_specifier declarator post_declarator_attributes_opt
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));
           PARSER.add_declarator(parser_stack($$), parser_stack($2));
           create_function_scope($$);
         }
-        | type_specifier declarator
+        | type_specifier declarator post_declarator_attributes_opt
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));