[VladimirMakaev]

C functions are identified by name only, so a call can resolve to a definition with another number
of parameters (another program analyzed together, an unprototyped declaration, a function pointer
cast). Every pre/post of that definition then failed with a FormalActualLength contradiction,
silently dropping all paths through the call.

// conn.c
#include <stddef.h>
#include <sys/socket.h>
int npe_after_shutdown(int fd) {
  int* p = NULL;
  shutdown(fd, SHUT_RDWR);
  return *p; // Infer missed: null dereference
}
// plugin.c, part of another program
void shutdown(void) {}

Treat such calls as unknown: skip the summary and havoc the arguments; a noreturn attribute of the
definition still ends the path. A new stats counter, pulse_unknown_calls_arity_mismatch, counts
these calls.

Limitations: the summary is skipped even when the definition is the real callee (e.g. casts), and a
call-site noreturn declaration (like err()) is lost when the definition returns.

Test plan

New c/pulse tests arity_mismatch.c and arity_mismatch2.c: more or fewer actuals across files,
a cast function pointer, a function pointer variable and a K&R definition; variadic, matching-arity
and noreturn controls; FP_ tests for the limitations. On main the _bad tests after mismatched
calls report nothing. All codetoanalyze tests pass.

[dulmarod]

@jvillard could you have a look?

[jvillard]

Could you check if #2078 happens to solve this too?

[VladimirMakaev]

I checked: #2078 doesn't cover this. Its changes are all behind is_clang_variadic, while #2142 is about non-variadic calls whose arity doesn't match the resolved definition (cross-TU name collisions, function-pointer casts, K&R definitions), where every pre/post currently fails with a FormalActualLength contradiction and the paths are silently dropped. Only the variadic test case overlaps. The two touch the same code in PulseCallOperations.ml, so I'll rebase #2142 once #2078 lands.

[dulmarod]

There are conflicts now

[VladimirMakaev]

Rebased on top of #2078.