2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
21 ** To report a bug: lclint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
28 # include "lclintMacros.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;
47 stateClause_create (lltok tok, qual q, sRefSet s)
49 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
51 if (lltok_getTok (tok) == QPRECLAUSE)
53 ret->state = TK_BEFORE;
55 else if (lltok_getTok (tok) == QPOSTCLAUSE)
57 ret->state = TK_AFTER;
64 ret->loc = fileloc_copy (lltok_getLoc (tok));
69 if (sRefSet_isDefined (s))
75 ret->kind = SP_GLOBAL;
81 bool stateClause_isBeforeOnly (stateClause cl)
83 return (cl->state == TK_BEFORE);
86 bool stateClause_isBefore (stateClause cl)
88 return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
91 bool stateClause_isAfter (stateClause cl)
93 return (cl->state == TK_AFTER || cl->state == TK_BOTH);
96 bool stateClause_isEnsures (stateClause cl)
98 return (cl->state == TK_AFTER);
101 bool stateClause_isMemoryAllocation (stateClause cl)
115 return (qual_isMemoryAllocation (cl->squal)
116 || qual_isSharing (cl->squal));
123 ** An error is reported if the test is NOT true.
126 sRefTest stateClause_getPreTestFunction (stateClause cl)
131 return sRef_isStrictReadable;
133 return sRef_hasNoStorage;
135 return sRef_hasNoStorage;
137 return sRef_isNotUndefined;
139 return sRef_isNotUndefined;
144 if (qual_isOnly (cl->squal)) {
146 } else if (qual_isShared (cl->squal)) {
147 return sRef_isShared;
148 } else if (qual_isDependent (cl->squal)) {
149 return sRef_isDependent;
150 } else if (qual_isOwned (cl->squal)) {
152 } else if (qual_isObserver (cl->squal)) {
153 return sRef_isObserver;
154 } else if (qual_isExposed (cl->squal)) {
155 return sRef_isExposed;
156 } else if (qual_isNotNull (cl->squal)) {
157 return sRef_isNotNull;
158 } else if (qual_isIsNull (cl->squal)) {
159 return sRef_isDefinitelyNull;
169 sRefTest stateClause_getPostTestFunction (stateClause cl)
171 llassert (stateClause_isAfter (cl));
178 return sRef_isAllocated;
180 return sRef_isReallyDefined;
182 return sRef_isReallyDefined;
184 return sRef_isDeadStorage;
188 if (qual_isOnly (cl->squal)) {
190 } else if (qual_isShared (cl->squal)) {
191 return sRef_isShared;
192 } else if (qual_isDependent (cl->squal)) {
193 return sRef_isDependent;
194 } else if (qual_isOwned (cl->squal)) {
196 } else if (qual_isObserver (cl->squal)) {
197 return sRef_isObserver;
198 } else if (qual_isExposed (cl->squal)) {
199 return sRef_isExposed;
200 } else if (qual_isNotNull (cl->squal)) {
201 return sRef_isNotNull;
202 } else if (qual_isIsNull (cl->squal)) {
203 return sRef_isDefinitelyNull;
212 sRefShower stateClause_getPostTestShower (stateClause cl)
221 return sRef_showNotReallyDefined;
227 if (qual_isMemoryAllocation (cl->squal)) {
228 return sRef_showAliasInfo;
229 } else if (qual_isSharing (cl->squal)) {
230 return sRef_showExpInfo;
231 } else if (qual_isIsNull (cl->squal) || qual_isNotNull (cl->squal)) {
232 return sRef_showNullInfo;
241 sRefMod stateClause_getEntryFunction (stateClause cl)
243 if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
248 return sRef_setDefinedComplete;
254 return sRef_setAllocatedComplete;
256 return sRef_setDefinedComplete;
260 if (qual_isOnly (cl->squal)) {
262 } else if (qual_isShared (cl->squal)) {
263 return sRef_setShared;
264 } else if (qual_isDependent (cl->squal)) {
265 return sRef_setDependent;
266 } else if (qual_isOwned (cl->squal)) {
267 return sRef_setOwned;
268 } else if (qual_isObserver (cl->squal)) {
269 return sRef_setObserver;
270 } else if (qual_isExposed (cl->squal)) {
271 return sRef_setExposed;
272 } else if (qual_isNotNull (cl->squal)) {
273 return sRef_setNotNull;
274 } else if (qual_isIsNull (cl->squal)) {
275 return sRef_setDefNull;
277 DPRINTF (("Here we are: %s",
278 qual_unparse (cl->squal)));
293 sRefMod stateClause_getEffectFunction (stateClause cl)
295 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
302 return sRef_setAllocatedComplete;
304 return sRef_setDefinedNCComplete;
306 return sRef_setDefinedNCComplete;
308 return sRef_killComplete;
312 if (qual_isOnly (cl->squal)) {
314 } else if (qual_isShared (cl->squal)) {
315 return sRef_setShared;
316 } else if (qual_isDependent (cl->squal)) {
317 return sRef_setDependent;
318 } else if (qual_isOwned (cl->squal)) {
319 return sRef_setOwned;
320 } else if (qual_isObserver (cl->squal)) {
321 return sRef_setObserver;
322 } else if (qual_isExposed (cl->squal)) {
323 return sRef_setExposed;
324 } else if (qual_isNotNull (cl->squal)) {
325 return sRef_setNotNull;
326 } else if (qual_isIsNull (cl->squal)) {
327 return sRef_setDefNull;
343 sRefMod stateClause_getReturnEffectFunction (stateClause cl)
345 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
358 if (qual_isOnly (cl->squal)) {
359 return sRef_killComplete;
375 static flagcode stateClause_qualErrorCode (stateClause cl)
377 if (qual_isOnly (cl->squal)) {
378 return FLG_ONLYTRANS;
379 } else if (qual_isShared (cl->squal)) {
380 return FLG_SHAREDTRANS;
381 } else if (qual_isDependent (cl->squal)) {
382 return FLG_DEPENDENTTRANS;
383 } else if (qual_isOwned (cl->squal)) {
384 return FLG_OWNEDTRANS;
385 } else if (qual_isObserver (cl->squal)) {
386 return FLG_OBSERVERTRANS;
387 } else if (qual_isExposed (cl->squal)) {
388 return FLG_EXPOSETRANS;
389 } else if (qual_isIsNull (cl->squal)
390 || qual_isNotNull (cl->squal)) {
391 return FLG_NULLSTATE;
396 BADBRANCHRET (INVALID_FLAG);
399 flagcode stateClause_preErrorCode (stateClause cl)
401 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
407 case SP_ALLOCATES: /*@fallthrough@*/
415 return stateClause_qualErrorCode (cl);
418 BADBRANCHRET (INVALID_FLAG);
421 static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
423 if (qual_isMemoryAllocation (cl->squal)) {
424 return alkind_capName (sRef_getAliasKind (sr));
425 } else if (qual_isObserver (cl->squal)) {
426 return cstring_makeLiteralTemp ("Non-observer");
427 } else if (qual_isExposed (cl->squal)) {
428 if (sRef_isObserver (sr))
430 return cstring_makeLiteralTemp ("Observer");
434 return cstring_makeLiteralTemp ("Non-exposed");
436 } else if (qual_isNotNull (cl->squal)) {
437 if (sRef_isDefinitelyNull (sr))
439 return cstring_makeLiteralTemp ("Null");
443 return cstring_makeLiteralTemp ("Possibly null");
445 } else if (qual_isIsNull (cl->squal)) {
446 return cstring_makeLiteralTemp ("Non-null");
451 BADBRANCHRET (cstring_undefined);
454 cstring stateClause_preErrorString (stateClause cl, sRef sr)
456 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
461 if (sRef_isDead (sr))
462 return cstring_makeLiteralTemp ("Dead");
464 return cstring_makeLiteralTemp ("Undefined");
465 case SP_ALLOCATES: /*@fallthrough@*/
468 return cstring_makeLiteralTemp ("Allocated");
470 if (sRef_isDead (sr))
472 return cstring_makeLiteralTemp ("Dead");
474 else if (sRef_isDependent (sr)
475 || sRef_isShared (sr))
477 return alkind_unparse (sRef_getAliasKind (sr));
479 else if (sRef_isObserver (sr) || sRef_isExposed (sr))
481 return exkind_unparse (sRef_getExKind (sr));
485 return cstring_makeLiteralTemp ("Undefined");
490 return stateClause_qualErrorString (cl, sr);
496 flagcode stateClause_postErrorCode (stateClause cl)
498 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
514 return stateClause_qualErrorCode (cl);
517 BADBRANCHRET (INVALID_FLAG);
520 cstring stateClause_postErrorString (stateClause cl, sRef sr)
522 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
528 return cstring_makeLiteralTemp ("<ERROR>");
530 return cstring_makeLiteralTemp ("Unallocated");
533 return cstring_makeLiteralTemp ("Undefined");
535 return cstring_makeLiteralTemp ("Unreleased");
539 return stateClause_qualErrorString (cl, sr);
545 cstring stateClause_dump (stateClause s)
547 return (message ("%d.%d.%q.%q",
550 qual_dump (s->squal),
551 sRefSet_dump (s->refs)));
554 stateClause stateClause_undump (char **s)
556 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
558 ret->loc = fileloc_undefined;
559 ret->state = (stateConstraint) reader_getInt (s);
560 reader_checkChar (s, '.');
561 ret->kind = (stateClauseKind) reader_getInt (s);
562 reader_checkChar (s, '.');
563 ret->squal = qual_undump (s);
564 reader_checkChar (s, '.');
565 ret->refs = sRefSet_undump (s);
570 stateClause stateClause_copy (stateClause s)
572 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
574 ret->state = s->state;
576 ret->squal = s->squal;
577 ret->refs = sRefSet_newCopy (s->refs);
578 ret->loc = fileloc_copy (s->loc);
583 bool stateClause_sameKind (stateClause s1, stateClause s2)
585 return (s1->state == s2->state
586 && s1->kind == s2->kind
587 && qual_match (s1->squal, s2->squal));
590 void stateClause_free (stateClause s)
592 sRefSet_free (s->refs);
593 fileloc_free (s->loc);
597 static /*@observer@*/ cstring
598 stateClauseKind_unparse (stateClause s)
603 return cstring_makeLiteralTemp ("uses");
605 return cstring_makeLiteralTemp ("defines");
607 return cstring_makeLiteralTemp ("allocates");
609 return cstring_makeLiteralTemp ("releases");
611 return cstring_makeLiteralTemp ("sets");
613 return qual_unparse (s->squal);
615 return qual_unparse (s->squal);
621 cstring stateClause_unparseKind (stateClause s)
625 cstring_makeLiteralTemp (s->state == TK_BEFORE
627 : (s->state == TK_AFTER
629 stateClauseKind_unparse (s)));
632 cstring stateClause_unparse (stateClause s)
634 return (message ("%q %q",
635 stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
638 stateClause stateClause_createDefines (sRefSet s)
640 return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
643 stateClause stateClause_createUses (sRefSet s)
645 return (stateClause_createRaw (TK_BOTH, SP_USES, s));
648 stateClause stateClause_createSets (sRefSet s)
650 return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
653 stateClause stateClause_createReleases (sRefSet s)
655 return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
658 stateClause stateClause_createPlain (lltok tok, sRefSet s)
660 switch (lltok_getTok (tok))
663 return stateClause_createUses (s);
665 return stateClause_createDefines (s);
667 return stateClause_createAllocates (s);
669 return stateClause_createSets (s);
671 return stateClause_createReleases (s);
677 BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
680 stateClause stateClause_createAllocates (sRefSet s)
682 return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
685 bool stateClause_matchKind (stateClause s1, stateClause s2)
687 return (s1->state == s2->state && s1->kind == s2->kind
688 && qual_match (s1->squal, s2->squal));
691 bool stateClause_hasEnsures (stateClause cl)
693 return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
696 bool stateClause_hasRequires (stateClause cl)
698 return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
701 bool stateClause_setsMetaState (stateClause cl)
703 return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
704 && qual_isMetaState (cl->squal));
707 qual stateClause_getMetaQual (stateClause cl)
709 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
713 static sRefModVal stateClause_getStateFunction (stateClause cl)
717 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
723 if (qual_isNullStateQual (sq))
725 return (sRefModVal) sRef_setNullState;
727 else if (qual_isExQual (sq))
729 return (sRefModVal) sRef_setExKind;
731 else if (qual_isAliasQual (sq))
733 return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
737 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
744 int stateClause_getStateParameter (stateClause cl)
748 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
752 /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
755 if (qual_isNotNull (sq))
759 else if (qual_isIsNull (sq))
763 else if (qual_isNull (sq))
767 else if (qual_isRelNull (sq))
771 else if (qual_isExposed (sq))
775 else if (qual_isObserver (sq))
779 else if (qual_isAliasQual (sq))
781 if (qual_isOnly (sq)) return AK_ONLY;
782 if (qual_isImpOnly (sq)) return AK_IMPONLY;
783 if (qual_isTemp (sq)) return AK_TEMP;
784 if (qual_isOwned (sq)) return AK_OWNED;
785 if (qual_isShared (sq)) return AK_SHARED;
786 if (qual_isUnique (sq)) return AK_UNIQUE;
787 if (qual_isDependent (sq)) return AK_DEPENDENT;
788 if (qual_isKeep (sq)) return AK_KEEP;
789 if (qual_isKept (sq)) return AK_KEPT;
794 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
803 sRefModVal stateClause_getEnsuresFunction (stateClause cl)
805 llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
806 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
807 return stateClause_getStateFunction (cl);
810 sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
812 llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
813 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
814 return stateClause_getStateFunction (cl);
817 /*@observer@*/ fileloc stateClause_loc (stateClause s)