test/modifies.c

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