Skip to content

Comments

Update charon#351

Merged
Nadrieril merged 1 commit intoAeneasVerif:mainfrom
Nadrieril:update-charon2
Nov 25, 2025
Merged

Update charon#351
Nadrieril merged 1 commit intoAeneasVerif:mainfrom
Nadrieril:update-charon2

Conversation

@Nadrieril
Copy link
Member

Companion PR to AeneasVerif/charon#908.

@Nadrieril Nadrieril merged commit d6060bf into AeneasVerif:main Nov 25, 2025
5 of 6 checks passed
@Nadrieril Nadrieril deleted the update-charon2 branch November 25, 2025 14:47
ssyram added a commit to ssyram/eurydice that referenced this pull request Nov 26, 2025
commit 578723a
Merge: 2bb2bae 4ab9796
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 13:36:21 2025 -0800

    Merge pull request AeneasVerif#353 from AeneasVerif/protz/cosmetic

    Another round of cosmetic improvements -- this fixes AeneasVerif#270

commit 4ab9796
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 13:19:40 2025 -0800

    Another round of cosmetic improvements -- this fixes AeneasVerif#270

commit 2bb2bae
Merge: d6060bf fc34b24
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 11:35:10 2025 -0800

    Merge pull request AeneasVerif#352 from AeneasVerif/protz/cosmetic

    A bunch of cosmetic improvements

commit fc34b24
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 11:26:08 2025 -0800

    Refresh noconst version

commit ee7eefd
Merge: b94ac31 d6060bf
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:39:11 2025 -0800

    Merge branch 'main' into protz/cosmetic

commit b94ac31
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:38:39 2025 -0800

    Refresh krml version

commit 0fcbf6d
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:37:59 2025 -0800

    Some cosmetic improvements

commit d6060bf
Merge: c4e4066 430890b
Author: Nadrieril <Nadrieril@users.noreply.github.com>
Date:   Tue Nov 25 15:47:29 2025 +0100

    Merge pull request AeneasVerif#351 from Nadrieril/update-charon2

commit 430890b
Author: Nadrieril <nadrieril+git@gmail.com>
Date:   Tue Nov 25 15:29:04 2025 +0100

    Update charon

commit c4e4066
Merge: 21fd353 d0583a2
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 19:45:36 2025 -0800

    Merge pull request AeneasVerif#346 from ssyram/option_no_const

    Adding the option [no-const] to disable the const pointers in C

commit d0583a2
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 25 11:17:41 2025 +0800

    updated

commit eba7626
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 25 10:46:28 2025 +0800

    Update lib/Builtin.ml

    Co-authored-by: Jonathan Protzenko <jonathan.protzenko+github@gmail.com>

commit 28bd1fa
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 16:19:06 2025 -0800

    Refresh test output

commit 88029b4
Merge: a71f6c7 21fd353
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 16:11:09 2025 -0800

    Merge branch 'main' into option_no_const

commit 21fd353
Merge: fed8fee 9a27bae
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 15:32:10 2025 -0800

    Merge pull request AeneasVerif#350 from AeneasVerif/protz/345

    Pull in a more recent karamel and fix AeneasVerif#345

commit 9a27bae
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 15:27:40 2025 -0800

    Refresh output

commit a7ce89f
Merge: 22ccf66 bee0bbe
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:51:24 2025 -0800

    Merge branch 'main' into protz/345

commit bee0bbe
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:49:55 2025 -0800

    Refresh krml

commit 22ccf66
Merge: b037b89 fed8fee
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:35:03 2025 -0800

    Merge branch 'main' into protz/345

commit b037b89
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:26:23 2025 -0800

    Pull in a more recent karamel and fix AeneasVerif#345

commit a71f6c7
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Wed Nov 19 13:33:28 2025 +0800

    updated Makefile, added [array_eq_slice_mut]

commit 38c2e5f
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 19:45:07 2025 +0800

    reverted useless change

commit d720498
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 19:30:58 2025 +0800

    restored the test output without the [no-const] option

commit 7a265ef
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 16:10:32 2025 +0800

    fixed bug, passed all tests, the C files in out/ cannot support both options yet

commit 0e684ce
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 15:14:58 2025 +0800

    wip: passed tests using --no-const
ssyram added a commit to ssyram/eurydice that referenced this pull request Nov 27, 2025
commit 6e7b94e
Merge: 6ff35ee 119d530
Author: Nadrieril <Nadrieril@users.noreply.github.com>
Date:   Wed Nov 26 22:20:33 2025 +0100

    Merge pull request AeneasVerif#358 from Nadrieril/update-charon2

commit 119d530
Author: Nadrieril <nadrieril+git@gmail.com>
Date:   Wed Nov 26 22:12:38 2025 +0100

    Update charon

commit 6ff35ee
Merge: 578723a c191352
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Wed Nov 26 07:53:38 2025 -0800

    Merge pull request AeneasVerif#356 from ssyram/small-fix

    Fixing `check_addrof` recursion

commit c191352
Author: ssyram <liguany126@126.com>
Date:   Wed Nov 26 17:21:23 2025 +0800

    fixing `check_addrof`

commit 578723a
Merge: 2bb2bae 4ab9796
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 13:36:21 2025 -0800

    Merge pull request AeneasVerif#353 from AeneasVerif/protz/cosmetic

    Another round of cosmetic improvements -- this fixes AeneasVerif#270

commit 4ab9796
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 13:19:40 2025 -0800

    Another round of cosmetic improvements -- this fixes AeneasVerif#270

commit 2bb2bae
Merge: d6060bf fc34b24
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 11:35:10 2025 -0800

    Merge pull request AeneasVerif#352 from AeneasVerif/protz/cosmetic

    A bunch of cosmetic improvements

commit fc34b24
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 11:26:08 2025 -0800

    Refresh noconst version

commit ee7eefd
Merge: b94ac31 d6060bf
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:39:11 2025 -0800

    Merge branch 'main' into protz/cosmetic

commit b94ac31
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:38:39 2025 -0800

    Refresh krml version

commit 0fcbf6d
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Tue Nov 25 10:37:59 2025 -0800

    Some cosmetic improvements

commit d6060bf
Merge: c4e4066 430890b
Author: Nadrieril <Nadrieril@users.noreply.github.com>
Date:   Tue Nov 25 15:47:29 2025 +0100

    Merge pull request AeneasVerif#351 from Nadrieril/update-charon2

commit 430890b
Author: Nadrieril <nadrieril+git@gmail.com>
Date:   Tue Nov 25 15:29:04 2025 +0100

    Update charon

commit c4e4066
Merge: 21fd353 d0583a2
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 19:45:36 2025 -0800

    Merge pull request AeneasVerif#346 from ssyram/option_no_const

    Adding the option [no-const] to disable the const pointers in C

commit d0583a2
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 25 11:17:41 2025 +0800

    updated

commit eba7626
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 25 10:46:28 2025 +0800

    Update lib/Builtin.ml

    Co-authored-by: Jonathan Protzenko <jonathan.protzenko+github@gmail.com>

commit 28bd1fa
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 16:19:06 2025 -0800

    Refresh test output

commit 88029b4
Merge: a71f6c7 21fd353
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Mon Nov 24 16:11:09 2025 -0800

    Merge branch 'main' into option_no_const

commit 21fd353
Merge: fed8fee 9a27bae
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 15:32:10 2025 -0800

    Merge pull request AeneasVerif#350 from AeneasVerif/protz/345

    Pull in a more recent karamel and fix AeneasVerif#345

commit 9a27bae
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 15:27:40 2025 -0800

    Refresh output

commit a7ce89f
Merge: 22ccf66 bee0bbe
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:51:24 2025 -0800

    Merge branch 'main' into protz/345

commit bee0bbe
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:49:55 2025 -0800

    Refresh krml

commit 22ccf66
Merge: b037b89 fed8fee
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:35:03 2025 -0800

    Merge branch 'main' into protz/345

commit b037b89
Author: Jonathan Protzenko <jonathan.protzenko@gmail.com>
Date:   Thu Nov 20 14:26:23 2025 -0800

    Pull in a more recent karamel and fix AeneasVerif#345

commit a71f6c7
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Wed Nov 19 13:33:28 2025 +0800

    updated Makefile, added [array_eq_slice_mut]

commit 38c2e5f
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 19:45:07 2025 +0800

    reverted useless change

commit d720498
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 19:30:58 2025 +0800

    restored the test output without the [no-const] option

commit 7a265ef
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 16:10:32 2025 +0800

    fixed bug, passed all tests, the C files in out/ cannot support both options yet

commit 0e684ce
Author: Ling Zhang <ling.zhang@sjtu.edu.cn>
Date:   Tue Nov 18 15:14:58 2025 +0800

    wip: passed tests using --no-const
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant