Search results

Wildcard permissions don't work inside predicate bodies

Status: Open.

#584 In viperproject/carbon;

· alexanderjsummers opened on Apr 23, 2026

Carbon does not "frame" trigger-matching heap-dependent functions which depend on QPs (without help)

Status: Open.

#583 In viperproject/carbon;

· alexanderjsummers opened on Apr 17, 2026

Incorrect encoding when predicate arguments in fold contain permission introspection

bugSomething isn't workingSomething isn't working

Status: Open.

#577 In viperproject/carbon;

· Dev-XYS opened on Oct 2, 2025

Heap location is added to the known-folded permission mask in fold statements even if the permission amount is zero

bugSomething isn't workingSomething isn't working

Status: Open.

#576 In viperproject/carbon;

· Dev-XYS opened on Oct 2, 2025

Known-folded permissions are not updated in unfold statements leading to unsoundness

bugSomething isn't workingSomething isn't working

Status: Open.

#572 In viperproject/carbon;

· Dev-XYS opened on Jul 31, 2025

Test case sensitive to Z3 seeds

Status: Open.

#569 In viperproject/carbon;

· Dev-XYS opened on Jun 5, 2025

Incorrect encoding when the predicate argument in an unfold statement contains a permission introspection of the same predicate

bugSomething isn't workingSomething isn't working

Status: Open.

#568 In viperproject/carbon;

· Dev-XYS opened on Jun 4, 2025

Carbon crashes when packaging wand with wildcard permission on rhs

Status: Open.

#567 In viperproject/carbon;

· marcoeilers opened on May 26, 2025

Potential incompleteness with postcondition for mutually recursive functions

Status: Open.

#564 In viperproject/carbon;

· mschwerhoff opened on Apr 4, 2025

Separating conjunction in package statement does not lead to unreachable state

incompleteness

magic-wands

Status: Open.

#557 In viperproject/carbon;

· marcoeilers opened on Feb 17, 2025

Stack overflow from Boogie

Status: Open.

#525 In viperproject/carbon;

· atoiz opened on Aug 30, 2024

Heap-dependent function with QPs generates triggerless axiom

Status: Open.

#522 In viperproject/carbon;

· jwkai opened on Jun 24, 2024