encounter __CPROVER_enforce_requires_is_fresh : function malloc is not declare

[kaichieh0524]

Version: CBMC 6.7.1
OS: Ubuntu 24.04

I'm trying to write a harness proof to such function below

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

void foo(uint8_t *a)
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(uint8_t)))
{
   if(!a) return;
   *a = 1;
   return;
}

void harness(void)
{
  uint8_t *a;
  foo(a);
  return;
}

when I run the cbmc, then I got ' __CPROVER_enforce_requires_is_fresh : function malloc is not declare'. How can I fix this issue?

[tautschnig]

Would you mind posting the exact command lines you've used with the above test to ensure we can reproduce the problem in all detail?

[kaichieh0524]

Hi, I am using cbmc-starter-kit tool to construct a simple test program. The version is 2.10. All the flags are default, and just make the report (the harness and program is above).