ldv benchmarks, call to undefined functions `ldv_xmalloc` and `ldv_calloc`

While investigating which calls to library functions happen in sv-comp that are still missing in Goblint (https://github.com/goblint/analyzer/issues/868), I came across the following issue:

Some benchmarks contain a call to ldv_xmalloc or ldv_calloc, but do not contain the definition (or even declaration in some cases) of these functions.

ldv_xmalloc

• c/ldv-linux-3.4-simple/32_7_cilled_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
• c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.i
• c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--can--softing--softing.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
• c/ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--can--usb--peak_usb--peak_usb.ko-entry_point.cil.out.i
• c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--phy--dp83640.ko-entry_point.cil.out.i
• c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-net--sched--sch_cbq.ko-entry_point.cil.out.i
• c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--atm--atmtcp.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--imu--inv_mpu6050--inv-mpu6050.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--video--fbdev--core--fb.ko-entry_point.cil.out.i
• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--irda--ali-ircc.ko-entry_point.cil.out.i

ldv_calloc

• c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--gadget--udc--bdc--bdc.ko-entry_point.cil.out.i

In other ldv tests, they are given by:

void *ldv_reference_xmalloc(size_t size)
{
  void *res;
  
  res = malloc(size);
  
  assume_abort_if_not(res != (void *)0);
  
  return res;
}

void *ldv_xmalloc(size_t size)
{
  void *tmp;
  
  tmp = ldv_reference_xmalloc(size);
  
  return tmp;
}

and

void *ldv_reference_calloc(size_t nmemb, size_t size)
{
  void *tmp;
  
  tmp = calloc(nmemb,size);
  
  return tmp;
}

void *ldv_calloc(size_t nmemb, size_t size)
{
  void *tmp;
  
  tmp = ldv_reference_calloc(nmemb,size);
  
  return tmp;
}

I would propose to manually add these definitions to the affected .i files. Or is there a better way to fix this?