[acl2/acl2] 7948b8: [STS safety] Fix bug with incomplete struct types.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 7948b818db60e1be1444ae778b2a3215f9d715f0
https://github.com/acl2/acl2/commit/7948b818db60e1be1444ae778b2a3215f9d715f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

Log Message:
-----------
[STS safety] Fix bug with incomplete struct types.

The code was expecting to always find members when looking up structures by tag,
but that is not the case with incomplete struct types, e.g. `struct
incomplete;`. This is now handled properly. The bug manifested as a crash
(internal/implementation error), not as passing unsafe code.

Thanks to Grant Jurgensen for running the checks on an example that exhibited
the problem.


Commit: 296d4ab54a8f56e4404cd82cea3a6c67eff45a22
https://github.com/acl2/acl2/commit/296d4ab54a8f56e4404cd82cea3a6c67eff45a22
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)

Changed paths:
A books/kestrel/c/transformation/tests/struct-type-split/opaque.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[STS] Add test with an incomplete struct type.

This tests the bug fix in the previous commit. This test failed before the fix.


Commit: 70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
https://github.com/acl2/acl2/commit/70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)

Changed paths:
M books/kestrel/axe/arm/package.lsp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/c523eef02b27...70dac4e09c35

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