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"
30 # include "cgrammar.h"
31 # include "cgrammar_tokens.h"
34 stateClause_createRaw (stateConstraint st, stateClauseKind sk, /*@only@*/ sRefSet s)
36 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
40 ret->squal = qual_createUnknown ();
42 ret->loc = fileloc_undefined;
46 /*drl added 3/7/2003*/
47 bool stateClause_hasEmptyReferences (stateClause s)
49 if (sRefSet_isUndefined(s->refs) )
55 bool stateClause_isMetaState (stateClause s)
58 if (qual_isMetaState (s->squal) )
66 stateClause_create (lltok tok, qual q, sRefSet s)
68 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
70 if (lltok_getTok (tok) == QPRECLAUSE)
72 ret->state = TK_BEFORE;
74 else if (lltok_getTok (tok) == QPOSTCLAUSE)
76 ret->state = TK_AFTER;
83 ret->loc = fileloc_copy (lltok_getLoc (tok));
88 if (sRefSet_isDefined (s))
94 ret->kind = SP_GLOBAL;
100 bool stateClause_isBeforeOnly (stateClause cl)
102 return (cl->state == TK_BEFORE);
105 bool stateClause_isBefore (stateClause cl)
107 return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
110 bool stateClause_isAfter (stateClause cl)
112 return (cl->state == TK_AFTER || cl->state == TK_BOTH);
115 bool stateClause_isEnsures (stateClause cl)
117 return (cl->state == TK_AFTER);
120 bool stateClause_isQual (stateClause cl)
122 return (cl->kind == SP_QUAL);
125 bool stateClause_isMemoryAllocation (stateClause cl)
139 return (qual_isMemoryAllocation (cl->squal)
140 || qual_isSharing (cl->squal));
147 ** An error is reported if the test is NOT true.
151 /* Microsoft doesn't believe in higher order functions... */
\r
152 # pragma warning( disable : 4550 )
\r
155 sRefTest stateClause_getPreTestFunction (stateClause cl)
160 return sRef_isStrictReadable;
162 return sRef_hasNoStorage;
164 return sRef_hasNoStorage;
166 return sRef_isNotUndefined;
168 return sRef_isNotUndefined;
173 if (qual_isOnly (cl->squal)) {
175 } else if (qual_isShared (cl->squal)) {
176 return sRef_isShared;
177 } else if (qual_isDependent (cl->squal)) {
178 return sRef_isDependent;
179 } else if (qual_isOwned (cl->squal)) {
181 } else if (qual_isObserver (cl->squal)) {
182 return sRef_isObserver;
183 } else if (qual_isExposed (cl->squal)) {
184 return sRef_isExposed;
185 } else if (qual_isNotNull (cl->squal)) {
186 return sRef_isNotNull;
187 } else if (qual_isIsNull (cl->squal)) {
188 return sRef_isDefinitelyNull;
198 sRefTest stateClause_getPostTestFunction (stateClause cl)
200 llassert (stateClause_isAfter (cl));
207 return sRef_isAllocated;
209 return sRef_isReallyDefined;
211 return sRef_isReallyDefined;
213 return sRef_isDeadStorage;
217 if (qual_isOnly (cl->squal)) {
219 } else if (qual_isShared (cl->squal)) {
220 return sRef_isShared;
221 } else if (qual_isDependent (cl->squal)) {
222 return sRef_isDependent;
223 } else if (qual_isOwned (cl->squal)) {
225 } else if (qual_isObserver (cl->squal)) {
226 return sRef_isObserver;
227 } else if (qual_isExposed (cl->squal)) {
228 return sRef_isExposed;
229 } else if (qual_isNotNull (cl->squal)) {
230 return sRef_isNotNull;
231 } else if (qual_isIsNull (cl->squal)) {
232 return sRef_isDefinitelyNull;
241 sRefShower stateClause_getPostTestShower (stateClause cl)
250 return sRef_showNotReallyDefined;
256 if (qual_isMemoryAllocation (cl->squal)) {
257 return sRef_showAliasInfo;
258 } else if (qual_isSharing (cl->squal)) {
259 return sRef_showExpInfo;
260 } else if (qual_isIsNull (cl->squal) || qual_isNotNull (cl->squal)) {
261 return sRef_showNullInfo;
270 sRefMod stateClause_getEntryFunction (stateClause cl)
272 if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
277 return sRef_setDefinedComplete;
279 return sRef_setUndefined; /* evans 2002-01-01 */
281 return sRef_setUndefined; /* evans 2002-01-01 */
283 return sRef_setAllocatedComplete;
285 return sRef_setDefinedComplete;
289 if (qual_isOnly (cl->squal)) {
291 } else if (qual_isShared (cl->squal)) {
292 return sRef_setShared;
293 } else if (qual_isDependent (cl->squal)) {
294 return sRef_setDependent;
295 } else if (qual_isOwned (cl->squal)) {
296 return sRef_setOwned;
297 } else if (qual_isObserver (cl->squal)) {
298 return sRef_setObserver;
299 } else if (qual_isExposed (cl->squal)) {
300 return sRef_setExposed;
301 } else if (qual_isNotNull (cl->squal)) {
302 return sRef_setNotNull;
303 } else if (qual_isIsNull (cl->squal)) {
304 return sRef_setDefNull;
306 DPRINTF (("Here we are: %s",
307 qual_unparse (cl->squal)));
322 sRefMod stateClause_getEffectFunction (stateClause cl)
324 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
331 return sRef_setAllocatedComplete;
333 return sRef_setDefinedNCComplete;
335 return sRef_setDefinedNCComplete;
337 return sRef_killComplete;
341 if (qual_isOnly (cl->squal)) {
343 } else if (qual_isShared (cl->squal)) {
344 return sRef_setShared;
345 } else if (qual_isDependent (cl->squal)) {
346 return sRef_setDependent;
347 } else if (qual_isOwned (cl->squal)) {
348 return sRef_setOwned;
349 } else if (qual_isObserver (cl->squal)) {
350 return sRef_setObserver;
351 } else if (qual_isExposed (cl->squal)) {
352 return sRef_setExposed;
353 } else if (qual_isNotNull (cl->squal)) {
354 return sRef_setNotNull;
355 } else if (qual_isIsNull (cl->squal)) {
356 return sRef_setDefNull;
372 sRefMod stateClause_getReturnEffectFunction (stateClause cl)
374 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
387 if (qual_isOnly (cl->squal)) {
388 return sRef_killComplete;
404 static flagcode stateClause_qualErrorCode (stateClause cl)
406 if (qual_isOnly (cl->squal)) {
407 return FLG_ONLYTRANS;
408 } else if (qual_isShared (cl->squal)) {
409 return FLG_SHAREDTRANS;
410 } else if (qual_isDependent (cl->squal)) {
411 return FLG_DEPENDENTTRANS;
412 } else if (qual_isOwned (cl->squal)) {
413 return FLG_OWNEDTRANS;
414 } else if (qual_isObserver (cl->squal)) {
415 return FLG_OBSERVERTRANS;
416 } else if (qual_isExposed (cl->squal)) {
417 return FLG_EXPOSETRANS;
418 } else if (qual_isIsNull (cl->squal)
419 || qual_isNotNull (cl->squal)) {
420 return FLG_NULLSTATE;
425 BADBRANCHRET (INVALID_FLAG);
428 flagcode stateClause_preErrorCode (stateClause cl)
430 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
436 case SP_ALLOCATES: /*@fallthrough@*/
439 return FLG_MUSTFREEONLY;
444 return stateClause_qualErrorCode (cl);
447 BADBRANCHRET (INVALID_FLAG);
450 static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
452 if (qual_isMemoryAllocation (cl->squal)) {
453 return alkind_capName (sRef_getAliasKind (sr));
454 } else if (qual_isObserver (cl->squal)) {
455 return cstring_makeLiteralTemp ("Non-observer");
456 } else if (qual_isExposed (cl->squal)) {
457 if (sRef_isObserver (sr))
459 return cstring_makeLiteralTemp ("Observer");
463 return cstring_makeLiteralTemp ("Non-exposed");
465 } else if (qual_isNotNull (cl->squal)) {
466 if (sRef_isDefinitelyNull (sr))
468 return cstring_makeLiteralTemp ("Null");
472 return cstring_makeLiteralTemp ("Possibly null");
474 } else if (qual_isIsNull (cl->squal)) {
475 return cstring_makeLiteralTemp ("Non-null");
480 BADBRANCHRET (cstring_undefined);
483 cstring stateClause_preErrorString (stateClause cl, sRef sr)
485 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
490 if (sRef_isDead (sr))
491 return cstring_makeLiteralTemp ("Dead");
493 return cstring_makeLiteralTemp ("Undefined");
494 case SP_ALLOCATES: /*@fallthrough@*/
497 return cstring_makeLiteralTemp ("Allocated");
499 if (sRef_isDead (sr))
501 return cstring_makeLiteralTemp ("Dead");
503 else if (sRef_isDependent (sr)
504 || sRef_isShared (sr))
506 return alkind_unparse (sRef_getAliasKind (sr));
508 else if (sRef_isObserver (sr) || sRef_isExposed (sr))
510 return exkind_unparse (sRef_getExKind (sr));
514 return cstring_makeLiteralTemp ("Undefined");
519 return stateClause_qualErrorString (cl, sr);
525 flagcode stateClause_postErrorCode (stateClause cl)
527 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
539 return FLG_MUSTFREEONLY;
543 return stateClause_qualErrorCode (cl);
546 BADBRANCHRET (INVALID_FLAG);
549 cstring stateClause_postErrorString (stateClause cl, sRef sr)
551 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
557 return cstring_makeLiteralTemp ("<ERROR>");
559 return cstring_makeLiteralTemp ("Unallocated");
562 return cstring_makeLiteralTemp ("Undefined");
564 return cstring_makeLiteralTemp ("Unreleased");
568 return stateClause_qualErrorString (cl, sr);
574 cstring stateClause_dump (stateClause s)
576 return (message ("%d.%d.%q.%q",
579 qual_dump (s->squal),
580 sRefSet_dump (s->refs)));
583 stateClause stateClause_undump (char **s)
585 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
587 ret->loc = fileloc_undefined;
588 ret->state = (stateConstraint) reader_getInt (s);
589 reader_checkChar (s, '.');
590 ret->kind = (stateClauseKind) reader_getInt (s);
591 reader_checkChar (s, '.');
592 ret->squal = qual_undump (s);
593 reader_checkChar (s, '.');
594 ret->refs = sRefSet_undump (s);
599 stateClause stateClause_copy (stateClause s)
601 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
603 ret->state = s->state;
605 ret->squal = s->squal;
606 ret->refs = sRefSet_newCopy (s->refs);
607 ret->loc = fileloc_copy (s->loc);
612 bool stateClause_sameKind (stateClause s1, stateClause s2)
614 return (s1->state == s2->state
615 && s1->kind == s2->kind
616 && qual_match (s1->squal, s2->squal));
619 void stateClause_free (stateClause s)
621 sRefSet_free (s->refs);
622 fileloc_free (s->loc);
626 static /*@observer@*/ cstring
627 stateClauseKind_unparse (stateClause s)
632 return cstring_makeLiteralTemp ("uses");
634 return cstring_makeLiteralTemp ("defines");
636 return cstring_makeLiteralTemp ("allocates");
638 return cstring_makeLiteralTemp ("releases");
640 return cstring_makeLiteralTemp ("sets");
642 return qual_unparse (s->squal);
644 return qual_unparse (s->squal);
650 cstring stateClause_unparseKind (stateClause s)
654 cstring_makeLiteralTemp (s->state == TK_BEFORE
656 : (s->state == TK_AFTER
658 stateClauseKind_unparse (s)));
661 cstring stateClause_unparse (stateClause s)
663 return (message ("%q %q",
664 stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
667 stateClause stateClause_createDefines (sRefSet s)
669 return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
672 stateClause stateClause_createUses (sRefSet s)
674 return (stateClause_createRaw (TK_BOTH, SP_USES, s));
677 stateClause stateClause_createSets (sRefSet s)
679 return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
682 stateClause stateClause_createReleases (sRefSet s)
684 return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
687 stateClause stateClause_createPlain (lltok tok, sRefSet s)
689 switch (lltok_getTok (tok))
692 return stateClause_createUses (s);
694 return stateClause_createDefines (s);
696 return stateClause_createAllocates (s);
698 return stateClause_createSets (s);
700 return stateClause_createReleases (s);
706 BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
709 stateClause stateClause_createAllocates (sRefSet s)
711 return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
714 bool stateClause_matchKind (stateClause s1, stateClause s2)
716 return (s1->state == s2->state && s1->kind == s2->kind
717 && qual_match (s1->squal, s2->squal));
720 bool stateClause_hasEnsures (stateClause cl)
722 return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
725 bool stateClause_hasRequires (stateClause cl)
727 return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
730 bool stateClause_setsMetaState (stateClause cl)
732 return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
733 && qual_isMetaState (cl->squal));
736 qual stateClause_getMetaQual (stateClause cl)
738 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
742 static sRefModVal stateClause_getStateFunction (stateClause cl)
746 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
752 if (qual_isNullStateQual (sq))
754 return (sRefModVal) sRef_setNullState;
756 else if (qual_isExQual (sq))
758 return (sRefModVal) sRef_setExKind;
760 else if (qual_isAliasQual (sq))
762 return (sRefModVal) sRef_setAliasKind;
766 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
773 int stateClause_getStateParameter (stateClause cl)
777 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
783 ** Since this can be many different types of state kinds, we need to allow all
784 ** enum's to be returned as int.
787 if (qual_isNotNull (sq))
791 else if (qual_isIsNull (sq))
795 else if (qual_isNull (sq))
799 else if (qual_isRelNull (sq))
803 else if (qual_isExposed (sq))
807 else if (qual_isObserver (sq))
811 else if (qual_isAliasQual (sq))
813 if (qual_isOnly (sq)) return AK_ONLY;
814 if (qual_isImpOnly (sq)) return AK_IMPONLY;
815 if (qual_isTemp (sq)) return AK_TEMP;
816 if (qual_isOwned (sq)) return AK_OWNED;
817 if (qual_isShared (sq)) return AK_SHARED;
818 if (qual_isUnique (sq)) return AK_UNIQUE;
819 if (qual_isDependent (sq)) return AK_DEPENDENT;
820 if (qual_isKeep (sq)) return AK_KEEP;
821 if (qual_isKept (sq)) return AK_KEPT;
826 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
835 sRefModVal stateClause_getEnsuresFunction (stateClause cl)
837 llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
838 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
839 return stateClause_getStateFunction (cl);
842 sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
844 llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
845 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
846 return stateClause_getStateFunction (cl);
849 /*@observer@*/ fileloc stateClause_loc (stateClause s)