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; /* unless +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 }