X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/28bf4b0bfd405a2057d865910f8589c54a40f17b..f2b6724f9fdd443cbb7cd7db1ddd31c4c54fa5cf:/src/Headers/misc.h

diff --git a/src/Headers/misc.h b/src/Headers/misc.h
index d631e16..74ba427 100644
--- a/src/Headers/misc.h
+++ b/src/Headers/misc.h
@@ -20,6 +20,10 @@ extern void assertSet (/*@special@*/ /*@sef@*/ /*@unused@*/ void *p_x)
    /*@sets p_x, *p_x@*/ ;
 # define assertSet(x) ;
 
+extern void assertDefined (/*@sef@*/ /*@unused@*/ void *p_x) ;
+# define assertDefined(x) ;
+
+
 /*@-czechfcns@*/
 extern int size_toInt (size_t p_x) /*@*/ ;
 extern long size_toLong (size_t p_x) /*@*/ ;
@@ -45,7 +49,8 @@ extern char *mstring_append (/*@only@*/ char *p_s1, char p_c);
 extern char *mstring_copy (/*@null@*/ char *p_s1) /*@*/ ;
 extern bool mstring_equalPrefix (const char *p_c1, const char *p_c2) /*@*/ ;
 extern bool mstring_equal (/*@null@*/ const char *p_s1, /*@null@*/ const char *p_s2) /*@*/ ;
-extern bool mstring_containsChar (const char *p_s, char p_c) /*@*/ ;
+extern bool mstring_containsChar (/*@unique@*/ const char *p_s, char p_c) /*@*/ ;
+extern bool mstring_containsString (/*@unique@*/ const char *p_s, /*@unique@*/ const char *p_c) /*@*/ ;
 
 extern int mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
 # define mstring_length(s) \
@@ -59,7 +64,7 @@ extern /*@truenull@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*
 
 extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ;
 
-extern /*@notnull@*/ /*@only@*/ char *mstring_create (int p_n) /*@*/ ;
+extern /*@notnull@*/ /*@only@*/ char *mstring_create (int p_n) /*@*/  /*@ensures maxSet(result) == p_n @*/ ;
 extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ;
 
 extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s);