[splint-discuss] Undeclared operator: maxRead

[splint at coreland.ath.cx]

>From alloc.lcl:

/*
 * Allocate new storage of size size_new, copy size_old bytes
 * of pointer to new storage, deallocate original storage and
 * assign new storage to pointer.
 */

int
alloc_re (only out void **pointer, unsigned long size_old, unsigned long size_new)
{
  requires
    (size_old > 0) /\
    (size_new > 0) /\
    (maxRead (*pointer) == size_old);
  ensures
    ((result == 0) \/ (result == 1)) /\
    (maxRead (*pointer) == size_new);
}

$ splint +strict +lh alloc.lcl
Splint 3.1.2 --- 24 May 2009

alloc.lcl:42:6: Undeclared operator: maxRead
alloc.lcl:45:6: Undeclared operator: maxRead
Finished checking --- 2 spec warnings
       no code processed

Not sure what's happening here...