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

diff --git a/src/Headers/misc.h b/src/Headers/misc.h
index cd0217a..74ba427 100644
--- 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);