[splint.git] / test / globals.c

int imp;
/*@checked@*/ int check;
/*@unchecked@*/ int uncheck;
/*@checkedstrict@*/ int checkstrict;
/*@checked@*/ /*@checked@*/ int doubled; /* 1. Redundant checked qualifier on doubled */
/*@checked@*/ /*@unchecked@*/ int contradict; /* 2. Contradictory checked and unchecked qualifiers on contradict */

void noglobs (void)
{
  imp++;         /* if +globunspec +allglobals */
  check++;       /* if +globunspec */
  uncheck++;
  checkstrict++; /* 3. Unauthorized use of global checkstrict */
}

void specglobs (void) /*@*/
{
  imp++;   /* +  if +allglobals, +impcheckedglobals */
  check++; /* 4. Unauthorized use of global check */
  uncheck++;
  checkstrict++; /* 5. Unauthorized use of global checkstrict */
}
Commit	Line	Data
885824d3	1	int imp;
	2	/@checked@/ int check;
	3	/@unchecked@/ int uncheck;
	4	/@checkedstrict@/ int checkstrict;
	5	/@checked@/ /@checked@/ int doubled; /* 1. Redundant checked qualifier on doubled */
	6	/@checked@/ /@unchecked@/ int contradict; /* 2. Contradictory checked and unchecked qualifiers on contradict */
	7
	8	void noglobs (void)
	9	{
	10	imp++; /* if +globunspec +allglobals */
	11	check++; /* if +globunspec */
	12	uncheck++;
	13	checkstrict++; /* 3. Unauthorized use of global checkstrict */
	14	}
	15
	16	void specglobs (void) /@/
	17	{
	18	imp++; /* + if +allglobals, +impcheckedglobals */
	19	check++; /* 4. Unauthorized use of global check */
	20	uncheck++;
	21	checkstrict++; /* 5. Unauthorized use of global checkstrict */
	22	}