Regression: CBMC crashes because it passes the string "NULL" get_bvrep_bit during symex

[hannes-steffenhagen-diffblue]

Observed on: 3b7d59a
Still working on: 9cf2bfb

(approximate range, haven't bisected yet)

CBMC fails with:

Invariant check failed
File: ../src/util/arith_tools.cpp:305 function: get_bvrep_bit
Condition: isdigit(nibble) || (nibble >= 'A' && nibble <= 'F')
Reason: bvrep is hexadecimal, upper-case

For some reason the src parameter ends up being the string "NULL" when running cbmc against the following example:

#include <assert.h>
#include <stddef.h>

struct linked_list {
  struct linked_list *next;
};


int main(void) {
  size_t list_sz = 8ul;
  assert(list_sz == sizeof(struct linked_list));
  struct linked_list *list = malloc(list_sz);
  list->next = (struct linked_list *)0;
}

This does not happen when 8ul above is replaced with sizeof(struct linked_list). It also didn't happen last year, so was presumably caused by some of the recent refactoring work.