A function declared inside a function body is dropped, leaving an unresolvable call

[akashlal]

Versions: PAL a9ebbed · F*/Pulse nightly 2026-08-27 · Clang 20.1.8

Summary

A function declared inside a function body — the K&R-era idiom of declaring a library function locally instead of including its header — is dropped, and the call then has no definition to resolve to.

PAL does report unsupported variable declaration Function, but translation continues and emits a module that cannot verify.

Minimal repro

#include "pal.h"

/* 1. FAILS -- callee declared inside the body. */
double local_decl(_array double *v, unsigned n)
  _preserves(v._length == n)
  _requires(n > 0)
{
    double floor();
    double d = floor(2.0);
    return v[0] + d;
}

/* 2. control -- identical, callee declared at FILE scope.  VERIFIES */
double floor_at_file_scope();

double control_file_scope(_array double *v, unsigned n)
  _preserves(v._length == n)
  _requires(n > 0)
{
    double d = floor_at_file_scope();
    return v[0] + d;
}

/* 3. control -- no call at all.                            VERIFIES */
double control_no_call(_array double *v, unsigned n)
  _preserves(v._length == n)
  _requires(n > 0)
{
    return v[0];
}

$ pal --outdir out repro.c
error: unsupported variable declaration Function
error: (internal, after merge) unknown function floor
error: (internal, after normalize_casts) unknown function floor
error: (internal, after elim_cis) unknown function floor
error: (internal, after elim_cis) cannot infer type of floor(N): floor is not a function

$ run-fstar.sh --include out out/Func_local_decl.fst
Error 72: Identifier not found: func_floor

$ run-fstar.sh --include out out/Func_control_file_scope.fst   # Verified
$ run-fstar.sh --include out out/Func_control_no_call.fst      # Verified

All three functions carry the same trivially provable array index (v[0]), so the only variable is where the callee is declared.

Impact

We are using PAL to prove spatial memory safety on the Olden and Ptrdist benchmark suites, holding the C source fixed and adding only annotations. Older C in these suites declares floor, sqrt, atoi and similar locally rather than including a header, so the construct shows up in real code.

The impact is modest on its own — in olden/bh it accounts for 2 of 73 obligations — but the diagnostic is misleading: the reported error is about a variable declaration, and the eventual failure is an unresolved identifier in generated code, so the connection back to the local declaration is not obvious.

Suggested behaviour

Either treat a function declared in block scope the same as one declared at file scope (C's scoping rules make this equivalent for the callee's type), or make the translation error fatal so it is not silently followed by an unverifiable module.

Related: #92 (Provide specifications for C library functions), #73 (Support separate function declarations, closed).

[gebner]

or make the translation error fatal so it is not silently followed by an unverifiable module.

That is by design: we want to always produce as much output as we can. This is so that a single missing feature doesn't block the whole project.

[akashlal]

Thanks for the quick fix — I can confirm a177f59 works. Verified on 845d755: the declaration is hoisted and the call resolves.

There is a narrower case still open, which your new test/local_fn_decl/local_fn_decl.c doesn't cover because it declares no-argument functions. A K&R-style declaration with unspecified parameters, called with arguments, still fails:

/* A: local decl, no params, called with none  -- your test's shape.  VERIFIES */
double a_noargs(_array double *v, unsigned n) _preserves(v._length == n) _requires(n > 0)
{ double pal_g(); double d = pal_g(); return v[0] + d; }

/* B: local decl with UNSPECIFIED params (K&R), called WITH an argument.  FAILS */
double b_kr_witharg(_array double *v, unsigned n) _preserves(v._length == n) _requires(n > 0)
{ double pal_h(); double d = pal_h(2.0); return v[0] + d; }

/* C: local decl with an explicit prototype, called with an argument.  VERIFIES */
double c_proto(_array double *v, unsigned n) _preserves(v._length == n) _requires(n > 0)
{ double pal_k(double); double d = pal_k(2.0); return v[0] + d; }

error: (internal, after merge) incorrect number of arguments, expected 0, got 1
error: (internal, after normalize_casts) incorrect number of arguments, expected 0, got 1
error: (internal, after elim_cis) incorrect number of arguments, expected 0, got 1

Error 189: Ill-typed term
  refl_core_check_term failed:  Top ()

So the hoisting is right; the empty parameter list is being treated as "takes zero arguments" rather than C's "unspecified parameters". In C89 double floor(); declares an unspecified parameter list and floor(2.0) is a legal call — which is exactly the idiom that motivates hoisting in the first place, since old code that declares functions locally also tends to declare them without prototypes.

olden/tsp and olden/perimeter both hit this (chatting, the CMMD_* family).

Happy to open this as a separate issue if you'd rather keep this one closed — just say which you prefer.

That is by design: we want to always produce as much output as we can. This is so that a single missing feature doesn't block the whole project.

Understood, and that makes sense. For what it's worth, from the consumer side the thing that cost us time was not the non-fatal error itself but that the downstream symptom (Identifier not found: func_floor, in generated code) doesn't point back to the original diagnostic. Not asking for a behaviour change — just noting it in case a hint in the second message is ever cheap to add.