Fixed loading of rc files, warnrc and showscan.

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

diff --git a/src/Headers/misc.h b/src/Headers/misc.h
index cd0217acfa938fbc14d4e4ea77f2e9387ea03853..74ba427e3a40711785667cbaf49cfdff884a1ca8 100644 (file)
--- a/src/Headers/misc.h
+++ b/src/Headers/misc.h
@@ -64,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);