CBMC 6.8.0 not reporting use-after-free in printf

[lou1306]

gcc -Wall will warn of a use-after-free when compiling this simple program:

#include <stdio.h>
#include <stdlib.h>

int main(void) {
  char *test = malloc(20);
  if (test == NULL) { return 1; }
  for (int i = 0; i < 20; ++i) {
    test[i] = 'a' + i;
  }
  test[19] = '\0';
  free(test);
  printf("test = %s\n", test);
  return 0;
}

$ gcc -Wall main.c

main.c: In function ‘main’:
main.c:14:3: warning: pointer ‘test’ used after ‘free’ [-Wuse-after-free]
   14 |   printf("test = %s\n", test);
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~
main.c:12:3: note: call to ‘free’ here
   12 |   free(test);
      |   ^~~~~~~~~~

However, CBMC 6.8.0 does not seem to care about the freed pointer being passed to printf:

$ cbmc main.c

CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
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 UNSATISFIABLE

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

main.c function main
[main.overflow.2] line 7 arithmetic overflow on signed + in i + 1: SUCCESS
[main.overflow.1] line 8 arithmetic overflow on signed + in 97 + i: SUCCESS
[main.pointer_dereference.1] line 8 dereference failure: pointer NULL in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.2] line 8 dereference failure: pointer invalid in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.3] line 8 dereference failure: deallocated dynamic object in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.4] line 8 dereference failure: dead object in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.5] line 8 dereference failure: pointer outside object bounds in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.6] line 8 dereference failure: invalid integer address in test[(signed long int)i]: SUCCESS
[main.pointer_dereference.7] line 10 dereference failure: pointer NULL in test[(signed long int)19]: SUCCESS
[main.pointer_dereference.8] line 10 dereference failure: pointer invalid in test[(signed long int)19]: SUCCESS
[main.pointer_dereference.9] line 10 dereference failure: deallocated dynamic object in test[(signed long int)19]: SUCCESS
[main.pointer_dereference.10] line 10 dereference failure: dead object in test[(signed long int)19]: SUCCESS
[main.pointer_dereference.11] line 10 dereference failure: pointer outside object bounds in test[(signed long int)19]: SUCCESS
[main.pointer_dereference.12] line 10 dereference failure: invalid integer address in test[(signed long int)19]: SUCCESS
[main.precondition_instance.1] line 12 free argument must be NULL or valid pointer: SUCCESS
[main.precondition_instance.2] line 12 free argument must be dynamic object: SUCCESS
[main.precondition_instance.3] line 12 free argument has offset zero: SUCCESS
[main.precondition_instance.4] line 12 double free: SUCCESS
[main.precondition_instance.5] line 12 free called for new[] object: SUCCESS
[main.precondition_instance.6] line 12 free called for stack-allocated object: SUCCESS

** 0 of 22 failed (1 iterations)
VERIFICATION SUCCESSFUL

(I initially discovered this behaviour while using ESBMC, and they seem to confirm it is a bug: esbmc/esbmc#3135)

[tautschnig]

We do not currently parse the formatting string to a sufficient extent to ever even try to dereference test in the above example. So, yes, this is a bug on our end.