C front-end: reject invalid array declarators

regression/ansi-c/Array_Declarator2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=6$

regression/ansi-c/Array_Declarator3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=6$

regression/ansi-c/Array_Declarator4/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=6$

regression/ansi-c/Array_Declarator5/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=6$

regression/ansi-c/Array_Declarator6/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=6$

regression/ansi-c/Array_Declarator7/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=64$

src/ansi-c/c_typecheck_base.cpp

@@ -618,6 +618,25 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
 
   code_typet &code_type = to_code_type(symbol.type);
 
+  // Check for VLA unspecified ([*]) in function definitions
+  // This is only allowed in function prototypes, not definitions
+  for(const auto &param : code_type.parameters())
+  {
+    typet t = param.type();
+    while(t.id() == ID_array)
+    {
+      const array_typet &array_type = to_array_type(t);
+      if(array_type.get_bool(ID_C_vla_unspecified))
+      {
+        error().source_location = param.source_location();
+        error() << "'[*]' not allowed in other than function prototype scope"
+                << eom;
+        throw 0;
+      }
+      t = array_type.element_type();
+    }
+  }
+
   // reset labels
   labels_used.clear();
   labels_defined.clear();

src/ansi-c/parser.y

@@ -3532,7 +3532,73 @@ cprover_function_contract_sequence_opt:
         ;
 
 postfixing_abstract_declarator:
-          parameter_postfixing_abstract_declarator
+          non_parameter_array_abstract_declarator
+        | '(' ')'
+          {
+            // Set function name (last declarator) in source location
+            // before parsing function contracts.  Only do this if we
+            // are at a global scope.
+            if (PARSER.current_scope().prefix.empty()) {
+              PARSER.set_function(PARSER.current_scope().last_declarator);
+            }
+            // Use last declarator (i.e., function name) to name
+            // the scope.
+            PARSER.new_scope(
+              id2string(PARSER.current_scope().last_declarator)+"::");
+          }
+          cprover_function_contract_sequence_opt
+        {
+          set($1, ID_code);
+          stack_type($1).add(ID_parameters);
+          stack_type($1).add_subtype()=typet(ID_abstract);
+          PARSER.pop_scope();
+
+          // Clear function name in source location after parsing if
+          // at global scope.
+          if (PARSER.current_scope().prefix.empty()) {
+            PARSER.set_function(irep_idt());
+          }
+
+          $$ = merge($4, $1);
+        }
+        | '('
+          {
+            // Set function name (last declarator) in source location
+            // before parsing function contracts.  Only do this if we
+            // are at a global scope.
+            if (PARSER.current_scope().prefix.empty()) {
+              PARSER.set_function(PARSER.current_scope().last_declarator);
+            }
+            // Use last declarator (i.e., function name) to name
+            // the scope.
+            PARSER.new_scope(
+              id2string(PARSER.current_scope().last_declarator)+"::");
+          }
+          parameter_type_list
+          ')'
+          KnR_parameter_header_opt
+          cprover_function_contract_sequence_opt
+        {
+          set($1, ID_code);
+          stack_type($1).add_subtype()=typet(ID_abstract);
+          stack_type($1).add(ID_parameters).get_sub().
+            swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
+          PARSER.pop_scope();
+
+          // Clear function name in source location after parsing if
+          // at global scope.
+          if (PARSER.current_scope().prefix.empty()) {
+            PARSER.set_function(irep_idt());
+          }
+
+          if(parser_stack($5).is_not_nil())
+          {
+            adjust_KnR_parameters(parser_stack($$).add(ID_parameters), parser_stack($5));
+            parser_stack($$).set(ID_C_KnR, true);
+          }
+
+          $$ = merge($6, $1);
+        }
         /* The following two rules implement K&R headers! */
         | '(' 
           ')'
@@ -3636,6 +3702,32 @@ parameter_postfixing_abstract_declarator:
         }
         ;
 
+non_parameter_array_abstract_declarator:
+          '[' ']'
+        {
+          $$=$1;
+          set($$, ID_array);
+          stack_type($$).add_subtype()=typet(ID_abstract);
+          stack_type($$).add(ID_size).make_nil();
+        }
+        | '[' constant_expression ']'
+        {
+          $$=$1;
+          set($$, ID_array);
+          stack_type($$).add(ID_size).swap(parser_stack($2));
+          stack_type($$).add_subtype()=typet(ID_abstract);
+        }
+        | non_parameter_array_abstract_declarator '[' constant_expression ']'
+        {
+          // we need to push this down
+          $$=$1;
+          set($2, ID_array);
+          stack_type($2).add(ID_size).swap(parser_stack($3));
+          stack_type($2).add_subtype()=typet(ID_abstract);
+          make_subtype($1, $2);
+        }
+        ;
+
 array_abstract_declarator:
           '[' ']'
         {
@@ -3661,6 +3753,7 @@ array_abstract_declarator:
           set($$, ID_array);
           stack_type($$).add_subtype()=typet(ID_abstract);
           stack_type($$).add(ID_size).make_nil();
+          stack_type($$).set(ID_C_vla_unspecified, true);
         }
         | '[' constant_expression ']'
         {
@@ -3695,6 +3788,7 @@ array_abstract_declarator:
           set($2, ID_array);
           stack_type($2).add(ID_size).make_nil();
           stack_type($2).add_subtype()=typet(ID_abstract);
+          stack_type($2).set(ID_C_vla_unspecified, true);
           make_subtype($1, $2);
         }
         ;