Invariant violation in fatal_assertions.cpp on a program with a failing pointer check and an mmap call

[BowenWang]

Body

CBMC version: 6.11.0 (cbmc-6.11.0), this bug is still present in commit 820ff0f
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc r66.c
What behaviour did you expect: VERIFICATION FAILED reporting the null-pointer dereference.
What happened instead: CBMC aborts with an invariant violation (exit code 134).

Reproducer (r66.c)

#include <sys/mman.h>
int main(){int*p=0;*p=1;mmap(0,0,0,0,0,0);}

Output

CBMC version 6.11.0 (cbmc-6.11.0) 64-bit x86_64 linux
[...]
SAT checker: instance is SATISFIABLE
--- begin invariant violation report ---
Invariant check failed
File: src/goto-checker/fatal_assertions.cpp:91 function: reachable_fixpoint
Condition: function_iterator != goto_functions.function_map.end()
Reason: Check return value
--- end invariant violation report ---

What we found so far

We did some initial digging, though we may well be missing something:

• The failing check is in reachable_fixpoint in
  src/goto-checker/fatal_assertions.cpp, which looks up each callee in
  goto_functions.function_map.
• In this program, the mmap64 library model calls
  __CPROVER_allocated_memory (src/ansi-c/library/mman.c:121), and
  --list-goto-functions shows no function_map entry for that intrinsic,
  which would make the lookup fail.
• A variant that declares and calls __CPROVER_allocated_memory directly from
  the source file does not crash (there the intrinsic does appear in the
  function map), so the difference seems related to how the library model is
  linked in — but we are not sure this is the root cause.