]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
616915dd | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
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. | |
10 | ** | |
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. | |
15 | ** | |
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. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 23 | */ |
24 | /* | |
25 | ** general.c | |
26 | */ | |
27 | ||
1b8ae690 | 28 | # include "splintMacros.nf" |
616915dd | 29 | # include "basic.h" |
4caf866b | 30 | |
616915dd | 31 | # undef malloc |
32 | # undef realloc | |
33 | # undef calloc | |
34 | ||
35 | # ifdef USEDMALLOC | |
36 | # include "dmalloc.h" | |
37 | # endif | |
38 | ||
4caf866b | 39 | # include "osd.h" |
616915dd | 40 | |
41 | /* | |
42 | ** redefine undef'd memory ops | |
43 | */ | |
44 | ||
45 | # ifndef USEDMALLOC | |
616915dd | 46 | |
47 | /*@-mustdefine@*/ | |
48 | ||
49 | void sfree (void *x) | |
50 | { | |
51 | if (x != NULL) | |
52 | { | |
28bf4b0b | 53 | /* fprintf (stderr, "Freeing: %p\n", x); */ |
54 | ||
616915dd | 55 | /* |
28bf4b0b | 56 | if ((unsigned long) x > 0xbf000000) { |
616915dd | 57 | fprintf (stderr, "Looks bad!\n"); |
58 | } | |
59 | */ | |
28bf4b0b | 60 | |
616915dd | 61 | free (x); |
28bf4b0b | 62 | |
616915dd | 63 | /* fprintf (stderr, "Done.\n"); */ |
64 | } | |
65 | } | |
66 | # endif | |
67 | ||
68 | void sfreeEventually (void *x) | |
69 | { | |
70 | if (x != NULL) | |
71 | { | |
72 | ; /* should keep in a table */ | |
73 | } | |
74 | /*@-mustfree@*/ | |
75 | } /*@=mustfree@*/ | |
76 | ||
77 | /* | |
78 | ** all memory should be allocated from dimalloc | |
79 | */ | |
80 | ||
81 | static long unsigned size_toLongUnsigned (size_t x) | |
82 | { | |
83 | long unsigned res = (long unsigned) x; | |
84 | ||
85 | llassert ((size_t) res == x); | |
86 | return res; | |
87 | } | |
88 | ||
28bf4b0b | 89 | /*@out@*/ void *dimalloc (size_t size, const char *name, int line) |
86d93ed3 | 90 | /*@ensures maxSet(result) == (size - 1); @*/ |
616915dd | 91 | { |
92 | /* | |
93 | static void *lastaddr = 0; | |
94 | static int numallocs = 0; | |
95 | static int numbad = 0; | |
96 | */ | |
97 | ||
98 | /* was malloc, use calloc to initialize to zero */ | |
99 | void *ret = (void *) calloc (1, size); | |
100 | ||
101 | /* | |
102 | numallocs++; | |
103 | ||
104 | if (ret < lastaddr) | |
105 | { | |
106 | numbad++; | |
107 | fprintf (stderr, "Bad alloc: %d / %d\n", numbad, numallocs); | |
108 | } | |
109 | ||
110 | lastaddr = ret; | |
111 | */ | |
112 | ||
113 | if (ret == NULL) | |
114 | { | |
115 | if (size == 0) | |
116 | { | |
abd7f895 | 117 | llcontbug (message ("Zero allocation at %q.", |
118 | fileloc_unparseRaw (cstring_fromChars (name), line))); | |
119 | ||
120 | /* | |
121 | ** evans 2002-03-01 | |
122 | ** Return some allocated storage...hope we get lucky. | |
123 | */ | |
124 | ||
125 | return dimalloc (16, name, line); | |
616915dd | 126 | } |
127 | else | |
128 | { | |
a779b61e | 129 | /* drl |
130 | fix this so message doesn't run out of | |
131 | memory*/ | |
132 | ||
133 | llbuglit("Out of memory"); | |
134 | ||
616915dd | 135 | llfatalerrorLoc |
136 | (message ("Out of memory. Allocating %w bytes at %s:%d.", | |
137 | size_toLongUnsigned (size), | |
138 | cstring_fromChars (name), line)); | |
a779b61e | 139 | |
616915dd | 140 | } |
141 | } | |
142 | ||
143 | /*@-null@*/ /* null okay for size = 0 */ | |
28bf4b0b | 144 | /* fprintf (stderr, "%s:%d: Allocating: [%p / %d]\n", name, line, ret, size); */ |
616915dd | 145 | return ret; |
146 | /*@=null@*/ | |
147 | } | |
148 | ||
28bf4b0b | 149 | void *dicalloc (size_t num, size_t size, const char *name, int line) |
616915dd | 150 | { |
151 | void *ret = (void *) calloc (num, size); | |
152 | ||
153 | if (ret == NULL) | |
154 | { | |
155 | llfatalerrorLoc | |
156 | (message ("Out of memory. Allocating %w bytes at %s:%d.", | |
157 | size_toLongUnsigned (size), | |
158 | cstring_fromChars (name), line)); | |
159 | } | |
160 | ||
161 | return ret; | |
162 | } | |
163 | ||
164 | void *direalloc (/*@out@*/ /*@null@*/ void *x, size_t size, | |
165 | char *name, int line) | |
166 | { | |
167 | void *ret; | |
168 | ||
169 | if (x == NULL) | |
170 | { | |
171 | ret = (void *) dmalloc (size); | |
172 | } | |
173 | else | |
174 | { | |
175 | ret = (void *) realloc (x, size); | |
176 | } | |
177 | ||
178 | if (ret == NULL) | |
179 | { | |
180 | llfatalerrorLoc | |
181 | (message ("Out of memory. Allocating %w bytes at %s:%d.", | |
182 | size_toLongUnsigned (size), | |
183 | cstring_fromChars (name), line)); | |
184 | } | |
185 | ||
186 | return ret; | |
187 | } | |
188 | ||
189 | /*@=mustdefine@*/ | |
190 | ||
616915dd | 191 | bool firstWord (char *s, char *w) |
192 | { | |
193 | llassert (s != NULL); | |
194 | llassert (w != NULL); | |
195 | ||
196 | for (; *w != '\0'; w++, s++) | |
197 | { | |
198 | if (*w != *s || *s == '\0') | |
199 | return FALSE; | |
200 | } | |
201 | return TRUE; | |
202 | } | |
616915dd | 203 | |
616915dd | 204 | void mstring_markFree (char *s) |
205 | { | |
15b3d2b2 | 206 | sfreeEventually (s); |
616915dd | 207 | } |
208 | ||
616915dd | 209 | char *mstring_spaces (int n) |
210 | { | |
211 | int i; | |
212 | char *ret; | |
213 | char *ptr; | |
214 | ||
215 | llassert (n >= 0); | |
216 | ||
217 | ret = (char *) dmalloc (size_fromInt (n + 1)); | |
218 | ptr = ret; | |
219 | ||
220 | for (i = 0; i < n; i++) | |
221 | { | |
222 | *ptr++ = ' '; | |
223 | } | |
224 | ||
225 | *ptr = '\0'; | |
226 | ||
227 | return ret; | |
228 | } | |
28bf4b0b | 229 | |
230 | bool mstring_containsChar (const char *s, char c) | |
231 | { | |
232 | if (mstring_isDefined (s)) | |
233 | { | |
234 | return (strchr (s, c) != NULL); | |
235 | } | |
236 | else | |
237 | { | |
238 | return FALSE; | |
239 | } | |
240 | } | |
68de3f33 | 241 | |
242 | bool mstring_containsString (const char *s, const char *c) | |
243 | { | |
244 | if (mstring_isDefined (s)) | |
245 | { | |
246 | return (strstr (s, c) != NULL); | |
247 | } | |
248 | else | |
249 | { | |
250 | return FALSE; | |
251 | } | |
252 | } | |
616915dd | 253 | |
254 | char *mstring_concat (const char *s1, const char *s2) | |
255 | { | |
256 | char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1); | |
257 | strcpy (s, s1); | |
258 | strcat (s, s2); | |
259 | return s; | |
260 | } | |
261 | ||
262 | extern /*@only@*/ char * | |
263 | mstring_concatFree (/*@only@*/ char *s1, /*@only@*/ char *s2) | |
264 | { | |
265 | /* like mstring_concat but deallocates old strings */ | |
266 | char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1); | |
267 | strcpy (s, s1); | |
268 | strcat (s, s2); | |
269 | ||
270 | sfree (s1); | |
271 | sfree (s2); | |
272 | return s; | |
273 | } | |
274 | ||
275 | extern /*@only@*/ char * | |
276 | mstring_concatFree1 (/*@only@*/ char *s1, const char *s2) | |
277 | { | |
278 | char *s = (char *) dmalloc (strlen (s1) + strlen (s2) + 1); | |
279 | strcpy (s, s1); | |
280 | strcat (s, s2); | |
281 | sfree (s1); | |
282 | ||
283 | return s; | |
284 | } | |
285 | ||
286 | extern /*@only@*/ char * | |
287 | mstring_append (/*@only@*/ char *s1, char c) | |
288 | { | |
289 | size_t l = strlen (s1); | |
290 | char *s; | |
291 | ||
292 | s = (char *) dmalloc (sizeof (*s) * (l + 2)); | |
293 | ||
294 | strcpy (s, s1); | |
295 | *(s + l) = c; | |
296 | *(s + l + 1) = '\0'; | |
297 | sfree (s1); | |
298 | return s; | |
299 | } | |
300 | ||
301 | extern | |
86d93ed3 | 302 | char *mstring_copy (char *s1) /*@ensures maxRead(result) == maxRead(s1) /\ maxSet(result) == maxSet(s1) @*/ |
616915dd | 303 | { |
304 | if (s1 == NULL) | |
305 | { | |
306 | return NULL; | |
307 | } | |
308 | else | |
309 | { | |
310 | char *s = (char *) dmalloc ((strlen (s1) + 1) * sizeof (*s)); | |
311 | strcpy (s, s1); | |
312 | return s; | |
313 | } | |
314 | } | |
315 | ||
316 | extern | |
317 | char *mstring_safePrint (char *s) | |
318 | { | |
319 | if (s == NULL) | |
320 | { | |
321 | return ("<undefined>"); | |
322 | } | |
323 | else | |
324 | { | |
325 | return s; | |
326 | } | |
327 | } | |
328 | ||
329 | extern | |
abd7f895 | 330 | char *mstring_create (size_t n) |
616915dd | 331 | { |
332 | char *s; | |
333 | ||
334 | s = dmalloc (sizeof (*s) * (n + 1)); | |
335 | *s = '\0'; | |
336 | return s; | |
337 | } | |
338 | ||
339 | void | |
340 | fputline (FILE *out, char *s) | |
341 | { | |
342 | if (strlen (s) > 0) | |
343 | { | |
344 | check (fputs (s, out) != EOF); | |
345 | } | |
346 | ||
347 | check (fputc ('\n', out) == (int) '\n'); | |
348 | } | |
349 | ||
86d93ed3 | 350 | unsigned int int_toNonNegative (int x) /*@*/ |
a956d444 | 351 | { |
352 | llassert (x >= 0); | |
353 | return (unsigned) x; | |
354 | } | |
355 | ||
616915dd | 356 | int int_log (int x) |
357 | { | |
358 | int ret = 1; | |
359 | ||
360 | while (x > 10) | |
361 | { | |
362 | ret++; | |
363 | x /= 10; | |
364 | } | |
365 | ||
366 | return ret; | |
367 | } | |
368 | ||
369 | /*@-czechfcns@*/ | |
370 | long unsigned int | |
371 | longUnsigned_fromInt (int x) | |
372 | { | |
373 | llassert (x >= 0); | |
374 | ||
375 | return (long unsigned) x; | |
376 | } | |
377 | ||
86d93ed3 | 378 | size_t size_fromInt (int x) /*@ensures result==x@*/ |
616915dd | 379 | { |
380 | size_t res = (size_t) x; | |
381 | ||
382 | llassert ((int) res == x); | |
383 | return res; | |
384 | } | |
385 | ||
e5081f8c | 386 | size_t size_fromLong (long x) /*@ensures result==x@*/ |
387 | { | |
388 | size_t res = (size_t) x; | |
389 | ||
390 | llassert ((long) res == x); | |
391 | return res; | |
392 | } | |
393 | ||
394 | size_t size_fromLongUnsigned (unsigned long x) /*@ensures result==x@*/ | |
395 | { | |
396 | size_t res = (size_t) x; | |
397 | ||
398 | llassert ((unsigned long) res == x); | |
399 | return res; | |
400 | } | |
401 | ||
616915dd | 402 | int size_toInt (size_t x) |
403 | { | |
404 | int res = (int) x; | |
405 | ||
406 | llassert ((size_t) res == x); | |
407 | return res; | |
408 | } | |
409 | ||
410 | long size_toLong (size_t x) | |
411 | { | |
412 | long res = (long) x; | |
413 | ||
414 | llassert ((size_t) res == x); | |
415 | return res; | |
416 | } | |
417 | ||
418 | /*@=czechfcns@*/ | |
419 | ||
420 | char | |
421 | char_fromInt (int x) | |
422 | { | |
2209bcb7 | 423 | /* |
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. | |
427 | */ | |
616915dd | 428 | |
2209bcb7 | 429 | char res = (char) x; |
430 | llassert ((int) res == x); | |
431 | return res; | |
616915dd | 432 | } |
433 | ||
434 | /*@-czechfcns@*/ | |
435 | int | |
436 | longUnsigned_toInt (long unsigned int x) | |
437 | { | |
438 | int res = (int) x; | |
439 | ||
440 | llassert ((long unsigned) res == x); | |
441 | return res; | |
442 | } | |
443 | ||
444 | int | |
445 | long_toInt (long int x) | |
446 | { | |
447 | int res = (int) x; | |
448 | ||
449 | /*@+ignorequals@*/ llassert (res == x); /*@=ignorequals@*/ | |
450 | return res; | |
451 | } | |
452 | ||
453 | /*@+czechfcns@*/ | |
454 | ||
455 | bool mstring_equalPrefix (const char *c1, const char *c2) | |
456 | { | |
457 | llassert (c1 != NULL); | |
458 | llassert (c2 != NULL); | |
459 | ||
460 | if (strncmp(c1, c2, strlen(c2)) == 0) | |
461 | { | |
462 | return TRUE; | |
463 | } | |
464 | else | |
465 | { | |
466 | return FALSE; | |
467 | } | |
468 | } | |
469 | ||
470 | bool mstring_equal (/*@null@*/ const char *s1, /*@null@*/ const char *s2) | |
471 | { | |
472 | if (s1 == NULL) | |
473 | { | |
474 | return (s2 == NULL); | |
475 | } | |
476 | else | |
477 | { | |
478 | if (s2 == NULL) | |
479 | { | |
480 | return FALSE; | |
481 | } | |
482 | else | |
483 | { | |
484 | return (strcmp(s1, s2) == 0); | |
485 | } | |
486 | } | |
487 | } | |
488 |