*** empty log message ***

[splint.git] / test / moreBufferTests / strrchr.c

diff --git a/test/moreBufferTests/strrchr.c b/test/moreBufferTests/strrchr.c
index 6f0b4bb047614845c92acdb7eaca767205c9ac0d..3809d01ab2a2bdc7443198df535bd37461adf41d 100644 (file)
--- a/test/moreBufferTests/strrchr.c
+++ b/test/moreBufferTests/strrchr.c
@@ -1,13 +1,8 @@
 
-extern /*@null@*/ /*@exposed@*/ char *
-strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c)     /*@*/  /*@ensures MaxSet(result) >= 0 /\ MaxSet(result) <= MaxSet(s) /\ MaxRead (result) <= MaxRead(s) /\ MaxRead(result) >= 0 @*/ ;
-
 void
 bar (char * t)
 {
 
-  char *ot = t;
-  
   char *tt;
   tt = strrchr (t, '\n');
 }