[acl2/acl2] 9f3efe: [C$] Fix validator UID bug

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 9f3efe3d2c34d17eae2b53ff49bd499d66047f74
https://github.com/acl2/acl2/commit/9f3efe3d2c34d17eae2b53ff49bd499d66047f74
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Fix validator UID bug

Redeclarations within the same scope were sometimes assigned new UIDs.
This fixes this issue, and adds a test.


Commit: 43f71f4994cca0e6a382c48bc3ecc3a0628fce34
https://github.com/acl2/acl2/commit/43f71f4994cca0e6a382c48bc3ecc3a0628fce34
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/utilities/qualified-ident.lisp

Log Message:
-----------
[C2C] Fix resolution of qualified identifiers

Resolution no longer checks the "externals" set if the identifier is
qualified (i.e. it has a translation unit filepath).

Also adds test cases for add-section-attr.


Commit: ecbecb3fbe79d6a95f2423abdc00099a968488a1
https://github.com/acl2/acl2/commit/ecbecb3fbe79d6a95f2423abdc00099a968488a1
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp

Log Message:
-----------
[C2C] Change add-section-attr argument to alist


Commit: 327d0f50caf4d8dbf23e2ad36d46254496f29500
https://github.com/acl2/acl2/commit/327d0f50caf4d8dbf23e2ad36d46254496f29500
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp

Log Message:
-----------
[C2C] Rename qualified-ident functions

This reflects the fact that a fully qualified identifier (one where the
filepath is provided) does not necessarily represent an identifier with
internal linkage.


Commit: 341173cf7808df48111de7d6d314234934c26773
https://github.com/acl2/acl2/commit/341173cf7808df48111de7d6d314234934c26773
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp

Log Message:
-----------
[C2C] Move a theorem about annotated ASTs


Compare: https://github.com/acl2/acl2/compare/a1674138cba2...341173cf7808

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/master

Commit: 1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
https://github.com/acl2/acl2/commit/1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp

M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp

M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp

A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c

M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp

Log Message:
-----------

Merge commit '341173cf7808df48111de7d6d314234934c26773' into HEAD


Compare: https://github.com/acl2/acl2/compare/223141e65ea7...1c31d98cf7eb

[acl2buildserver]

Branch: refs/heads/testing