/*@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) /*@*/ ;
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) \
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);