2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
28 # include "splintMacros.nf"
42 ** redefine undef'd memory ops
53 /* fprintf (stderr, "Freeing: %p\n", x); */
56 if ((unsigned long) x > 0xbf000000) {
57 fprintf (stderr, "Looks bad!\n");
63 /* fprintf (stderr, "Done.\n"); */
68 void sfreeEventually (void *x)
72 ; /* should keep in a table */
78 ** all memory should be allocated from dimalloc
81 static long unsigned size_toLongUnsigned (size_t x)
83 long unsigned res = (long unsigned) x;
85 llassert ((size_t) res == x);
89 /*@out@*/ void *dimalloc (size_t size, const char *name, int line)
90 /*@ensures maxSet(result) == (size - 1); @*/
93 static void *lastaddr = 0;
94 static int numallocs = 0;
95 static int numbad = 0;
98 /* was malloc, use calloc to initialize to zero */
99 void *ret = (void *) calloc (1, size);
107 fprintf (stderr, "Bad alloc: %d / %d\n", numbad, numallocs);
117 llcontbug (message ("Zero allocation at %q.",
118 fileloc_unparseRaw (cstring_fromChars (name), line)));
122 ** Return some allocated storage...hope we get lucky.
125 return dimalloc (16, name, line);
130 fix this so message doesn't run out of
133 llbuglit("Out of memory");
136 (message ("Out of memory. Allocating %w bytes at %s:%d.",
137 size_toLongUnsigned (size),
138 cstring_fromChars (name), line));
143 /*@-null@*/ /* null okay for size = 0 */
144 /* fprintf (stderr, "%s:%d: Allocating: [%p / %d]\n", name, line, ret, size); */
149 void *dicalloc (size_t num, size_t size, const char *name, int line)
151 void *ret = (void *) calloc (num, size);
156 (message ("Out of memory. Allocating %w bytes at %s:%d.",
157 size_toLongUnsigned (size),
158 cstring_fromChars (name), line));
164 void *direalloc (/*@out@*/ /*@null@*/ void *x, size_t size,
165 char *name, int line)
171 ret = (void *) dmalloc (size);
175 ret = (void *) realloc (x, size);
181 (message ("Out of memory. Allocating %w bytes at %s:%d.",
182 size_toLongUnsigned (size),
183 cstring_fromChars (name), line));
191 bool firstWord (char *s, char *w)
193 llassert (s != NULL);
194 llassert (w != NULL);
196 for (; *w != '\0'; w++, s++)
198 if (*w != *s || *s == '\0')
204 void mstring_markFree (char *s)
209 char *mstring_spaces (int n)
217 ret = (char *) dmalloc (size_fromInt (n + 1));
220 for (i = 0; i < n; i++)
230 bool mstring_containsChar (const char *s, char c)
232 if (mstring_isDefined (s))
234 return (strchr (s, c) != NULL);
242 bool mstring_containsString (const char *s, const char *c)
244 if (mstring_isDefined (s))
246 return (strstr (s, c) != NULL);
254 char *mstring_concat (const char *s1, const char *s2)
256 char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1);
262 extern /*@only@*/ char *
263 mstring_concatFree (/*@only@*/ char *s1, /*@only@*/ char *s2)
265 /* like mstring_concat but deallocates old strings */
266 char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1);
275 extern /*@only@*/ char *
276 mstring_concatFree1 (/*@only@*/ char *s1, const char *s2)
278 char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1);
286 extern /*@only@*/ char *
287 mstring_append (/*@only@*/ char *s1, char c)
289 size_t l = strlen (s1);
292 s = (char *) dmalloc (sizeof (*s) * (l + 2));
302 char *mstring_copy (char *s1) /*@ensures maxRead(result) == maxRead(s1) /\ maxSet(result) == maxSet(s1) @*/
310 char *s = (char *) dmalloc ((strlen (s1) + 1) * sizeof (*s));
317 char *mstring_safePrint (char *s)
321 return ("<undefined>");
330 char *mstring_create (size_t n)
334 s = dmalloc (sizeof (*s) * (n + 1));
340 fputline (FILE *out, char *s)
344 check (fputs (s, out) != EOF);
347 check (fputc ('\n', out) == (int) '\n');
350 unsigned int int_toNonNegative (int x) /*@*/
371 longUnsigned_fromInt (int x)
375 return (long unsigned) x;
378 size_t size_fromInt (int x) /*@ensures result==x@*/
380 size_t res = (size_t) x;
382 llassert ((int) res == x);
386 size_t size_fromLong (long x) /*@ensures result==x@*/
388 size_t res = (size_t) x;
390 llassert ((long) res == x);
394 size_t size_fromLongUnsigned (unsigned long x) /*@ensures result==x@*/
396 size_t res = (size_t) x;
398 llassert ((unsigned long) res == x);
402 int size_toInt (size_t x)
406 llassert ((size_t) res == x);
410 long size_toLong (size_t x)
414 llassert ((size_t) res == x);
424 ** evans 2001-09-28 - changed assertion in response to Anthony Giorgio's comment
425 ** that the old assertions failed for EBCDIC character set. Now we just check
426 ** that the result is equal.
430 llassert ((int) res == x);
436 longUnsigned_toInt (long unsigned int x)
440 llassert ((long unsigned) res == x);
445 long_toInt (long int x)
449 /*@+ignorequals@*/ llassert (res == x); /*@=ignorequals@*/
455 bool mstring_equalPrefix (const char *c1, const char *c2)
457 llassert (c1 != NULL);
458 llassert (c2 != NULL);
460 if (strncmp(c1, c2, strlen(c2)) == 0)
470 bool mstring_equal (/*@null@*/ const char *s1, /*@null@*/ const char *s2)
484 return (strcmp(s1, s2) == 0);