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
27 ** based on set_template.c
29 ** where T has T_equal (or change this) and T_unparse
32 # include "splintMacros.nf"
38 return sRefSet_undefined;
41 static /*@notnull@*/ /*@only@*/ sRefSet
42 sRefSet_newEmpty (void)
44 sRefSet s = (sRefSet) dmalloc (sizeof (*s));
47 s->nspace = sRefSetBASESIZE;
48 s->elements = (sRef *) dmalloc (sizeof (*s->elements) * sRefSetBASESIZE);
54 sRefSet_single (/*@exposed@*/ sRef sr)
56 sRefSet s = (sRefSet) dmalloc (sizeof (*s));
59 s->nspace = sRefSetBASESIZE - 1;
60 s->elements = (sRef *) dmalloc (sizeof (*s->elements) * sRefSetBASESIZE);
67 sRefSet_grow (/*@notnull@*/ sRefSet s)
72 s->nspace = sRefSetBASESIZE;
73 newelements = (sRef *) dmalloc (sizeof (*newelements) * (s->entries + s->nspace));
75 for (i = 0; i < s->entries; i++)
77 newelements[i] = s->elements[i];
81 s->elements = newelements;
85 sRefSet_insert (sRefSet s, /*@exposed@*/ sRef el)
87 if (sRefSet_isUndefined (s))
89 s = sRefSet_newEmpty ();
93 if (!sRefSet_isSameMember (s, el))
101 llassert (s->elements != NULL);
102 s->elements[s->entries] = el;
114 sRefSet_clear (sRefSet s)
116 if (sRefSet_isDefined (s))
118 s->nspace += s->entries;
124 ** slow algorithm...but it doesn't matter
128 sRefSet_clearStatics (sRefSet s)
130 if (sRefSet_isDefined (s))
134 for (i = 0; i < s->entries; i++)
136 sRef current = s->elements[i];
138 if (sRef_isFileStatic (sRef_getRootBase (current)))
142 for (j = i; j < s->entries - 1; j++)
144 s->elements[j] = s->elements[j+1];
156 sRefSet_delete (sRefSet s, sRef el)
160 if (sRefSet_isUndefined (s)) return FALSE;
162 if (s->elements != NULL)
164 for (i = 0; i < s->entries; i++)
166 sRef current = s->elements[i];
168 if (sRef_realSame (el, current))
172 for (j = i; j < s->entries - 1; j++)
174 s->elements[j] = s->elements[j+1];
188 sRefSet_choose (sRefSet s)
190 llassert (sRefSet_isDefined (s));
191 llassert (s->entries > 0);
192 llassert (s->elements != NULL);
194 return (s->elements[0]);
198 sRefSet_mergeIntoOne (sRefSet s)
203 if (sRefSet_isUndefined (s)) return sRef_undefined;
204 if (s->entries == 0) return sRef_undefined;
206 llassert (s->elements != NULL);
208 res = s->elements[0];
210 for (i = 1; i < s->entries; i++)
214 tmp = sRef_makeConj (res, s->elements[i]);
222 ** this is really yucky...but it works...
226 sRefSet_deleteBase (sRefSet s, sRef base)
231 if (sRefSet_isUndefined (s) || (s->elements == NULL))
236 while (i + offset < s->entries)
238 sRef current = s->elements[i + offset];
240 while (sRef_includedBy (current, base))
243 if (i + offset >= s->entries) goto doneLoop;
244 current = s->elements [i + offset];
249 s->elements [i] = current;
256 s->entries -= offset;
267 sRefSet_unionFree (/*@returned@*/ sRefSet s1, sRefSet s2)
269 sRefSet res = sRefSet_union (s1, s2);
276 sRefSet_union (/*@returned@*/ sRefSet s1, sRefSet s2)
283 if (sRefSet_isEmpty (s1))
285 s1 = sRefSet_copyInto (s1, s2);
289 sRefSet_allElements (s2, el)
291 s1 = sRefSet_insert (s1, el);
292 } end_sRefSet_allElements;
299 ** s1 <- s1 U (s2 - ex - params)
303 sRefSet_unionExcept (/*@returned@*/ sRefSet s1, sRefSet s2, sRef ex)
305 if (s1 == s2) return s1;
307 sRefSet_allElements (s2, el)
309 if (sRef_same (el, ex))
315 s1 = sRefSet_insert (s1, el);
317 } end_sRefSet_allElements;
323 sRefSet_realNewUnion (sRefSet s1, sRefSet s2)
325 llassert (NOALIAS (s1, s2));
327 if (sRefSet_isUndefined (s1))
329 return (sRefSet_newCopy (s2));
333 sRefSet ret = sRefSet_newCopy (s1);
335 sRefSet_allElements (s2, el)
337 ret = sRefSet_insert (ret, el);
338 } end_sRefSet_allElements;
347 sRefSet_intersect (sRefSet s1, sRefSet s2)
349 sRefSet s = sRefSet_new ();
351 llassert (NOALIAS (s1, s2));
353 sRefSet_allElements (s1, el)
355 if (sRefSet_member (s2, el))
357 s = sRefSet_insert (s, el);
359 } end_sRefSet_allElements;
365 sRefSet_levelUnion (/*@returned@*/ sRefSet sr, sRefSet s, int lexlevel)
367 llassert (NOALIAS (sr, s));
369 sRefSet_allElements (s, el)
371 if (sRef_lexLevel (el) <= lexlevel)
373 sr = sRefSet_insert (sr, el);
375 } end_sRefSet_allElements;
381 sRefSet_levelPrune (sRefSet s, int lexlevel)
383 if (sRefSet_isDefined (s))
386 int backcount = sRefSet_size (s) - 1;
388 for (i = 0; i <= backcount; i++)
390 sRef el = s->elements[i];
392 if (sRef_lexLevel (el) > lexlevel)
397 for (j = backcount; j > i; j--)
403 if (sRef_lexLevel (s->elements[j]) <= lexlevel)
405 s->elements[i] = s->elements[j];
407 if (backcount == i) s->entries++;
408 /*@innerbreak@*/ break;
425 sRefSet sRefSet_copyInto (/*@returned@*/ sRefSet s1, /*@exposed@*/ sRefSet s2)
429 llassert (NOALIAS (s1, s2));
431 if (sRefSet_isUndefined (s1))
433 if (sRefSet_isEmpty (s2))
439 s1 = sRefSet_newEmpty ();
443 origentries = s1->entries;
445 s1->nspace = s1->entries + s1->nspace;
448 sRefSet_allElements (s2, el)
455 s1->elements[s1->entries] = el;
458 } end_sRefSet_allElements;
464 sRefSet_newCopy (/*@exposed@*/ sRefSet s)
466 if (sRefSet_isEmpty (s))
468 return sRefSet_undefined;
472 sRefSet r = (sRefSet) dmalloc (sizeof (*r));
475 r->entries = s->entries;
476 r->nspace = s->nspace;
477 r->elements = (sRef *) dmalloc (sizeof (*r->elements) * (s->entries + s->nspace));
479 for (i = 0; i < s->entries; i++)
481 r->elements[i] = s->elements[i];
489 sRefSet_levelCopy (/*@exposed@*/ sRefSet s, int lexlevel)
491 if (sRefSet_isEmpty (s))
493 return sRefSet_undefined;
497 sRefSet r = (sRefSet) dmalloc (sizeof (*r));
500 r->nspace = s->entries;
502 r->elements = (sRef *) dmalloc (sizeof (*r->elements) * (s->entries));
504 for (i = 0; i < s->entries; i++)
506 if (sRef_lexLevel (s->elements[i]) <= lexlevel)
508 r->elements[r->entries] = s->elements[i];
519 sRefSet_newDeepCopy (sRefSet s)
521 if (sRefSet_isUndefined (s))
523 return sRefSet_newEmpty ();
527 sRefSet r = (sRefSet) dmalloc (sizeof (*r));
530 r->entries = s->entries;
531 r->nspace = s->nspace;
532 r->elements = (sRef *) dmalloc (sizeof (*r->elements) * (s->entries + s->nspace));
534 for (i = 0; i < s->entries; i++)
536 r->elements[i] = sRef_copy (s->elements[i]);
544 sRefSet_isElementCompare (bool (*test)(sRef, sRef), sRefSet s, sRef el)
546 sRefSet_allElements (s, e)
552 } end_sRefSet_allElements;
558 sRefSet_isElementTest (bool (*test)(sRef), sRefSet s)
560 sRefSet_allElements (s, e)
566 } end_sRefSet_allElements;
572 sRefSet_hasRealElement (sRefSet s)
574 sRefSet_allElements (s, e)
576 if (sRef_isMeaningful (e) && !sRef_isUnconstrained (e))
580 } end_sRefSet_allElements;
586 sRefSet_containsSameObject (sRefSet s, sRef el)
588 return (sRefSet_isElementCompare (sRef_sameObject, s, el));
592 sRefSet_isSameMember (sRefSet s, sRef el)
594 return (sRefSet_isElementCompare (sRef_realSame, s, el));
598 sRefSet_isSameNameMember (sRefSet s, sRef el)
600 return (sRefSet_isElementCompare (sRef_sameName, s, el));
604 sRefSet_member (sRefSet s, sRef el)
606 return (sRefSet_isElementCompare (sRef_similar, s, el));
610 sRefSet_hasStatic (sRefSet s)
612 return (sRefSet_isElementTest (sRef_isFileStatic, s));
616 sRefSet_hasUnconstrained (sRefSet s)
618 return (sRefSet_isElementTest (sRef_isUnconstrained, s));
622 sRefSet_unparseUnconstrained (sRefSet s)
625 cstring res = cstring_undefined;
627 sRefSet_allElements (s, el)
629 if (sRef_isUnconstrained (el))
631 if (cstring_isUndefined (res))
633 res = cstring_copy (sRef_unconstrainedName (el));
637 res = message ("%q, %s", res, sRef_unconstrainedName (el));
642 } end_sRefSet_allElements ;
646 llassert (cstring_isUndefined (res));
647 return (cstring_makeLiteral ("<ERROR: no unconstrained calls>"));
651 return (message ("unconstrained function %q", res));
655 return (message ("unconstrained functions %q", res));
660 sRefSet_unparseUnconstrainedPlain (sRefSet s)
662 cstring res = cstring_undefined;
664 sRefSet_allElements (s, el)
666 if (sRef_isUnconstrained (el))
668 if (cstring_isUndefined (res))
670 res = cstring_copy (sRef_unconstrainedName (el));
674 res = message ("%q, %s", res, sRef_unconstrainedName (el));
677 } end_sRefSet_allElements ;
683 sRefSet_modifyMember (sRefSet s, sRef m)
687 sRefSet_allElements (s, e)
689 if (sRef_similar (m, e))
691 sRef_setModified (e);
694 } end_sRefSet_allElements;
701 sRefSet_lookupMember (sRefSet s, sRef el)
703 sRefSet_allElements (s, e)
705 if (sRef_similar (el, e))
709 } end_sRefSet_allElements;
711 return sRef_undefined;
714 int sRefSet_size (sRefSet s)
716 if (sRefSet_isUndefined (s)) return 0;
721 sRefSet_unparse (sRefSet s)
724 cstring st = cstring_makeLiteral ("{");
726 if (sRefSet_isDefined (s))
728 for (i = 0; i < sRefSet_size (s); i++)
731 st = message ("%q %q", st, sRef_unparse (s->elements[i]));
733 st = message ("%q, %q", st, sRef_unparse (s->elements[i]));
737 st = message ("%q }", st);
741 cstring sRefSet_unparsePlain (sRefSet s)
744 cstring st = cstring_undefined;
746 if (sRefSet_isDefined (s))
748 for (i = 0; i < sRefSet_size (s); i++)
751 st = sRef_unparse (s->elements[i]);
753 st = message ("%q, %q", st, sRef_unparse (s->elements[i]));
761 sRefSet_unparseDebug (sRefSet s)
764 cstring st = cstring_makeLiteral ("{");
766 if (sRefSet_isDefined (s))
768 for (i = 0; i < sRefSet_size (s); i++)
772 st = message ("%q %q", st, sRef_unparseDebug (s->elements[i]));
776 st = message ("%q, %q", st, sRef_unparseDebug (s->elements[i]));
781 st = message ("%q }", st);
786 sRefSet_unparseFull (sRefSet s)
789 cstring st = cstring_makeLiteral ("{");
791 if (sRefSet_isDefined (s))
793 for (i = 0; i < sRefSet_size (s); i++)
797 st = message ("%q %q", st, sRef_unparseFull (s->elements[i]));
801 st = message ("%q, %q", st, sRef_unparseFull (s->elements[i]));
806 st = message ("%q }", st);
811 sRefSet_fixSrefs (sRefSet s)
813 if (sRefSet_isDefined (s))
817 for (i = 0; i < sRefSet_size (s); i++)
819 sRef current = s->elements[i];
821 if (sRef_isLocalVar (current))
823 s->elements[i] = uentry_getSref (sRef_getUentry (current));
830 sRefSet_free (/*@only@*/ sRefSet s)
832 if (!sRefSet_isUndefined (s))
834 llassertprint (s->entries < 1000, ("sRefSet free size: %d", s->entries));
841 sRefSet sRefSet_removeIndirection (sRefSet s)
844 ** returns a NEW sRefSet containing references to all sRef's in s
847 sRefSet t = sRefSet_new ();
850 sRefSet_allElements (s, el)
852 if (!sRef_isAddress (el))
854 t = sRefSet_insert (t, sRef_makeAddress (el));
856 } end_sRefSet_allElements;
861 sRefSet sRefSet_addIndirection (sRefSet s)
864 ** returns a NEW sRefSet containing references to all sRef's in s
867 sRefSet t = sRefSet_new ();
870 sRefSet_allElements (s, el)
872 ctype ct = ctype_realType (sRef_getType (el));
875 if ((ctype_isArrayPtr (ct)))
878 sRef a = sRef_constructPointer (el);
879 t = sRefSet_insert (t, a);
881 } end_sRefSet_allElements;
886 sRefSet sRefSet_accessField (sRefSet s, /*@observer@*/ cstring f)
889 ** returns a NEW sRefSet containing references to all sRef's in s
892 sRefSet t = sRefSet_new ();
894 sRefSet_allElements (s, el)
896 ctype ct = ctype_realType (sRef_getType (el));
898 if ((ctype_isStruct (ct) || ctype_isUnion (ct))
899 && (!uentry_isUndefined (uentryList_lookupField (ctype_getFields (ct), f))))
901 t = sRefSet_insert (t, sRef_makeNCField (el, f));
903 } end_sRefSet_allElements;
908 sRefSet sRefSet_fetchUnknown (sRefSet s)
910 sRefSet t = sRefSet_new ();
912 sRefSet_allElements (s, el)
914 ctype ct = ctype_realType (sRef_getType (el));
916 if (ctype_isArrayPtr (ct))
918 t = sRefSet_insert (t, sRef_makeArrayFetch (el));
920 } end_sRefSet_allElements;
925 sRefSet sRefSet_fetchKnown (sRefSet s, int i)
927 sRefSet t = sRefSet_new ();
929 sRefSet_allElements (s, el)
931 ctype ct = ctype_realType (sRef_getType (el));
933 if (ctype_isArrayPtr (ct))
935 t = sRefSet_insert (t, sRef_makeArrayFetchKnown (el, i));
937 } end_sRefSet_allElements;
942 int sRefSet_compare (sRefSet s1, sRefSet s2)
944 sRefSet_allElements (s1, el)
946 if (!sRefSet_isSameMember (s2, el))
950 } end_sRefSet_allElements;
952 sRefSet_allElements (s2, el)
954 if (!sRefSet_isSameMember (s1, el))
958 } end_sRefSet_allElements;
963 bool sRefSet_equal (sRefSet s1, sRefSet s2)
965 sRefSet_allElements (s1, el)
967 if (!sRefSet_isSameMember (s2, el))
971 } end_sRefSet_allElements;
973 sRefSet_allElements (s2, el)
975 if (!sRefSet_isSameMember (s1, el))
979 } end_sRefSet_allElements;
985 sRefSet_undump (char **s)
988 sRefSet sl = sRefSet_new ();
990 while ((c = **s) != '#' && c != '@' && c != '$' && c != '&')
992 sl = sRefSet_insert (sl, sRef_undump (s));
1005 sRefSet_dump (sRefSet sl)
1007 cstring st = cstring_undefined;
1011 sRefSet_allElements (sl, el)
1015 st = cstring_appendChar (st, ',');
1022 st = cstring_concatFree (st, sRef_dump (el));
1023 } end_sRefSet_allElements;
1029 sRefSet_markImmutable (sRefSet s)
1031 sRefSet_allElements (s, el)
1033 sRef_markImmutable (el);
1034 } end_sRefSet_allElements;