Search results

Feature request: track unwinding in LLBC

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1206 In AeneasVerif/charon;

· Nadrieril opened on May 29, 2026

Deduplicate LLBC and ULLBC

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1205 In AeneasVerif/charon;

· Nadrieril opened on May 29, 2026

ci: auto-update the github runners

A-CIPertains to Continuous IntegrationPertains to Continuous Integration

Status: Open.

#1177 In AeneasVerif/charon;

· Nadrieril opened on May 26, 2026

ci: Fall back to github-hosted runners when self-hosted ones are unavailable

A-CIPertains to Continuous IntegrationPertains to Continuous Integration

Status: Open.

#1176 In AeneasVerif/charon;

· Nadrieril opened on May 26, 2026

Rvalue "with retag" marker

Status: Open.

#1171 In AeneasVerif/charon;

· N1ark opened on May 22, 2026

Don't use made-up strings in item names

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1169 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Bug: constant unevaluation loses padding bytes

C-bugA bug in charonA bug in charon

Status: Open.

#1168 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Clarify the evaluation of named constants

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1167 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Cleanup values representation

E-needs-helpIssues where non-expert help is needed and instructions have been given.Issues where non-expert help is needed and instructions have been given.

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1165 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Remove BuiltinFunId

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1164 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Cleanup builtin type representations

E-needs-helpIssues where non-expert help is needed and instructions have been given.Issues where non-expert help is needed and instructions have been given.

S-representationThis feature requires a nontrivial change to the AST of CharonThis feature requires a nontrivial change to the AST of Charon

Status: Open.

#1163 In AeneasVerif/charon;

· Nadrieril opened on May 17, 2026

Feature request: Setting for putting const function arguments into locals first

Status: Open.

#1161 In AeneasVerif/charon;

· firefighterduck opened on May 15, 2026