/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
** general.c
*/
-# include "lclintMacros.nf"
+# 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
*/
# ifndef USEDMALLOC
-# include <stdlib.h>
/*@-mustdefine@*/
{
if (x != NULL)
{
+ /* fprintf (stderr, "Freeing: %p\n", x); */
+
/*
- fprintf (stderr, "Freeing: %ld\n", x);
- if ((unsigned long) x < 136000000 && (unsigned long) x > 135000000) {
+ if ((unsigned long) x > 0xbf000000) {
fprintf (stderr, "Looks bad!\n");
}
*/
+
free (x);
+
/* fprintf (stderr, "Done.\n"); */
}
}
return res;
}
-/*@out@*/ void *dimalloc (size_t size, char *name, int line)
+/*@out@*/ void *dimalloc (size_t size, const char *name, int line)
+ /*@ensures maxSet(result) == (size - 1); @*/
{
/*
static void *lastaddr = 0;
{
if (size == 0)
{
- llbug (message ("Zero allocation at %q.",
- fileloc_unparseRaw (cstring_fromChars (name), line)));
+ llcontbug (message ("Zero allocation at %q.",
+ fileloc_unparseRaw (cstring_fromChars (name), line)));
+
+ /*
+ ** evans 2002-03-01
+ ** Return some allocated storage...hope we get lucky.
+ */
+
+ return dimalloc (16, name, line);
}
else
{
+ /* drl
+ fix this so message doesn't run out of
+ memory*/
+
+ llbuglit("Out of memory");
+
llfatalerrorLoc
(message ("Out of memory. Allocating %w bytes at %s:%d.",
size_toLongUnsigned (size),
cstring_fromChars (name), line));
+
}
}
/*@-null@*/ /* null okay for size = 0 */
+ /* fprintf (stderr, "%s:%d: Allocating: [%p / %d]\n", name, line, ret, size); */
return ret;
/*@=null@*/
}
-void *dicalloc (size_t num, size_t size, char *name, int line)
+void *dicalloc (size_t num, size_t size, const char *name, int line)
{
void *ret = (void *) calloc (num, size);
/*@=mustdefine@*/
-# ifndef NOLCL
-char *FormatInt (int i)
-{
- char temp[255]; /* assume the integer has at most 254 digits */
- char *outs;
-
- sprintf (temp, "%i", i);
- outs = (char *) dmalloc (sizeof (*outs) * (1 + strlen (temp)));
- strcpy (outs, temp);
-
- return (outs);
-}
-# endif
-
-bool
-isCext (char *ext)
-{
- return (!mstring_equal (ext, ".lcl") &&
- !mstring_equal (ext, ".spc") &&
- !mstring_equal (ext, ".ll"));
-}
-
-bool
-isLCLfile (cstring s)
-{
- char *ext;
-
- ext = filenameExtension (cstring_toCharsSafe (s));
-
- if (ext != NULL)
- {
- return (!(isCext (ext)));
- }
-
- return (TRUE);
-}
-
-char *removeExtension (/*@temp@*/ char *s, const char *suffix)
-{
- char *t = strrchr (s, '.');
- char *s2;
-
- if (t == (char *) 0 || !mstring_equal (t, suffix))
- {
- return mstring_copy (s);
- }
-
- /*@-mods@*/
- *t = '\0';
- s2 = mstring_copy (s);
- *t = '.';
- /*@=mods@*/ /* Modification is undone. */
- return s2;
-}
-
-# ifndef NOLCL
bool firstWord (char *s, char *w)
{
llassert (s != NULL);
}
return TRUE;
}
-# endif
-
-# ifndef NOLCL
-/*@only@*/ char *removePath (char *s)
-{
- char *t = strrchr (s, CONNECTCHAR);
-
- if (t == NULL) return (mstring_copy (s));
- else return (mstring_copy (t + 1));
-}
-# endif
-
-/*@only@*/ char *
-removePathFree (/*@only@*/ char *s)
-{
- char *t = strrchr (s, CONNECTCHAR);
-
-# ifdef ALTCONNECTCHAR
- {
- char *at = strrchr (s, ALTCONNECTCHAR);
- if (t == NULL || (at > t)) {
- t = at;
- }
- }
-# endif
-
- if (t == NULL)
- {
- return (s);
- }
- else
- {
- char *res = mstring_copy (t + 1);
- mstring_free (s);
- return res;
- }
-}
void mstring_markFree (char *s)
{
- sfreeEventually (s);
+ sfreeEventually (s);
}
-/*@only@*/ char *
-removeAnyExtension (char *s)
+char *mstring_spaces (int n)
{
+ int i;
char *ret;
- char *t = strrchr (s, '.');
-
- if (t == (char *) 0)
- {
- return mstring_copy (s);
- }
-
- /*@-mods@*/
- *t = '\0';
- ret = mstring_copy (s);
- *t = '.';
- /*@=mods@*/ /* modification is undone */
-
- return ret;
-}
-
-/*@only@*/ char *
-addExtension (char *s, const char *suffix)
-{
- if (strrchr (s, '.') == (char *) 0)
- {
- /* <<< was mstring_concatFree1 --- bug detected by lclint >>> */
- return (mstring_concat (s, suffix));
- }
- else
- {
- return mstring_copy (s);
- }
-}
-
-int
-getInt (char **s)
-{
- bool gotOne = FALSE;
- int i = 0;
-
- while (**s == ' ')
- {
- (*s)++;
- }
-
- if (**s == '-')
- {
- (*s)++;
- if (**s < '0' || **s > '9')
- {
- llbug (message ("getInt: bad int: %s", cstring_fromChars (*s)));
- }
- else
- {
- i = -1 * (int) (**s - '0');
- gotOne = TRUE;
- }
-
- (*s)++;
- }
-
- while (**s >= '0' && **s <= '9')
- {
- i *= 10;
- i += (int) (**s - '0');
- (*s)++;
- gotOne = TRUE;
- }
-
- if (!gotOne)
- {
- llbug (message ("No int to read: %s", cstring_fromChars (*s)));
- }
-
- while (**s == '\n' || **s == ' ' || **s == '\t')
- {
- (*s)++;
- }
+ char *ptr;
- return i;
-}
+ llassert (n >= 0);
-char
-loadChar (char **s)
-{
- char ret;
+ ret = (char *) dmalloc (size_fromInt (n + 1));
+ ptr = ret;
- while (**s == ' ')
+ for (i = 0; i < n; i++)
{
- (*s)++;
+ *ptr++ = ' ';
}
-
- ret = **s;
- (*s)++;
- return ret;
-}
-
-/*
-** not sure if this works...
-*/
-
-double
-getDouble (char **s)
-{
- char *end = mstring_createEmpty ();
- double ret;
- ret = strtod (*s, &end);
+ *ptr = '\0';
- *s = end;
return ret;
}
-/*
-** read to ' ', '\t'. '\n', '#', ',' or '\0'
-*/
-
-char *
-getWord (char **s)
+bool mstring_containsChar (const char *s, char c)
{
- char *res;
- char *t = *s;
- char c;
-
- while ((c = **s) != '\0' && (c != ' ') && (c != ',')
- && (c != '\n') && (c != '\t') && (c != '#'))
+ if (mstring_isDefined (s))
{
- (*s)++;
- }
-
- if (*s == t)
- {
- return NULL;
- }
-
- **s = '\0';
- res = mstring_copy (t);
- **s = c;
- return res;
-}
-
-bool
-optCheckChar (char **s, char c)
-{
- if (**s == c)
- {
- (*s)++;
- return TRUE;
+ return (strchr (s, c) != NULL);
}
else
{
}
}
-void
-docheckChar (char **s, char c, char *file, int line)
+bool mstring_containsString (const char *s, const char *c)
{
- /*@unchecked@*/ static int nbadchars = 0;
-
- if (**s == c)
+ if (mstring_isDefined (s))
{
- (*s)++;
+ return (strstr (s, c) != NULL);
}
else
{
- nbadchars++;
-
- if (nbadchars > 5)
- {
- llfatalbug (cstring_makeLiteral
- ("checkChar: Too many errors. Check library is up to date."));
- }
- else
- {
- llbug (message ("checkChar: %q: Bad char, expecting %h: %s",
- fileloc_unparseRaw (cstring_fromChars (file), line),
- c,
- cstring_fromChars (*s)));
- }
- }
-}
-
-char *mstring_spaces (int n)
-{
- int i;
- char *ret;
- char *ptr;
-
- llassert (n >= 0);
-
- ret = (char *) dmalloc (size_fromInt (n + 1));
- ptr = ret;
-
- for (i = 0; i < n; i++)
- {
- *ptr++ = ' ';
+ return FALSE;
}
-
- *ptr = '\0';
-
- return ret;
}
char *mstring_concat (const char *s1, const char *s2)
}
extern
-char *mstring_copy (char *s1)
+char *mstring_copy (char *s1) /*@ensures maxRead(result) == maxRead(s1) /\ maxSet(result) == maxSet(s1) @*/
{
if (s1 == NULL)
{
}
extern
-char *mstring_create (int n)
+char *mstring_create (size_t n)
{
char *s;
check (fputc ('\n', out) == (int) '\n');
}
+unsigned int int_toNonNegative (int x) /*@*/
+{
+ llassert (x >= 0);
+ return (unsigned) x;
+}
+
int int_log (int x)
{
int ret = 1;
return (long unsigned) x;
}
-size_t size_fromInt (int x)
+size_t size_fromInt (int x) /*@ensures result==x@*/
{
size_t res = (size_t) x;
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;
char
char_fromInt (int x)
{
- llassert ((x >= (int)'\0') && (x <= (int)'~'));
+ /*
+ ** evans 2001-09-28 - changed assertion in response to Anthony Giorgio's comment
+ ** that the old assertions failed for EBCDIC character set. Now we just check
+ ** that the result is equal.
+ */
- return ((char) x);
+ char res = (char) x;
+ llassert ((int) res == x);
+ return res;
}
/*@-czechfcns@*/
}
}
-/*@observer@*/ char *filenameExtension (/*@returned@*/ char *s)
-{
- llassert (s != NULL);
-
- return (strrchr(s, '.'));
-}
-
-char *removePreDirs (char *s)
-{
- while (*s == '.' && *(s + 1) == CONNECTCHAR)
- {
- s += 2;
- }
-
-# if defined(OS2) || defined(MSDOS)
- /* remove remainders from double path delimiters... */
- while (*s == CONNECTCHAR)
- {
- ++s;
- }
-# endif /* !defined(OS2) && !defined(MSDOS) */
-
- return s;
-}
-
-void checkUngetc (int c, FILE *f)
-{
- int res;
-
- llassert (c != EOF);
- res = ungetc (c, f);
- llassert (res == c);
-}
-
-bool isHeaderFile (cstring fname)
-{
- char *ext = filenameExtension (cstring_toCharsSafe (fname));
-
- return (mstring_equal (ext, ".h")
- || mstring_equal (ext, ".H")
- || mstring_equal (ext, ".lh"));
-}
-
andersk / splint.git / blobdiff