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

[splint at coreland.ath.cx]

On 2009-05-26 16:47:13, splint at coreland.ath.cx wrote:
> Hello.
> 
> I'm trying to write a formal specification of a function
> very similar to malloc().

Managed to answer my own question about five seconds after
sending the last mail by just trying things at random:

$ cat alloc.lcl
only out null void *
alloc (unsigned long size)
{
  requires size > 0;
  ensures fresh (*result);
}

$ cat alloc.lh
extern void *alloc (unsigned long  /* size */);

$ cat alloc.c
#include "alloc.h"
#include <stdlib.h>

void *
alloc (unsigned long size)
{
  return malloc ((size_t) size);
}

$ splint +strict +partial alloc.c alloc.h alloc.lcl
Splint 3.1.2 --- 24 May 2009

Finished checking --- no warnings

Bit bemused that nowhere does any of the documentation I've
been able to find on LCL specify anything called "out", "null"
or "only". Are these splint extensions?

Is there some enormous reference manual on LCL that I'm missing
somewhere?