2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 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;
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_isQual (stateClause cl)
103 return (cl->kind == SP_QUAL);
106 bool stateClause_isMemoryAllocation (stateClause cl)
120 return (qual_isMemoryAllocation (cl->squal)
121 || qual_isSharing (cl->squal));
128 ** An error is reported if the test is NOT true.
132 /* Microsoft doesn't believe in higher order functions... */
\r
133 # pragma warning( disable : 4550 )
\r
136 sRefTest stateClause_getPreTestFunction (stateClause cl)
141 return sRef_isStrictReadable;
143 return sRef_hasNoStorage;
145 return sRef_hasNoStorage;
147 return sRef_isNotUndefined;
149 return sRef_isNotUndefined;
154 if (qual_isOnly (cl->squal)) {
156 } else if (qual_isShared (cl->squal)) {
157 return sRef_isShared;
158 } else if (qual_isDependent (cl->squal)) {
159 return sRef_isDependent;
160 } else if (qual_isOwned (cl->squal)) {
162 } else if (qual_isObserver (cl->squal)) {
163 return sRef_isObserver;
164 } else if (qual_isExposed (cl->squal)) {
165 return sRef_isExposed;
166 } else if (qual_isNotNull (cl->squal)) {
167 return sRef_isNotNull;
168 } else if (qual_isIsNull (cl->squal)) {
169 return sRef_isDefinitelyNull;
179 sRefTest stateClause_getPostTestFunction (stateClause cl)
181 llassert (stateClause_isAfter (cl));
188 return sRef_isAllocated;
190 return sRef_isReallyDefined;
192 return sRef_isReallyDefined;
194 return sRef_isDeadStorage;
198 if (qual_isOnly (cl->squal)) {
200 } else if (qual_isShared (cl->squal)) {
201 return sRef_isShared;
202 } else if (qual_isDependent (cl->squal)) {
203 return sRef_isDependent;
204 } else if (qual_isOwned (cl->squal)) {
206 } else if (qual_isObserver (cl->squal)) {
207 return sRef_isObserver;
208 } else if (qual_isExposed (cl->squal)) {
209 return sRef_isExposed;
210 } else if (qual_isNotNull (cl->squal)) {
211 return sRef_isNotNull;
212 } else if (qual_isIsNull (cl->squal)) {
213 return sRef_isDefinitelyNull;
222 sRefShower stateClause_getPostTestShower (stateClause cl)
231 return sRef_showNotReallyDefined;
237 if (qual_isMemoryAllocation (cl->squal)) {
238 return sRef_showAliasInfo;
239 } else if (qual_isSharing (cl->squal)) {
240 return sRef_showExpInfo;
241 } else if (qual_isIsNull (cl->squal) || qual_isNotNull (cl->squal)) {
242 return sRef_showNullInfo;
251 sRefMod stateClause_getEntryFunction (stateClause cl)
253 if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
258 return sRef_setDefinedComplete;
260 return sRef_setUndefined; /* evans 2002-01-01 */
262 return sRef_setUndefined; /* evans 2002-01-01 */
264 return sRef_setAllocatedComplete;
266 return sRef_setDefinedComplete;
270 if (qual_isOnly (cl->squal)) {
272 } else if (qual_isShared (cl->squal)) {
273 return sRef_setShared;
274 } else if (qual_isDependent (cl->squal)) {
275 return sRef_setDependent;
276 } else if (qual_isOwned (cl->squal)) {
277 return sRef_setOwned;
278 } else if (qual_isObserver (cl->squal)) {
279 return sRef_setObserver;
280 } else if (qual_isExposed (cl->squal)) {
281 return sRef_setExposed;
282 } else if (qual_isNotNull (cl->squal)) {
283 return sRef_setNotNull;
284 } else if (qual_isIsNull (cl->squal)) {
285 return sRef_setDefNull;
287 DPRINTF (("Here we are: %s",
288 qual_unparse (cl->squal)));
303 sRefMod stateClause_getEffectFunction (stateClause cl)
305 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
312 return sRef_setAllocatedComplete;
314 return sRef_setDefinedNCComplete;
316 return sRef_setDefinedNCComplete;
318 return sRef_killComplete;
322 if (qual_isOnly (cl->squal)) {
324 } else if (qual_isShared (cl->squal)) {
325 return sRef_setShared;
326 } else if (qual_isDependent (cl->squal)) {
327 return sRef_setDependent;
328 } else if (qual_isOwned (cl->squal)) {
329 return sRef_setOwned;
330 } else if (qual_isObserver (cl->squal)) {
331 return sRef_setObserver;
332 } else if (qual_isExposed (cl->squal)) {
333 return sRef_setExposed;
334 } else if (qual_isNotNull (cl->squal)) {
335 return sRef_setNotNull;
336 } else if (qual_isIsNull (cl->squal)) {
337 return sRef_setDefNull;
353 sRefMod stateClause_getReturnEffectFunction (stateClause cl)
355 if (cl->state == TK_AFTER || cl->state == TK_BOTH)
368 if (qual_isOnly (cl->squal)) {
369 return sRef_killComplete;
385 static flagcode stateClause_qualErrorCode (stateClause cl)
387 if (qual_isOnly (cl->squal)) {
388 return FLG_ONLYTRANS;
389 } else if (qual_isShared (cl->squal)) {
390 return FLG_SHAREDTRANS;
391 } else if (qual_isDependent (cl->squal)) {
392 return FLG_DEPENDENTTRANS;
393 } else if (qual_isOwned (cl->squal)) {
394 return FLG_OWNEDTRANS;
395 } else if (qual_isObserver (cl->squal)) {
396 return FLG_OBSERVERTRANS;
397 } else if (qual_isExposed (cl->squal)) {
398 return FLG_EXPOSETRANS;
399 } else if (qual_isIsNull (cl->squal)
400 || qual_isNotNull (cl->squal)) {
401 return FLG_NULLSTATE;
406 BADBRANCHRET (INVALID_FLAG);
409 flagcode stateClause_preErrorCode (stateClause cl)
411 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
417 case SP_ALLOCATES: /*@fallthrough@*/
420 return FLG_MUSTFREEONLY;
425 return stateClause_qualErrorCode (cl);
428 BADBRANCHRET (INVALID_FLAG);
431 static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
433 if (qual_isMemoryAllocation (cl->squal)) {
434 return alkind_capName (sRef_getAliasKind (sr));
435 } else if (qual_isObserver (cl->squal)) {
436 return cstring_makeLiteralTemp ("Non-observer");
437 } else if (qual_isExposed (cl->squal)) {
438 if (sRef_isObserver (sr))
440 return cstring_makeLiteralTemp ("Observer");
444 return cstring_makeLiteralTemp ("Non-exposed");
446 } else if (qual_isNotNull (cl->squal)) {
447 if (sRef_isDefinitelyNull (sr))
449 return cstring_makeLiteralTemp ("Null");
453 return cstring_makeLiteralTemp ("Possibly null");
455 } else if (qual_isIsNull (cl->squal)) {
456 return cstring_makeLiteralTemp ("Non-null");
461 BADBRANCHRET (cstring_undefined);
464 cstring stateClause_preErrorString (stateClause cl, sRef sr)
466 llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
471 if (sRef_isDead (sr))
472 return cstring_makeLiteralTemp ("Dead");
474 return cstring_makeLiteralTemp ("Undefined");
475 case SP_ALLOCATES: /*@fallthrough@*/
478 return cstring_makeLiteralTemp ("Allocated");
480 if (sRef_isDead (sr))
482 return cstring_makeLiteralTemp ("Dead");
484 else if (sRef_isDependent (sr)
485 || sRef_isShared (sr))
487 return alkind_unparse (sRef_getAliasKind (sr));
489 else if (sRef_isObserver (sr) || sRef_isExposed (sr))
491 return exkind_unparse (sRef_getExKind (sr));
495 return cstring_makeLiteralTemp ("Undefined");
500 return stateClause_qualErrorString (cl, sr);
506 flagcode stateClause_postErrorCode (stateClause cl)
508 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
520 return FLG_MUSTFREEONLY;
524 return stateClause_qualErrorCode (cl);
527 BADBRANCHRET (INVALID_FLAG);
530 cstring stateClause_postErrorString (stateClause cl, sRef sr)
532 llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
538 return cstring_makeLiteralTemp ("<ERROR>");
540 return cstring_makeLiteralTemp ("Unallocated");
543 return cstring_makeLiteralTemp ("Undefined");
545 return cstring_makeLiteralTemp ("Unreleased");
549 return stateClause_qualErrorString (cl, sr);
555 cstring stateClause_dump (stateClause s)
557 return (message ("%d.%d.%q.%q",
560 qual_dump (s->squal),
561 sRefSet_dump (s->refs)));
564 stateClause stateClause_undump (char **s)
566 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
568 ret->loc = fileloc_undefined;
569 ret->state = (stateConstraint) reader_getInt (s);
570 reader_checkChar (s, '.');
571 ret->kind = (stateClauseKind) reader_getInt (s);
572 reader_checkChar (s, '.');
573 ret->squal = qual_undump (s);
574 reader_checkChar (s, '.');
575 ret->refs = sRefSet_undump (s);
580 stateClause stateClause_copy (stateClause s)
582 stateClause ret = (stateClause) dmalloc (sizeof (*ret));
584 ret->state = s->state;
586 ret->squal = s->squal;
587 ret->refs = sRefSet_newCopy (s->refs);
588 ret->loc = fileloc_copy (s->loc);
593 bool stateClause_sameKind (stateClause s1, stateClause s2)
595 return (s1->state == s2->state
596 && s1->kind == s2->kind
597 && qual_match (s1->squal, s2->squal));
600 void stateClause_free (stateClause s)
602 sRefSet_free (s->refs);
603 fileloc_free (s->loc);
607 static /*@observer@*/ cstring
608 stateClauseKind_unparse (stateClause s)
613 return cstring_makeLiteralTemp ("uses");
615 return cstring_makeLiteralTemp ("defines");
617 return cstring_makeLiteralTemp ("allocates");
619 return cstring_makeLiteralTemp ("releases");
621 return cstring_makeLiteralTemp ("sets");
623 return qual_unparse (s->squal);
625 return qual_unparse (s->squal);
631 cstring stateClause_unparseKind (stateClause s)
635 cstring_makeLiteralTemp (s->state == TK_BEFORE
637 : (s->state == TK_AFTER
639 stateClauseKind_unparse (s)));
642 cstring stateClause_unparse (stateClause s)
644 return (message ("%q %q",
645 stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
648 stateClause stateClause_createDefines (sRefSet s)
650 return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
653 stateClause stateClause_createUses (sRefSet s)
655 return (stateClause_createRaw (TK_BOTH, SP_USES, s));
658 stateClause stateClause_createSets (sRefSet s)
660 return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
663 stateClause stateClause_createReleases (sRefSet s)
665 return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
668 stateClause stateClause_createPlain (lltok tok, sRefSet s)
670 switch (lltok_getTok (tok))
673 return stateClause_createUses (s);
675 return stateClause_createDefines (s);
677 return stateClause_createAllocates (s);
679 return stateClause_createSets (s);
681 return stateClause_createReleases (s);
687 BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
690 stateClause stateClause_createAllocates (sRefSet s)
692 return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
695 bool stateClause_matchKind (stateClause s1, stateClause s2)
697 return (s1->state == s2->state && s1->kind == s2->kind
698 && qual_match (s1->squal, s2->squal));
701 bool stateClause_hasEnsures (stateClause cl)
703 return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
706 bool stateClause_hasRequires (stateClause cl)
708 return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
711 bool stateClause_setsMetaState (stateClause cl)
713 return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
714 && qual_isMetaState (cl->squal));
717 qual stateClause_getMetaQual (stateClause cl)
719 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
723 static sRefModVal stateClause_getStateFunction (stateClause cl)
727 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
733 if (qual_isNullStateQual (sq))
735 return (sRefModVal) sRef_setNullState;
737 else if (qual_isExQual (sq))
739 return (sRefModVal) sRef_setExKind;
741 else if (qual_isAliasQual (sq))
743 return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
747 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
754 int stateClause_getStateParameter (stateClause cl)
758 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
762 /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
765 if (qual_isNotNull (sq))
769 else if (qual_isIsNull (sq))
773 else if (qual_isNull (sq))
777 else if (qual_isRelNull (sq))
781 else if (qual_isExposed (sq))
785 else if (qual_isObserver (sq))
789 else if (qual_isAliasQual (sq))
791 if (qual_isOnly (sq)) return AK_ONLY;
792 if (qual_isImpOnly (sq)) return AK_IMPONLY;
793 if (qual_isTemp (sq)) return AK_TEMP;
794 if (qual_isOwned (sq)) return AK_OWNED;
795 if (qual_isShared (sq)) return AK_SHARED;
796 if (qual_isUnique (sq)) return AK_UNIQUE;
797 if (qual_isDependent (sq)) return AK_DEPENDENT;
798 if (qual_isKeep (sq)) return AK_KEEP;
799 if (qual_isKept (sq)) return AK_KEPT;
804 DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
813 sRefModVal stateClause_getEnsuresFunction (stateClause cl)
815 llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
816 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
817 return stateClause_getStateFunction (cl);
820 sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
822 llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
823 llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
824 return stateClause_getStateFunction (cl);
827 /*@observer@*/ fileloc stateClause_loc (stateClause s)