ansi-c: support the neon_vector_type attribute

[tautschnig]

Clang's <arm_neon.h> declares the NEON vector typedefs (int8x16_t, ...) with attribute((neon_vector_type(N))), where N is a lane count rather than a size in bytes as for vector_size. Recognise it in the scanner, add a grammar rule mirroring vector_size that marks the frontend vector as lane-counted (ID_C_vector_lanes), carry that marker through ansi_c_convert_typet, and skip the byte-size/base-size division in typecheck_vector_type for lane-counted vectors.

• 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.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds support for Clang’s __attribute__((neon_vector_type(N))) (lane-count semantics) alongside vector_size (byte-size semantics) in the ANSI-C frontend, ensuring NEON typedefs from headers like <arm_neon.h> are correctly represented and typechecked.

Changes:

• Extend scanning/parsing to recognize neon_vector_type and mark the resulting frontend vector type as lane-counted.
• Carry a new ID_C_vector_lanes marker through ansi_c_convert_typet.
• Adjust vector typechecking to skip byte-size/base-size division for lane-counted vectors, and add a regression test.

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/util/irep_ids.def	Adds new irep id C_vector_lanes used to mark lane-counted vectors.
src/ansi-c/scanner.l	Recognizes neon_vector_type / __neon_vector_type__ as GCC-style attribute tokens.
src/ansi-c/parser.y	Adds grammar rule mirroring vector_size, tagging vectors as lane-counted.
src/ansi-c/c_typecheck_type.cpp	Updates vector typechecking to interpret size as lanes for lane-counted vectors.
src/ansi-c/ansi_c_convert_type.h	Stores lane-count semantics during type conversion (vector_lanes).
src/ansi-c/ansi_c_convert_type.cpp	Propagates lane-count marker into the constructed frontend vector type.
regression/ansi-c/gcc_neon_vector_type/test.desc	Adds regression test harness expectations for the new feature.
regression/ansi-c/gcc_neon_vector_type/main.c	Adds a regression test using neon_vector_type and asserts indexing/sizeof behavior.

---

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.69%. Comparing base (9919381) to head (d9f1976).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9038   +/-   ##
========================================
  Coverage    80.68%   80.69%           
========================================
  Files         1714     1714           
  Lines       189508   189518   +10     
  Branches        73       73           
========================================
+ Hits        152911   152927   +16     
+ Misses       36597    36591    -6     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.