[splint-discuss] question about constraints, missing warning

[Thomas]

Hi.
I have a problem with understanding constraints, or it's abug:

For example memcpy():
  void *memcpy
  (
    /*@unique@*/ /*@out@*/ /*@returned@*/ void *dest, const void *src, size_t n
  )
  /*@modifies *dest@*/
  /*@requires maxSet(dest) >= (n-1); @*/
  /*@ensures maxRead(src) >= maxRead(dest) /\ maxRead(dest) <= n;@*/;


Code example:
	char	a[5];
	char	b[10];

	// h
	memcpy(a, b, sizeof(a)+1);
	printf("sink: %s\na: %s\nb: %s\n\n", sink, a, b);

	// i
	memcpy(a, b, sizeof(a)+2);
	printf("sink: %s\na: %s\nb: %s\n\n", sink, a, b);

Splint only reports:
	bof_static.c:62:2: Likely out-of-bounds store: memcpy(a, b, sizeof((a)) + 2)

But not the off-by-one of case (h). Why that?


When I resolve the constraint I get:
maxSet(a) = 4
n         = sizeof(a) + 1 = 6
n-1       = 6 - 1         = 5

4 >= 5 ==> FALSE

splint should warn about this, shouldn't it?



Bye
Thomas