[splint.git] / test / simplebufferConstraintTests / sizeof.c


extern void /*@alt char * @*/
  mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,
size_t n) 
  /*@modifies *s1@*/      /*@requires MaxSet(s1) >= ( n - 1
) /\ MaxRead (s2) >= ( n - 1 ); @*/ /*@ensures MaxRead (s1) ==
MaxRead (s2) /\ MaxRead (s1) <= n; @*/; 

 void f(char *z) /*@requires MaxRead(z) >= 2; @*/
{
char x[3];
char y[3];

mystrncpy (x, z, 3);
mystrncpy (y, z, 3);

x[(sizeof x)] = 'i';
y[((sizeof y) - 1)] = '0';

}
Commit	Line	Data
41320549	1
	2	extern void /@alt char @*/
	3	mystrncpy (/@unique@/ /@out@/ /@returned@/ char s1, char s2,
	4	size_t n)
dcaf75ea	5	/@modifies s1@/ /@requires MaxSet(s1) >= ( n - 1
	6	) /\ MaxRead (s2) >= ( n - 1 ); @/ /@ensures MaxRead (s1) ==
	7	MaxRead (s2) /\ MaxRead (s1) <= n; @*/;
41320549	8
dcaf75ea	9	void f(char z) /@requires MaxRead(z) >= 2; @*/
41320549	10	{
	11	char x[3];
	12	char y[3];
	13
	14	mystrncpy (x, z, 3);
	15	mystrncpy (y, z, 3);
	16
	17	x[(sizeof x)] = 'i';
	18	y[((sizeof y) - 1)] = '0';
	19
	20	}