[acl2/acl2] c54b84: [C$] Improve the precision of the validator.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: c54b848e045c7d4e51143d8509ab7ec32c8df6da
https://github.com/acl2/acl2/commit/c54b848e045c7d4e51143d8509ab7ec32c8df6da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-30 (Sat, 30 May 2026)

Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Improve the precision of the validator.

Add and use a version of the unknown type that restricts it to be scalar.

This was Grant Jurgensen's idea.


Commit: 6f7f01b592afa23e755e6febb1d1794850fae093
https://github.com/acl2/acl2/commit/6f7f01b592afa23e755e6febb1d1794850fae093
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-01 (Mon, 01 Jun 2026)

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

Log Message:
-----------
[C$] Address Grant's review.


Commit: 5f457bdef005824fe5304af3d4c9630de000d87a
https://github.com/acl2/acl2/commit/5f457bdef005824fe5304af3d4c9630de000d87a
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-06-01 (Mon, 01 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
Merge pull request #1945 from acoglio/mac3

[C$] Improve the precision of the validator.


Compare: https://github.com/acl2/acl2/compare/f669fa1d29be...5f457bdef005

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