[acl2/acl2] 568df7: [C2C] Support typedefs of the split struct type.

0 views
Skip to first unread message

Grant Jurgensen

unread,
Jun 16, 2026, 3:49:32 PM (7 days ago) Jun 16
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 568df750b73e6ad6c9e802e684ab79753e1389a0
https://github.com/acl2/acl2/commit/568df750b73e6ad6c9e802e684ab79753e1389a0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[C2C] Support typedefs of the split struct type.

Now that the validator assigns unique identifiers to typedefs, a typedef
of a splittable type is split into a parallel right typedef, and uses of
the typedef name are substituted via the identifier map. Typedef
declarations reuse the existing uid-keyed declarator renaming, so the
core change is the type-spec typedef use case; the four rejection sites
and two detectors are removed. Add tests for direct, pointer, and chained
typedefs.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Reply all
Reply to author
Forward
0 new messages