*** empty log message ***

[splint.git] / src / Headers / cstring.h

diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h
index b034896bea5f8ae2a9d82d6a63ba6e41ec1da818..2a68dff4c576ef1986be2285f208a50b22eea048 100644 (file)
--- a/src/Headers/cstring.h
+++ b/src/Headers/cstring.h
@@ -51,8 +51,8 @@ extern void cstring_replaceAll (cstring p_s, char p_old, char p_snew) /*@modifie
 # endif
 
 extern void cstring_replaceLit (/*@unique@*/ cstring p_s, char *p_old, char *p_snew);
-extern char cstring_firstChar (cstring p_s);
-extern char cstring_secondChar (cstring p_s);
+extern char cstring_firstChar (cstring p_s) /*@*/ ;
+extern char cstring_secondChar (cstring p_s) /*@*/ ;
 extern char cstring_lastChar (cstring p_s) /*@*/ ;
 extern char cstring_getChar (cstring p_s, int p_n);
 extern void cstring_setChar (cstring p_s, int p_n, char p_c);