test/numabstract.c

   1 typedef /*@numabstract@*/ int apples;
   2 typedef /*@numabstract@*/ int oranges;
   3
   4 /*@noaccess apples@*/
   5 /*@noaccess oranges@*/
   6
   7 int adding (apples a, oranges o)
   8 {
   9   int i;
  10   apples a2;
  11   a++; /* Okay */
  12   a2 = 13; /* error (unless +numabstractlit) ? */
  13   a2 = 'a'; /* error */
  14   i = 'c'; /* error */
  15   a2 = (apples) 13; /* warning if +numabstractcast */
  16   a2 = a + 5; /* okay */
  17   a2 = o; /* error */
  18   a2 = a2 - a; /* okay */
  19   i = o; /* error */
  20   i = a2 + a; /* error */
  21   return a + o; /* error */
  22 }
  23
  24 int comparing (apples a, oranges o, apples a2)
  25 {
  26   if (a < 3) { /* error unless +numabstractlit */
  27     return 3;
  28   }
  29
  30   if (a < o) { /* error */
  31     return 5;
  32   }
  33
  34   if (a == o) { /* error */
  35     return 6;
  36   }
  37
  38   if (a == a2) { /* okay */
  39     return 23;
  40   }
  41
  42   --a2;
  43
  44   if (a >= a2) {
  45     return 523;
  46   }
  47
  48   return 7;
  49 }