Issues

• Loop abstraction creates a borrow flow edge from a lifetime projection to itself

  prusti/pcg#194 · Filter by author rgwohlbold opened on Nov 2, 2026

• Placeholder assertion when a raw pointer is copied while a mutable borrow through it is live

  prusti/pcg#193 · Filter by author rgwohlbold opened on Nov 2, 2026
  1

• loop_invariant_place_capabilities reports W for a write-only loop local, but the dataflow keeps it at E and later weakens E -> W

  prusti/pcg#181 · Filter by author JonasAlaif opened on Sep 23, 2026

• Over-approximate loop shape generated

  prusti/pcg#162 · Filter by author zgrannan opened on Apr 14, 2026

• Function shape edge being removed too early for call with nested refs

  prusti/pcg#151 · Filter by author zgrannan opened on Mar 30, 2026

• Unsound restoration to E capability after expiry of conditional borrow

  prusti/pcg#137 · Filter by author zgrannan opened on Feb 11, 2026

• Ensure PCG + Prusti works for paper examples

  prusti/pcg#134 · Filter by author zgrannan opened on Feb 9, 2026

• Change order for borrow expiry / reference weakining

  prusti/pcg#132 · Filter by author zgrannan opened on Feb 9, 2026

• Visualization shows capabilities for labelled places

  prusti/pcg#131 · Filter by author zgrannan opened on Feb 6, 2026

• Enum pack/unpack wrong

  prusti/pcg#77 · Filter by author JonasAlaif opened on Sep 9, 2025
  3