[Question] CBMC reports a missing body for `ctype.h#isspace` and `__ctype_b_loc`

[jyoo980]

I am attempting to verify some code that uses functions from ctypes.h. I have included a minimal example below:

#include <stdlib.h>
#include <ctype.h>

int is_separator(int c)
{
    return c == '\0' || isspace(c) || strchr(",.()+-/*=~%[];",c) != NULL;
}

Command:

goto-cc -o is_separator.goto test.c --function is_separator && goto-instrument --partial-loops --unwind 5 is_separator.goto is_separator.goto && goto-instrument  --enforce-contract is_separator is_separator.goto checking-is_separator-contracts.goto && cbmc checking-is_separator-contracts.goto --function is_separator --depth 100

Yields the error:

Reading GOTO program from 'is_separator.goto'
Writing GOTO program to 'is_separator.goto'
Reading GOTO program from 'is_separator.goto'
Function Pointer Removal
Virtual function removal
Cleaning inline assembler statements
Trying to force one backedge per target
Enforcing contracts
file data/test.c line 20 function is_separator: no body for function '__ctype_b_loc'
file data/test.c line 20 function is_separator: no body for function 'strchr'
line 9 function __CPROVER_enforce_requires_is_fresh: function 'malloc' is not declared
Adding nondeterministic initialization of static/global variables.
Writing GOTO program to 'checking-is_separator-contracts.goto'
**** WARNING: Depth-bounded analysis may yield unsound verification results
CBMC version 6.7.1 (cbmc-6.7.1) 64-bit arm64 linux
Reading GOTO program from file checking-is_separator-contracts.goto
Generating GOTO Program
Adding CPROVER library (arm64)
file <builtin-library-strchr> line 9: implicit function declaration 'strchr'
old definition in module test file test.c line 20 function is_separator
signed int (void)
new definition in module <built-in-library> file <builtin-library-strchr> line 9
char * (const char *src, signed int c)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker: instance is SATISFIABLE

** Results:
<builtin-library-strchr> function strchr
[strchr.pointer_dereference.1] line 21 dereference failure: pointer NULL in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.2] line 21 dereference failure: pointer invalid in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.3] line 21 dereference failure: deallocated dynamic object in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.4] line 21 dereference failure: dead object in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.5] line 21 dereference failure: pointer outside object bounds in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.6] line 21 dereference failure: invalid integer address in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.7] line 23 dereference failure: pointer NULL in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.8] line 23 dereference failure: pointer invalid in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.9] line 23 dereference failure: deallocated dynamic object in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.10] line 23 dereference failure: dead object in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.11] line 23 dereference failure: pointer outside object bounds in src[(signed long int)i]: UNKNOWN
[strchr.pointer_dereference.12] line 23 dereference failure: invalid integer address in src[(signed long int)i]: UNKNOWN

data/kilo_minimized_copy.c function is_separator
[is_separator.no-body.__ctype_b_loc] line 20 no body for callee __ctype_b_loc: FAILURE
[is_separator.pointer_dereference.1] line 20 dereference failure: pointer NULL in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.2] line 20 dereference failure: pointer invalid in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.3] line 20 dereference failure: deallocated dynamic object in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.4] line 20 dereference failure: dead object in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.5] line 20 dereference failure: pointer outside object bounds in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.6] line 20 dereference failure: invalid integer address in *return_value___ctype_b_loc: FAILURE
[is_separator.pointer_dereference.7] line 20 dereference failure: pointer NULL in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE
[is_separator.pointer_dereference.8] line 20 dereference failure: pointer invalid in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE
[is_separator.pointer_dereference.9] line 20 dereference failure: deallocated dynamic object in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE
[is_separator.pointer_dereference.10] line 20 dereference failure: dead object in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE
[is_separator.pointer_dereference.11] line 20 dereference failure: pointer outside object bounds in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE
[is_separator.pointer_dereference.12] line 20 dereference failure: invalid integer address in (*return_value___ctype_b_loc)[(signed long int)(signed int)c]: FAILURE

** 13 of 25 failed (5 iterations)
VERIFICATION FAILED

I think this is surprising, given that CBMC has a model for isspace (which I assume is expanded into __ctype_b_loc), which I also assume is used during verification.

Is there something I am missing here? Perhaps I need to pass an additional command-line flag? Given that strchr appears to make use of the built-in CBMC model (see the line <builtin-library-strchr> function strchr in the error log), I would have assume the same to happen for isspace.

Thanks!