[acl2/acl2] 9c472b: [STS safety] Fix loop with self-referential types.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9c472b5ac807a3965d2b5b91f1238d6e661671e0
https://github.com/acl2/acl2/commit/9c472b5ac807a3965d2b5b91f1238d6e661671e0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[STS safety] Fix loop with self-referential types.

With (directly or indirectly) self-referential struct or union types, the
traversal code loops. We fix that by keeping track of the already visited tags
of struct and union types.


Commit: a387306e9d65c6f39ed0bc73acabe9874631c412
https://github.com/acl2/acl2/commit/a387306e9d65c6f39ed0bc73acabe9874631c412
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[STS safety] Add test with self-referential traversal.

This was failing prior to the bug fix in the previous commit.


Commit: 5625f0e62857b1ed4738e2433aa4ab5427fc3aa4
https://github.com/acl2/acl2/commit/5625f0e62857b1ed4738e2433aa4ab5427fc3aa4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/support.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp

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


Commit: 48f289ce50bcc88487fd3e85163e7afd8e9e6e7f
https://github.com/acl2/acl2/commit/48f289ce50bcc88487fd3e85163e7afd8e9e6e7f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[STS safety] Fix typo in doc.


Compare: https://github.com/acl2/acl2/compare/137f51d72d87...48f289ce50bc

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

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel