Issues

• Palow: loop inside an if arm leaves an unreduced match join (Error 228)

  FStarLang/pal#367 · Filter by author gebner opened on Oct 10, 2026

• Palow: advancing an _array pointer parameter (data++) is refused

  FStarLang/pal#355 · Filter by author gebner opened on Oct 7, 2026

• Palow: partial scatter state is lost at an if join

  palow
  FStarLang/pal#341 · Filter by author gebner opened on Oct 5, 2026

• function pointer unions generating ill-typed code

  FStarLang/pal#340 · Filter by author amosr-msft opened on Oct 3, 2026

• Block shadowing allows false contracts to verify

  FStarLang/pal#325 · Filter by author hei411 opened on Sep 23, 2026

• Support typed private storage in trailing byte arrays

  FStarLang/pal#309 · Filter by author hei411 opened on Sep 16, 2026

• String-literal arguments fail verification when the function's return value is used

  FStarLang/pal#305 · Filter by author hei411 opened on Sep 14, 2026

• A function named work__fp collides with PAL's generated wrapper for work

  bug
  FStarLang/pal#302 · Filter by author hei411 opened on Sep 11, 2026

• Generated anonymous struct names collide with explicit C tags and silently change field types

  bug
  FStarLang/pal#300 · Filter by author hei411 opened on Sep 11, 2026

• Same-named struct tags in different source files are merged, making verification depend on input order

  bug
  FStarLang/pal#299 · Filter by author hei411 opened on Sep 11, 2026

• Support free(NULL) and deallocation of nullable pointers

  enhancement
  FStarLang/pal#294 · Filter by author hei411 opened on Sep 9, 2026

• Internal error "Impossible: cycle detected after cycle detection has passed" when a pointer typedef is declared before its struct

  FStarLang/pal#282 · Filter by author akashlal opened on Sep 4, 2026

• Function-pointer wrappers drop all pointee postconditions (and silently accept false _old contracts)

  FStarLang/pal#279 · Filter by author hei411 opened on Aug 28, 2026
  

• Array literal in a nested expression is emitted without ownership (silently produces unverifiable Pulse)

  enhancement
  FStarLang/pal#273 · Filter by author hei411 opened on Aug 27, 2026

• Unsupported goto: label at the head of a tail else branch

  enhancement
  Feature

  FStarLang/pal#255 · Filter by author hei411 opened on Aug 20, 2026

• Make malloc return void*

  FStarLang/pal#186 · Filter by author gebner opened on Jul 28, 2026

• Extra pointer field breaks writes

  FStarLang/pal#113 · Filter by author gebner opened on Jun 3, 2026
  2

• switch translator emits brk := true; outside the matching case, killing all subsequent arms

  FStarLang/pal#107 · Filter by author KimayaBedarkar opened on May 28, 2026

• Using local struct requires lemma call

  FStarLang/pal#101 · Filter by author mtzguido opened on May 19, 2026

• _live should take an rvalue value instead of lvalue

  FStarLang/pal#97 · Filter by author gebner opened on Apr 20, 2026

• Restrict pointer equality to null or valid pointers

  FStarLang/pal#96 · Filter by author gebner opened on Apr 18, 2026

• Ensure that _ghost_stmt only adds ghost code

  FStarLang/pal#95 · Filter by author gebner opened on Apr 16, 2026

• Provide specifications for C library functions

  FStarLang/pal#92 · Filter by author gebner opened on Apr 9, 2026

• assert support breaks depending on the order of the includes

  FStarLang/pal#87 · Filter by author gebner opened on Apr 8, 2026
  1

• Performance issues with pts_to_mask

  FStarLang/pal#84 · Filter by author gebner opened on Mar 12, 2026