[splint.git] / test / modifies.c

# include "modifies.h"

static int mstat;
static /*@unused@*/ int internalState;

int f3 (int p[]) 
   /*@modifies internalState, fileSystem;@*/ ; /* 1. Modifies list uses ... */

int f4 (int p[]) 
   /*@modifies p[3];@*/;

int f5 (int fileSystem) 
   /*@modifies fileSystem;@*/ ; /* 2. Modifies list uses fileSystem ... */

int f6 (void);

int f6 (void) /*@modifies mstat;@*/ /* 3. Implementation modifies list for ... */
{ 
  return (mstat++);
}

int f1 (/*@unused@*/ int p[])
{
  mstat++; /* 4. Suspect modification of mstat: mstat++ */
  return mstat;
}

int f2 (/*@unused@*/ int p[]) /*@modifies mstat;@*/
{
  mstat++;
  return 3;
}

int g2 (/*@unused@*/ int p[]) 
{
  return 3;
} /* 5. Function g2 specified to modify internal state but no internal */
Commit	Line	Data
885824d3	1	# include "modifies.h"
	2
	3	static int mstat;
	4	static /@unused@/ int internalState;
	5
	6	int f3 (int p[])
e5081f8c	7	/@modifies internalState, fileSystem;@/ ; /* 1. Modifies list uses ... */
885824d3	8
	9	int f4 (int p[])
	10	/@modifies p[3];@/;
	11
	12	int f5 (int fileSystem)
	13	/@modifies fileSystem;@/ ; /* 2. Modifies list uses fileSystem ... */
	14
	15	int f6 (void);
	16
	17	int f6 (void) /@modifies mstat;@/ /* 3. Implementation modifies list for ... */
	18	{
	19	return (mstat++);
	20	}
	21
	22	int f1 (/@unused@/ int p[])
	23	{
	24	mstat++; /* 4. Suspect modification of mstat: mstat++ */
	25	return mstat;
	26	}
	27
	28	int f2 (/@unused@/ int p[]) /@modifies mstat;@/
	29	{
	30	mstat++;
	31	return 3;
	32	}
	33
	34	int g2 (/@unused@/ int p[])
	35	{
	36	return 3;
	37	} /* 5. Function g2 specified to modify internal state but no internal */