[acl2/acl2] fe38cf: [C$] Extend calculation of types from annotations.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: fe38cffeb0a81bc21afa150109974e4767ea8f48
https://github.com/acl2/acl2/commit/fe38cffeb0a81bc21afa150109974e4767ea8f48
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-19 (Fri, 19 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Extend calculation of types from annotations.

Add support for `while` loops.


Commit: ad5e69d986ff1a67be25876bfec2d7e6565a9845
https://github.com/acl2/acl2/commit/ad5e69d986ff1a67be25876bfec2d7e6565a9845
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-19 (Fri, 19 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/package.lsp

Log Message:
-----------
[C2C] Import symbol into package.


Commit: 03230f90a941ae77bc57d54ae7d7f0e035fb49e3
https://github.com/acl2/acl2/commit/03230f90a941ae77bc57d54ae7d7f0e035fb49e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/interface/emacs/acl2-indent.el
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
https://github.com/acl2/acl2/commit/fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp

Log Message:
-----------
[C2C] Move code to dedicated function.


Commit: 4f5fd59e424c3ad4af3f4be906e1f482b8b91316
https://github.com/acl2/acl2/commit/4f5fd59e424c3ad4af3f4be906e1f482b8b91316
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Add a predicate about variables in computation states.

This lifts the predicate for single variables and types to variable-type maps.
This is needed to prove general supporting theorems for `while` loops.


Commit: d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
https://github.com/acl2/acl2/commit/d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp

Log Message:
-----------
[C2C] Add supporting theorems for `while` loops.


Commit: 61c34683e3e9a056cb462a7b2ab3601babb7c0b6
https://github.com/acl2/acl2/commit/61c34683e3e9a056cb462a7b2ab3601babb7c0b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp

Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.

Add support for `while` loops.


Commit: ae8c229bb5d933d9df3015553dcf7a2e102f258c
https://github.com/acl2/acl2/commit/ae8c229bb5d933d9df3015553dcf7a2e102f258c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
A books/kestrel/c/transformation/tests/simpadd0/old/while.c
A books/kestrel/c/transformation/tests/simpadd0/while.lisp

Log Message:
-----------
[C2C] Add a `simpadd0` test for `while` loops.


Compare: https://github.com/acl2/acl2/compare/5b53fbe31dbf...ae8c229bb5d9

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

[Alessandro Coglio]

Branch: refs/heads/testing