/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
**
*/
# ifdef USEDMALLOC
# define sfree(x) do { if (x != NULL) free(x); } while (FALSE)
# else
-extern void sfree (/*@out@*/ /*@only@*/ /*@null@*/ void *p_x) /*@modifies *p_x@*/;
+extern void sfree (/*@out@*/ /*@only@*/ /*@null@*/ void *p_x) /*@modifies p_x@*/;
# endif
# include "misc.h"
# include "cstring.h"
# include "bool.h"
-extern /*@out@*/ /*@only@*/ void *dimalloc (size_t p_size, const char *p_name, int p_line);
+extern /*@out@*/ /*@only@*/ void *dimalloc (size_t p_size, const char *p_name, int p_line) /*@ensures maxSet(result) == (p_size - 1); @*/ ;
extern /*@only@*/ void *dicalloc (size_t p_num, size_t p_size, const char *p_name, int p_line);
extern /*@notnull@*/ /*@out@*/ /*@only@*/ void *
direalloc (/*@returned@*/ /*@only@*/ /*@out@*/ /*@null@*/ void *p_x,
/*@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); @*/ ;
+
+
+ /*drl 12/28/01 Work around for self checking */
+#ifndef LINTBUFFERCHECK
# ifdef USEDMALLOC
# define dmalloc(s) (malloc(s))
# define drealloc(s,l) (direalloc(s, l, __FILE__, __LINE__))
# endif
+#endif
+
# include "system_constants.h"
# ifdef USEGC
/*@constant int NOT_FOUND;@*/
# define NOT_FOUND (-23)
+unsigned int int_toNonNegative (int p_x) /*@*/;
+
# else
# error "Multiple include"
# endif