/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "splintMacros.nf"
# include "basic.h"
+
# undef malloc
# undef realloc
# undef calloc
# include "dmalloc.h"
# endif
-# include "portab.h"
+# include "osd.h"
/*
** redefine undef'd memory ops
/*@=mustdefine@*/
-char *FormatInt (int i)
-{
- char temp[255]; /* assume the integer has at most 254 digits */
- char *outs;
- int sres = snprintf (temp, 255, "%i", i);
- check (sres >= 0 && sres <= 255);
- outs = (char *) dmalloc (sizeof (*outs) * (1 + strlen (temp)));
- strcpy (outs, temp);
-
- return (outs);
-}
-
bool firstWord (char *s, char *w)
{
llassert (s != NULL);
return res;
}
+size_t size_fromLong (long x) /*@ensures result==x@*/
+{
+ size_t res = (size_t) x;
+
+ llassert ((long) res == x);
+ return res;
+}
+
+size_t size_fromLongUnsigned (unsigned long x) /*@ensures result==x@*/
+{
+ size_t res = (size_t) x;
+
+ llassert ((unsigned long) res == x);
+ return res;
+}
+
int size_toInt (size_t x)
{
int res = (int) x;