Spurious warnings in proof of s2n-tls function s2n_stuffer_read_hex()

[rod-chapman]

CBMC version: "develop" branch commit c193c27, built on 27th August 2024
Operating system: EC2/Ubuntu Linux
Exact command line resulting in the issue: "make result"
What behaviour did you expect: Successful proof with 0 warnings and 0 errors.
What happened instead: 2 warnings, possibly spurious.

Proof of the function s2n_stuffer_read_hex() from the fork at https://github.com/rod-chapman/s2n-tls,
on branch "unbound_stuffer_read_hex" at commit [e307312].

Proof succeeds OK, but generates two confusing warnings:

file <builtin-library-tolower> line 4:  'tolower'
old definition in module s2n_blob file /usr/include/ctype.h line 122
signed int (signed int __c, __CPROVER_contracts_write_set_ptr_t __write_set_to_check)
new definition in module <built-in-library> file <builtin-library-tolower> line 4
signed int (signed int c)

file <builtin-library-strcasecmp> line 9:  'strcasecmp'
old definition in module s2n_errno file /usr/include/strings.h line 116
signed int (const char *__s1, const char *__s2, __CPROVER_contracts_write_set_ptr_t __write_set_to_check)
new definition in module <built-in-library> file <builtin-library-strcasecmp> line 9
signed int (const char *s1, const char *s2)

It is rather non-obvious what's going wrong here, and if these really are a problem or not. Will cause confusion and anxiety for users.