test/moreBufferTests/strrchr.c

   1
   2 extern /*@null@*/ /*@exposed@*/ char *
   3 strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c)     /*@*/  /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
   4
   5 void
   6 bar (char * t)
   7 {
   8
   9   char *ot = t;
  10
  11   char *tt;
  12   tt = strrchr (t, '\n');
  13 }
  14
  15