Description
PAL fails to verify a function containing an unreachable pointer dereference. The pointer is annotated _plain, so no ownership of its pointee is available—but none should be needed because the dereference cannot execute.
Reproducer
#include "pal.h"
int example(_plain int *p)
{
if (1)
return 7;
return *p; /* Cannot execute. */
}Expected behavior
Verification succeeds without requiring ownership of *p. The function always returns 7.
Actual behavior
Translation reports no diagnostics, but verification fails with:
Error 228:
Tactic failed
Cannot prove:
Pulse.Lib.Reference.pts_to var_p (*?u171*)_
In the context:
Pulse.Lib.Reference.pts_to var_p var_p
PAL emits:
divergent fn func_example (var_p: (ref Int32.t))
returns return_1 : Int32.t
{
let mut var_p = var_p;
if ((int32_to_bool 1l)) {
return 7l;
} else {};
return (!(!var_p));
}
The available resource describes the generated mutable local holding p, not the object pointed to by p.
Explicit unreachability does not resolve the failure
Adding a ghost statement immediately before the dead dereference:
int example(_plain int *p)
{
if (1)
return 7;
_ghost_stmt(unreachable ());
return *p;
}still fails, with a different diagnostic:
Error 228:
Tactic failed
Unexpected unresolved uvars in the term:
!var_p
Additional investigation
Adding _ensures(false) immediately after if (1), before its then-statement, produces an explicit false postcondition for the generated if. However, verification then fails with a leftover resource for the mutable local holding p.
Adding _ghost_stmt(unreachable ()); in an explicit else branch removes that leftover-resource failure, but verification still fails at the subsequent dereference.
These experiments suggest an interaction between unreachable continuations and resource/type inference. The precise root cause, and whether the fix belongs in PAL’s lowering or Pulse’s handling of unreachable code, remain undetermined.
Reproduction environment
- PAL main:
545978a
- F* toolchain:
fstar-2026-09-15
- Regression:
test/unreachable_deref/unreachable_deref.c
- Focused command:
make -C test/unreachable_deref -j8
No PAL implementation changes were made during reproduction.
Description
PAL fails to verify a function containing an unreachable pointer dereference. The pointer is annotated
_plain, so no ownership of its pointee is available—but none should be needed because the dereference cannot execute.Reproducer
Expected behavior
Verification succeeds without requiring ownership of
*p. The function always returns7.Actual behavior
Translation reports no diagnostics, but verification fails with:
PAL emits:
The available resource describes the generated mutable local holding
p, not the object pointed to byp.Explicit unreachability does not resolve the failure
Adding a ghost statement immediately before the dead dereference:
still fails, with a different diagnostic:
Additional investigation
Adding
_ensures(false)immediately afterif (1), before its then-statement, produces an explicit false postcondition for the generatedif. However, verification then fails with a leftover resource for the mutable local holdingp.Adding
_ghost_stmt(unreachable ());in an explicitelsebranch removes that leftover-resource failure, but verification still fails at the subsequent dereference.These experiments suggest an interaction between unreachable continuations and resource/type inference. The precise root cause, and whether the fix belongs in PAL’s lowering or Pulse’s handling of unreachable code, remain undetermined.
Reproduction environment
545978afstar-2026-09-15test/unreachable_deref/unreachable_deref.cmake -C test/unreachable_deref -j8No PAL implementation changes were made during reproduction.