Klever

Memory allocation functions should be instrumented for different aspects
Namely:
1. Common parts of rule models impose restrictions on allocated pointers. For example, the ERR_PTR model should restrict value of successfully allocated pointer. The resulting pointer should be <= LDV_PTR_MAX
2. Rule models itself like 43_1a perform checks of input parameters and may also depend on returning values.
3. Memory allocation functions should not have a body. Thus they should be replaced by some functions without body.
For example, kzalloc is defined as inline function and has a body. It should be replaced, for example, by ldv_kzalloc, declared for verification task.

Suggested workaround approach defines a default model for memory allocation functions
For example,

pointcut ALLOC_AROUND: execution(static inline void *kzalloc(size_t size, gfp_t flags))

around: ALLOC_AROUND
{
  void *res;
  ldv_before_kzalloc(size, flags); 
  res = ldv_kzalloc(size, flags);
  ldv_after_kzalloc(res, size, flags);
  return res;
}

//ldv_kzalloc name is provided as configuration for verification tool
void *ldv_kzalloc(size_t size, gfp_t flags);
//the following functions may be implemented by commons parts and rule models
void ldv_before_kzalloc(size_t size, gfp_t flags);
void ldv_after_kzalloc(void *ptr, size_t size, gfp_t flags);

For example, for ERR_PTR:

void ldv_after_kzalloc(void *ptr, size_t size, gfp_t flags) {
    ldv_assume(ptr<=LDV_PTR_MAX);
}

void ldv_before_kzalloc(size_t size, gfp_t flags) {
    ldv_check_alloc_flags(flags);
}