Skip to content

C front-end: reject invalid array declarators#8773

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-132-array-decl
Open

C front-end: reject invalid array declarators#8773
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-132-array-decl

Conversation

@tautschnig
Copy link
Collaborator

  • Reject VLA declarators with * outside function definitions
  • Reject type qualifiers and storage class specifiers in array declarators outside function prototypes

According to the C standard (C99/C11):

  • Variable length array declarators with * are only valid in function parameter declarations within function definitions (not declarations)
  • Type qualifiers (like restrict, const, volatile) in array declarators are only valid in function parameter declarations
  • Storage class specifiers (like static) in array declarators are only valid in function parameter declarations within function prototypes or definitions

These constructs are not valid in:

  • File scope variable declarations
  • Block scope variable declarations
  • Any array declarator in non-parameter contexts

Fixes: #132

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this Feb 24, 2026
Reject static, type qualifiers (restrict, const, volatile), and [*] in
array declarators outside their valid contexts per C99 6.7.5.2/6.7.5.3:

- [static N], [restrict], [restrict N], etc. are only valid in function
  parameter declarations
- [*] is only valid in function prototype scope (declarations, not
  definitions)

Implementation: the parser marks array types that use these constructs
with flags (ID_C_array_fpm_qualifier for qualifiers/static,
ID_C_array_vla_unspecified for [*]). The type-checker then rejects
non-parameter declarations with the qualifier flag, and function
definitions with the [*] flag. The [*] flag is preserved through
array-to-pointer decay so it can be detected in function bodies.

Fixes: diffblue#132

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig marked this pull request as ready for review March 18, 2026 13:13
Copilot AI review requested due to automatic review settings March 18, 2026 13:13
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR improves the ANSI-C frontend’s handling of C99 array declarator qualifiers in function-parameter contexts by marking such syntax in the parsed types and enforcing scope rules during typechecking.

Changes:

  • Add irep IDs to tag array declarators that use function-parameter-only qualifiers and to mark [*] (VLA unspecified).
  • Propagate the [*] marker through array-to-pointer decay so it remains detectable during function-definition typechecking.
  • Enforce errors for invalid uses (e.g., [*] in function definitions; qualifiers like restrict/static outside parameter declarations) and update regression expectations from KNOWNBUG to CORE.

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 1 comment.

Show a summary per file
File Description
src/util/irep_ids.def Introduces internal irep IDs for new parser/typechecker flags.
src/ansi-c/parser.y Tags parsed array declarators with new flags when using qualifiers or [*].
src/ansi-c/c_typecheck_type.cpp Preserves the [*] marker across array-to-pointer decay for parameters.
src/ansi-c/c_typecheck_base.cpp Adds semantic checks rejecting invalid array declarator qualifier usage by scope.
regression/ansi-c/Array_Declarator{2..7}/test.desc Updates regression tests to expect conversion errors (and no “warning: ignoring”).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment on lines +812 to +816
const typet &decl_type = declarator.type();
std::function<bool(const typet &)> has_array_fpm =
[&](const typet &t) -> bool
{
if(t.id() == ID_array && t.get_bool(ID_C_array_fpm_qualifier))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

ansi-c/Array_Declarator* regression tests: front end is too permissive

2 participants