additional buffer checking annotations

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

diff --git a/src/Headers/general.h b/src/Headers/general.h
index e6a590982bfb7bb81d0903eb5ccf856c713e1487..3e61074610d894f364a33a0382d560a240bd8001 100644 (file)
--- a/src/Headers/general.h
+++ b/src/Headers/general.h
@@ -38,7 +38,8 @@ extern /*@only@*/ void *
   /*@releases p_x@*/
   /*@modifies *p_x@*/ ;
 
-extern /*@out@*/ /*@only@*/ void *dmalloc  (/*@sef@*/ size_t p_size) /*@*/ ;
+extern /*@out@*/ /*@only@*/ void *dmalloc  (/*@sef@*/ size_t p_size) /*@*/
+          /*@ensures MaxSet(result) == (p_size - 1); @*/ ;
 
 # ifdef USEDMALLOC
 # define dmalloc(s)    (malloc(s))