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 internalState, fileSystem;@*/ ; /* 1. Modifies list uses ... */
   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 */