[splint-discuss] Specifying malloc() (null pointers in LCL)

[splint at coreland.ath.cx]

Hello.

I'm trying to write a formal specification of a function
very similar to malloc().

Here's a definition in LCL:

  void *
  alloc (unsigned long size)
  {
    requires size > 0;
    ensures fresh (*result);
  }

Here's the generated .lh file:

  #include "bool.h"

  extern void *alloc (unsigned long  /* size */);
  /* Output from Splint 3.1.2 */

The problem with this is that alloc() might return NULL and
despite trawling through the documentation for LCL, I can't work
out the proper way to express 'might return NULL' in LCL so that
the generated definition has the proper /*@null@*/ annotations.

Unfortunately, I'm still not exactly clear on the relationship
between splint and LCL. Is it intended that you should have to
edit the generated output in order to get splint to accept it?