Don't try calling lsl when file is missing.
[splint-patched.git] / src / exprChecks.c
blob769f08d11186ca14d05fefdfc98a0f901b25d2f1
1 /*
2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
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.
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
25 ** exprChecks.c
28 # include "splintMacros.nf"
29 # include "basic.h"
30 # include "transferChecks.h"
31 # include "exprChecks.h"
34 ** for now, allow exprChecks to access exprNode.
35 ** may remove this in future
38 /*@access exprNode@*/
40 static bool checkCallModifyAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
41 static bool checkModifyValAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
42 static bool checkModifyAux (/*@exposed@*/ sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
43 static void checkSafeReturnExpr (/*@notnull@*/ exprNode p_e);
46 ** called at end of expression statement
48 ** of e->kind is not an assign, empty, body or modop
49 ** verify the the value is void
53 static int inCompoundStatementExpression = 0;
55 void
56 exprChecks_inCompoundStatementExpression (void)
58 inCompoundStatementExpression++;
61 void
62 exprChecks_leaveCompoundStatementExpression (void)
64 inCompoundStatementExpression--;
65 llassert (inCompoundStatementExpression >= 0);
68 void
69 exprChecks_checkStatementEffect (exprNode e)
71 bool hasError = FALSE;
73 if (inCompoundStatementExpression > 0)
76 ** Okay to have effectless statments in compound statement expression (should check
77 ** it is the last statement, but we don't for now).
80 return;
83 if (!exprNode_isError (e))
85 exprKind ek = e->kind;
87 if (ek == XPR_CALL && !(ctype_isRealVoid (e->typ)))
89 if (ctype_isKnown (e->typ))
91 if (ctype_isManifestBool (ctype_realishType (e->typ)))
93 hasError = optgenerror
94 (FLG_RETVALBOOL,
95 message ("Return value (type %t) ignored: %s",
96 e->typ,
97 exprNode_unparseFirst (e)),
98 e->loc);
100 else if (ctype_isDirectInt (e->typ))
102 hasError = optgenerror
103 (FLG_RETVALINT,
104 message ("Return value (type %t) ignored: %s",
105 e->typ,
106 exprNode_unparseFirst (e)),
107 e->loc);
109 else
111 hasError = optgenerror
112 (FLG_RETVALOTHER,
113 message ("Return value (type %t) ignored: %s",
114 e->typ,
115 exprNode_unparseFirst (e)),
116 e->loc);
121 if (!hasError && !(exprNode_mayEscape (e))
122 && !(e->canBreak)) /* control changes are effects too! */
124 if (sRefSet_hasRealElement (e->sets)
125 || sRefSet_hasRealElement (e->msets))
127 ; /* okay */
129 else
131 if (sRefSet_isEmpty (e->sets) && sRefSet_isEmpty (e->msets))
133 voptgenerror
134 (FLG_NOEFFECT,
135 message ("Statement has no effect: %s",
136 exprNode_unparseFirst (e)),
137 e->loc);
139 else
141 if (context_maybeSet (FLG_NOEFFECTUNCON))
143 if (sRefSet_hasUnconstrained (e->sets))
145 voptgenerror
146 (FLG_NOEFFECTUNCON,
147 message ("Statement has no effect (possible "
148 "undected modification through "
149 "call to %q): %s",
150 sRefSet_unparseUnconstrained (e->sets),
151 exprNode_unparseFirst (e)),
152 e->loc);
154 else if (sRefSet_hasUnconstrained (e->msets))
156 voptgenerror
157 (FLG_NOEFFECTUNCON,
158 message ("Statement has no effect (possible "
159 "undected modification through "
160 "call to %q): %s",
161 sRefSet_unparseUnconstrained (e->msets),
162 exprNode_unparseFirst (e)),
163 e->loc);
165 else
167 ; /* statement has unknown modification */
176 static bool
177 checkRepExposed (sRef base, /*@notnull@*/ exprNode e, sRef alias,
178 /*@unused@*/ exprNode unused)
180 ctype btype;
182 if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
184 btype = sRef_getType (base);
186 if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
188 voptgenerror (FLG_RETEXPOSE,
189 message ("Return value exposes rep of %s: %s",
190 ctype_unparse (btype),
191 exprNode_unparse (e)),
192 e->loc);
193 return TRUE;
196 else
198 sRef rbase = sRef_getRootBase (base);
199 btype = sRef_getType (rbase);
201 if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
203 voptgenerror
204 (FLG_RETEXPOSE,
205 message ("Return value may expose rep of %s through alias %q: %s",
206 ctype_unparse (btype),
207 sRef_unparse (rbase),
208 exprNode_unparse (e)),
209 e->loc);
210 return TRUE;
214 return FALSE;
217 static bool
218 checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e,
219 sRef alias, /*@unused@*/ exprNode unused)
221 if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
223 ctype ct = e->typ;
225 if (ctype_isUnknown (ct))
227 ct = sRef_getType (base);
230 if (ctype_isVisiblySharable (ct))
232 if (sRef_isFileOrGlobalScope (base))
234 uentry fcn = context_getHeader ();
235 bool noerror = FALSE;
237 if (uentry_isValid (fcn) && uentry_isFunction (fcn))
239 sRef res = uentry_getSref (fcn);
241 /* If result is dependent and global is owned, this is okay... */
242 if (sRef_isDependent (res)
243 && sRef_isOwned (base))
245 noerror = TRUE;
250 if (!noerror)
252 voptgenerror
253 (FLG_RETALIAS,
254 message ("Function returns reference to global %q: %s",
255 sRef_unparse (base),
256 exprNode_unparse (e)),
257 e->loc);
260 return TRUE;
262 else if (sRef_isAnyParam (base))
264 uentryList params = context_getParams ();
265 int paramno = sRef_getParam (base);
267 if (paramno < uentryList_size (params))
269 uentry arg = uentryList_getN (params, paramno);
270 sRef ref = uentry_getSref (arg);
272 if (uentry_isReturned (arg)
273 || sRef_isOnly (ref)
274 || sRef_isExposed (ref)
275 || sRef_isRefCounted (ref))
277 ; /* okay */
279 else
281 voptgenerror
282 (FLG_RETALIAS,
283 message ("Function returns reference to parameter %q: %s",
284 sRef_unparse (base),
285 exprNode_unparse (e)),
286 e->loc);
289 else
291 llbuglit ("ret alias: bad paramno");
294 return TRUE;
296 else
298 return FALSE;
302 else
304 if (ctype_isVisiblySharable (e->typ))
306 if (sRef_isFileOrGlobalScope (base))
308 voptgenerror
309 (FLG_RETALIAS,
310 message ("Function may return reference to global %q through alias %q: %s",
311 sRef_unparse (alias),
312 sRef_unparse (base),
313 exprNode_unparse (e)),
314 e->loc);
315 return TRUE;
317 else if (sRef_isAnyParam (base) && !(sRef_isOnly (base)))
319 uentryList params = context_getParams ();
320 int paramno = sRef_getParam (base);
322 if (paramno < uentryList_size (params))
324 uentry arg = uentryList_getN (params, paramno);
326 if (!uentry_isReturned (arg))
328 voptgenerror
329 (FLG_RETALIAS,
330 message
331 ("Function may return reference to parameter %q through alias %q: %s",
332 sRef_unparse (base),
333 sRef_unparse (alias),
334 exprNode_unparse (e)),
335 e->loc);
337 return TRUE;
340 else
342 voptgenerror
343 (FLG_RETALIAS,
344 message
345 ("Function may return reference to parameter %q through alias %q: %s",
346 sRef_unparse (base),
347 sRef_unparse (alias),
348 exprNode_unparse (e)),
349 e->loc);
351 return TRUE;
354 else
356 return FALSE;
360 return FALSE;
364 void
365 exprNode_checkModify (exprNode e, exprNode err)
367 llassert (exprNode_isDefined (e));
369 DPRINTF (("Check modify: %s", exprNode_unparse (e)));
371 if (sRef_isValid (e->sref))
373 sRef_aliasCheckPred (checkModifyAux, sRef_isReference, e->sref, e, err);
377 void
378 exprNode_checkModifyVal (exprNode e, exprNode err)
380 llassert (exprNode_isDefined (e));
382 DPRINTF (("Check modify val: %s", exprNode_unparse (e)));
384 if (sRef_isValid (e->sref))
386 sRef_aliasCheckPred (checkModifyValAux, sRef_isReference, e->sref, e, err);
390 void
391 exprChecks_checkNullReturn (fileloc loc)
393 if (!context_inRealFunction ())
396 llmsg ("exprChecks_checkNullReturnExpr: not in function context");
398 return;
400 else
402 if (ctype_isFunction (context_currentFunctionType ()))
404 ctype tr = ctype_getReturnType (context_currentFunctionType ());
406 if (!ctype_isFirstVoid (tr))
408 if (ctype_isUnknown (tr))
410 voptgenerror
411 (FLG_EMPTYRETURN,
412 cstring_makeLiteral ("Empty return in function declared to implicitly return int"),
413 loc);
415 else
417 voptgenerror (FLG_EMPTYRETURN,
418 message ("Empty return in function declared to return %t", tr),
419 loc);
426 void
427 exprNode_checkReturn (exprNode e)
429 if (!exprNode_isError (e))
431 if (!context_inRealFunction ())
433 if (context_inMacro ())
435 llerror (FLG_MACRORETURN,
436 message ("Macro %s uses return (not functional)",
437 context_inFunctionName ()));
439 else
442 llbuglit ("exprNode_checkReturn: not in function context");
446 else
448 if (ctype_isFunction (context_currentFunctionType ()))
450 checkSafeReturnExpr (e);
452 else
460 void
461 exprNode_checkPred (cstring c, exprNode e)
463 ctype ct;
465 if (exprNode_isError (e))
466 return;
468 ct = exprNode_getType (e);
470 if (exprNode_isAssign (e))
472 voptgenerror
473 (FLG_PREDASSIGN,
474 message ("Test expression for %s is assignment expression: %s",
475 c, exprNode_unparse (e)),
476 e->loc);
479 if (ctype_isRealBool (ct) || ctype_isUnknown (ct))
480 /* evs 2000-12-20 added || ctype_isUnknown to avoid spurious messages */
484 else if (ctype_isRealPointer (ct))
486 voptgenerror
487 (FLG_PREDBOOLPTR,
488 message ("Test expression for %s not %s, type %t: %s", c,
489 context_printBoolName (),
490 ct, exprNode_unparse (e)),
491 e->loc);
493 else if (ctype_isRealInt (ct))
495 voptgenerror
496 (FLG_PREDBOOLINT,
497 message ("Test expression for %s not %s, type %t: %s", c,
498 context_printBoolName (), ct, exprNode_unparse (e)),
499 e->loc);
501 else
503 voptgenerror
504 (FLG_PREDBOOLOTHERS,
505 message ("Test expression for %s not %s, type %t: %s", c,
506 context_printBoolName (), ct, exprNode_unparse (e)),
507 e->loc);
511 void
512 exprChecks_checkUsedGlobs (globSet decl, globSet used)
514 fileloc fl = uentry_whereSpecified (context_getHeader ());
516 if (fileloc_isUndefined (fl))
518 fl = uentry_whereDeclared (context_getHeader ());
521 globSet_allElements (decl, el)
523 if (!globSet_member (used, el))
525 if (sRef_isSpecInternalState (el)
526 || sRef_isNothing (el))
530 else
532 cstring sname = sRef_unparse (el);
534 if (fileloc_isLib (fl))
536 voptgenerror (FLG_USEALLGLOBS,
537 message ("Global %s listed (%q) but not used",
538 sname, fileloc_unparse (fl)),
539 g_currentloc);
541 else
543 voptgenerror (FLG_USEALLGLOBS,
544 message ("Global %s listed but not used", sname),
545 fl);
548 cstring_free (sname);
551 } end_globSet_allElements;
554 void
555 exprNode_checkAllMods (sRefSet mods, uentry ue)
557 bool realParams = FALSE;
558 uentry le = context_getHeader ();
559 fileloc fl = uentry_whereSpecified (le);
560 uentryList paramNames = context_getParams ();
562 if (uentry_isFunction (le))
564 uentryList specParamNames = uentry_getParams (le);
566 if (uentryList_isUndefined (specParamNames))
568 ; /* unknown params */
570 else if (uentryList_size (paramNames) != uentryList_size (specParamNames))
572 llbug
573 (message ("exprNode_checkAllMods: parameter lists have different sizes: "
574 "%q (%d) / %q (%d)",
575 uentryList_unparse (paramNames),
576 uentryList_size (paramNames),
577 uentryList_unparse (specParamNames),
578 uentryList_size (specParamNames)));
580 else if (uentryList_size (paramNames) > 0
581 && !uentry_hasRealName (uentryList_getN (specParamNames, 0)))
583 /* loaded from a library */
585 else
587 realParams = TRUE;
591 sRefSet_allElements (mods, sr)
593 if (sRef_isNothing (sr) || sRef_isSpecState (sr))
595 ; /* should report on anything? */
597 else if (sRef_isInternalState (sr))
599 if (!sRef_isModified (sr))
601 if (sRefSet_hasStatic (mods))
603 ; /* okay */
605 else
607 if (optgenerror
608 (FLG_MUSTMOD,
609 message
610 ("Function %s specified to modify internal state "
611 "but no internal state is modified",
612 uentry_rawName (ue)),
613 uentry_whereLast (ue)))
615 uentry_showWhereSpecified (le);
620 else
622 if (!sRef_isModified (sr))
624 cstring sname = realParams ? sRef_unparse (sr) : sRef_unparse (sr);
626 if (fileloc_isLib (fl) && !realParams)
628 voptgenerror
629 (FLG_MUSTMOD,
630 message ("Suspect object listed (%q) in modifies "
631 "clause of %s not modified: %s",
632 fileloc_unparse (fl),
633 uentry_rawName (ue),
634 sname),
635 uentry_whereLast (ue));
637 else
639 if (optgenerror
640 (FLG_MUSTMOD,
641 message ("Suspect object listed in modifies of %s "
642 "not modified: %s",
643 uentry_rawName (ue),
644 sname),
645 uentry_whereLast (ue)))
647 uentry_showWhereSpecified (le);
650 cstring_free (sname);
653 } end_sRefSet_allElements;
656 void exprNode_checkMacroBody (/*@only@*/ exprNode e)
658 if (!exprNode_isError (e))
660 uentry hdr;
662 if (!(context_inFunctionLike () || context_inMacroConstant ()
663 || context_inUnknownMacro ()))
665 llcontbug
666 (message
667 ("exprNode_checkMacroBody: not in macro function or constant: %q",
668 context_unparse ()));
669 exprNode_free (e);
670 return;
673 hdr = context_getHeader ();
675 if (e->kind == XPR_STMTLIST || e->kind == XPR_BODY)
677 voptgenerror
678 (FLG_MACROSTMT,
679 message
680 ("Macro %q definition is statement list (recommend "
681 "do { ... } while (0) constuction to ensure multiple "
682 "statement macro is syntactic function)",
683 uentry_getName (hdr)),
684 fileloc_isDefined (e->loc) ? e->loc : g_currentloc);
687 if (context_inMacroConstant ())
689 ctype t = uentry_getType (hdr);
691 uentry_setDefined (hdr, e->loc);
693 if (!(exprNode_matchType (t, e)))
695 cstring uname = uentry_getName (hdr);
697 if (cstring_equal (uname, context_getTrueName ())
698 || cstring_equal (uname, context_getFalseName ()))
701 ** We need to do something special to allow FALSE and TRUE
702 ** to be defined without reporting errors. This is a tad
703 ** bogus, but otherwise lots of things would break.
707 llassert (ctype_isManifestBool (t));
708 /* Should also check type of e is a reasonable (?) bool type. */
710 else
712 if (optgenerror
713 (FLG_INCONDEFS,
714 message
715 ("Constant %q specified as %s, but defined as %s: %s",
716 uentry_getName (hdr),
717 ctype_unparse (t),
718 ctype_unparse (e->typ),
719 exprNode_unparse (e)),
720 e->loc))
722 uentry_showWhereSpecified (hdr);
726 cstring_free (uname);
728 else
730 if (context_maybeSet (FLG_NULLSTATE)
731 && ctype_isUA(t)
732 && ctype_isRealPointer (t)
733 && exprNode_isNullValue (e))
735 uentry ue = usymtab_getTypeEntry (ctype_typeId (t));
736 sRef sr = uentry_getSref (ue);
738 if (!sRef_possiblyNull (sr))
740 vgenhinterror
741 (FLG_NULLSTATE,
742 message ("Constant %q of non-null type %s defined "
743 "as null: %s",
744 uentry_getName (hdr), ctype_unparse (t),
745 exprNode_unparse (e)),
746 message ("If %s can be null, add a /*@null@*/ "
747 "qualifer to its typedef.",
748 ctype_unparse (t)),
749 e->loc);
752 uentry_mergeConstantValue (hdr, e->val);
753 e->val = multiVal_undefined;
757 else if (context_inMacroFunction () || context_inUnknownMacro ())
759 ctype rettype = context_getRetType ();
761 if (context_isMacroMissingParams ())
763 llassert (context_inMacroFunction ());
766 ** # define newname oldname
768 ** newname is a function
769 ** specification of oldname should match
770 ** specification of newname.
773 if (!ctype_isFunction (e->typ))
775 voptgenerror
776 (FLG_INCONDEFS,
777 message ("Function %s defined by unparameterized "
778 "macro not corresponding to function",
779 context_inFunctionName ()),
780 e->loc);
782 else
784 uentry ue = exprNode_getUentry (e);
786 if (uentry_isValid (ue))
789 ** Okay, for now --- should check for consistency
792 ** uentry oldue = usymtab_lookup (cfname);
795 /* check var conformance here! */
797 else
799 voptgenerror
800 (FLG_INCONDEFS,
801 message ("Function %s defined by unparameterized "
802 "macro not corresponding to function",
803 context_inFunctionName ()),
804 e->loc);
807 e->typ = ctype_getReturnType (e->typ);
808 rettype = e->typ; /* avoid aditional errors */
812 if (ctype_isVoid (rettype) || ctype_isUnknown (rettype))
814 ; /* don't complain when void macros have values */
816 else if (!exprNode_matchType (rettype, e))
818 if (optgenerror
819 (FLG_INCONDEFS,
820 message ("Function %q specified to return %s, "
821 "implemented as macro having type %s: %s",
822 uentry_getName (hdr),
823 ctype_unparse (rettype), ctype_unparse (e->typ),
824 exprNode_unparse (e)),
825 e->loc))
827 uentry_showWhereSpecified (hdr);
830 else
832 switch (e->kind)
834 /* these expressions have values: */
835 case XPR_PARENS: case XPR_ASSIGN:
836 case XPR_EMPTY: case XPR_VAR:
837 case XPR_OP: case XPR_POSTOP:
838 case XPR_PREOP: case XPR_CALL:
839 case XPR_SIZEOFT: case XPR_SIZEOF:
840 case XPR_ALIGNOFT: case XPR_ALIGNOF:
841 case XPR_CAST: case XPR_FETCH:
842 case XPR_COMMA: case XPR_COND:
843 case XPR_ARROW: case XPR_CONST:
844 case XPR_STRINGLITERAL: case XPR_NUMLIT:
845 case XPR_FACCESS: case XPR_OFFSETOF:
847 transferChecks_return (e, hdr);
848 break;
850 /* these expressions don't */
851 case XPR_LABEL:
852 case XPR_VAARG: case XPR_ITER:
853 case XPR_FOR: case XPR_FORPRED:
854 case XPR_GOTO: case XPR_CONTINUE:
855 case XPR_BREAK: case XPR_RETURN:
856 case XPR_NULLRETURN: case XPR_IF:
857 case XPR_IFELSE: case XPR_DOWHILE:
858 case XPR_WHILE: case XPR_STMT:
859 case XPR_STMTLIST: case XPR_SWITCH:
860 case XPR_INIT: case XPR_BODY:
861 case XPR_NODE: case XPR_ITERCALL:
862 case XPR_TOK: case XPR_CASE:
863 case XPR_FTCASE: case XPR_FTDEFAULT:
864 case XPR_DEFAULT: case XPR_WHILEPRED:
865 case XPR_BLOCK: case XPR_INITBLOCK:
866 if (optgenerror
867 (FLG_INCONDEFS,
868 message ("Function %q specified to return %s, "
869 "implemented as macro with no result: %s",
870 uentry_getName (hdr),
871 ctype_unparse (rettype),
872 exprNode_unparse (e)),
873 e->loc))
875 uentry_showWhereSpecified (hdr);
880 usymtab_checkFinalScope (FALSE);
882 else
884 llbug (message ("exprNode_checkMacroBody: not in macro function: %q", context_unparse ()));
887 exprNode_free (e);
890 context_exitFunction ();
891 return;
894 void exprNode_checkFunctionBody (exprNode body)
896 if (!exprNode_isError (body))
898 bool noret = context_getFlag (FLG_NORETURN);
899 bool checkret = exprNode_mustEscape (body);
901 if (!checkret
902 && noret
903 && !exprNode_errorEscape (body)
904 && context_inRealFunction ()
905 && ctype_isFunction (context_currentFunctionType ()))
907 ctype tr = ctype_getReturnType (context_currentFunctionType ());
909 if (!ctype_isFirstVoid (tr))
911 if (ctype_isUnknown (tr))
913 voptgenerror
914 (FLG_NORETURN,
915 cstring_makeLiteral ("Path with no return in function declared to implicity return int"),
916 g_currentloc);
918 else
920 voptgenerror
921 (FLG_NORETURN,
922 message ("Path with no return in function declared to return %t",
923 tr),
924 g_currentloc);
929 if (!checkret)
931 context_returnFunction ();
935 /*drl modified */
938 void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
940 constraintList c, t, post;
941 constraintList c2, fix;
942 context_enterInnerContext ();
944 llassert (exprNode_isDefined (body));
946 DPRINTF (("Checking body: %s", exprNode_unparse (body)));
949 if we're not going to be printing any errors for buffer overflows
950 we can skip the checking to improve performance
952 FLG_DEBUGFUNCTIONCONSTRAINT controls wheather we perform the check anyway
953 in order to find potential problems like assert failures and seg faults...
956 if (!(context_getFlag (FLG_DEBUGFUNCTIONCONSTRAINT)
957 || context_getFlag (FLG_BOUNDSWRITE)
958 || context_getFlag (FLG_BOUNDSREAD)
959 || context_getFlag (FLG_LIKELYBOUNDSWRITE)
960 || context_getFlag (FLG_LIKELYBOUNDSREAD)
961 || context_getFlag (FLG_CHECKPOST)
962 || context_getFlag (FLG_ALLOCMISMATCH)))
964 exprNode_free (body);
965 context_exitInnerPlain();
966 return;
969 exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
970 dependent... fix it! */
972 c = uentry_getFcnPreconditions (ue);
974 if (constraintList_isDefined (c))
976 DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
978 body->requiresConstraints =
979 constraintList_reflectChangesFreePre (body->requiresConstraints, c);
981 c2 = constraintList_copy (c);
982 fix = constraintList_makeFixedArrayConstraints (body->uses);
983 c2 = constraintList_reflectChangesFreePre (c2, fix);
985 constraintList_free (fix);
987 if (context_getFlag (FLG_ORCONSTRAINT))
989 t = constraintList_reflectChangesOr (body->requiresConstraints, c2 );
991 else
993 t = constraintList_reflectChanges(body->requiresConstraints, c2);
996 constraintList_free (body->requiresConstraints);
997 DPRINTF ((message ("The body has the required constraints: %s", constraintList_unparseDetailed (t) ) ) );
999 body->requiresConstraints = t;
1001 t = constraintList_mergeEnsures (c, body->ensuresConstraints);
1002 constraintList_free(body->ensuresConstraints);
1004 body->ensuresConstraints = t;
1006 DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_unparseDetailed (t) ) ) );
1007 constraintList_free(c2);
1010 if (constraintList_isDefined(c))
1012 DPRINTF ((message ("The Function %s has the preconditions %s",
1013 uentry_unparse(ue), constraintList_unparseDetailed(c))));
1015 else
1017 DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue))));
1020 if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
1022 constraintList implicitFcnConstraints = context_getImplicitFcnConstraints (ue);
1024 if (constraintList_isDefined (implicitFcnConstraints))
1026 DPRINTF (("Implicit constraints: %s", constraintList_unparse (implicitFcnConstraints)));
1028 body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints,
1029 implicitFcnConstraints);
1030 constraintList_free (implicitFcnConstraints);
1032 else
1034 DPRINTF (("No implicit constraints"));
1038 body->requiresConstraints = constraintList_sort (body->requiresConstraints);
1040 constraintList_printError(body->requiresConstraints, g_currentloc);
1042 post = uentry_getFcnPostconditions (ue);
1044 if (context_getFlag (FLG_CHECKPOST))
1046 if (constraintList_isDefined (post))
1048 constraintList post2;
1050 DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n",
1051 constraintList_unparseDetailed (post) ) ) );
1053 post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
1055 post2 = constraintList_copy (post);
1056 fix = constraintList_makeFixedArrayConstraints (body->uses);
1057 post2 = constraintList_reflectChangesFreePre (post2, fix);
1058 constraintList_free(fix);
1059 if ( context_getFlag (FLG_ORCONSTRAINT) )
1061 t = constraintList_reflectChangesOr (post2, body->ensuresConstraints);
1063 else
1065 t = constraintList_reflectChanges(post2, body->ensuresConstraints);
1068 constraintList_free(post2);
1069 constraintList_free(post);
1070 post = t;
1072 printf("Unresolved post conditions\n");
1073 constraintList_printErrorPostConditions(post, g_currentloc);
1077 if (constraintList_isDefined (post))
1079 constraintList_free (post);
1082 body->ensuresConstraints = constraintList_sort(body->ensuresConstraints);
1084 if ( context_getFlag (FLG_FUNCTIONPOST) )
1086 constraintList_printError(body->ensuresConstraints, g_currentloc);
1089 /* ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
1091 ConPrint (message ("Splint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
1093 printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
1094 printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
1097 if (constraintList_isDefined (c))
1098 constraintList_free(c);
1100 context_exitInnerPlain();
1102 /* is it okay not to free this? */
1103 DPRINTF (("Done checking constraints..."));
1104 exprNode_free (body);
1107 void exprChecks_checkEmptyMacroBody (void)
1109 uentry hdr;
1111 if (!(context_inFunctionLike () || context_inMacroConstant ()
1112 || context_inUnknownMacro ()))
1114 llcontbug
1115 (message ("exprNode_checkEmptyMacroBody: not in macro function or constant: %q",
1116 context_unparse ()));
1117 return;
1120 hdr = context_getHeader ();
1122 beginLine ();
1124 if (uentry_isFunction (hdr))
1126 voptgenerror
1127 (FLG_MACROEMPTY,
1128 message
1129 ("Macro definition for %q is empty", uentry_getName (hdr)),
1130 g_currentloc);
1132 usymtab_checkFinalScope (FALSE);
1135 context_exitFunction ();
1136 return;
1139 void exprNode_checkIterBody (/*@only@*/ exprNode body)
1141 context_exitAllClauses ();
1143 context_exitFunction ();
1144 exprNode_free (body);
1147 void exprNode_checkIterEnd (/*@only@*/ exprNode body)
1149 context_exitAllClauses ();
1150 context_exitFunction ();
1151 exprNode_free (body);
1154 static
1155 bool checkModifyAuxAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
1157 bool hasMods = context_hasMods ();
1158 flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
1160 if (exprNode_isDefined (f))
1162 f->sets = sRefSet_insert (f->sets, s);
1165 if (context_getFlag (FLG_MODIFIES)
1166 && (hasMods || context_getFlag (FLG_MODNOMODS)))
1168 sRefSet mods = context_modList ();
1170 if (!sRef_canModify (s, mods))
1172 sRef rb = sRef_getRootBase (s);
1175 if (sRef_isFileOrGlobalScope (rb))
1177 if (!context_checkGlobMod (rb))
1179 return FALSE;
1183 if (sRef_isInvalid (alias) || sRef_sameName (s, alias))
1185 if (sRef_isLocalVar (sRef_getRootBase (s)))
1187 voptgenerror
1188 (errCode,
1189 message
1190 ("Undocumented modification of internal state (%q): %s",
1191 sRef_unparse (s), exprNode_unparse (err)),
1192 exprNode_isDefined (f) ? f->loc : g_currentloc);
1194 else
1196 if (sRef_isSystemState (s))
1198 if (errCode == FLG_MODNOMODS)
1200 if (context_getFlag (FLG_MODNOMODS))
1202 errCode = FLG_MODFILESYSTEM;
1205 else
1207 errCode = FLG_MODFILESYSTEM;
1211 voptgenerror
1212 (errCode,
1213 message ("Undocumented modification of %q: %s",
1214 sRef_unparse (s), exprNode_unparse (err)),
1215 exprNode_isDefined (f) ? f->loc : g_currentloc);
1218 return TRUE;
1220 else
1222 if (sRef_isReference (s) && !sRef_isAddress (alias))
1224 voptgenerror
1225 (errCode,
1226 message
1227 ("Possible undocumented modification of %q through alias %q: %s",
1228 sRef_unparse (s),
1229 sRef_unparse (alias),
1230 exprNode_unparse (err)),
1231 exprNode_isDefined (f) ? f->loc : g_currentloc);
1232 return TRUE;
1237 else
1239 if (context_maybeSet (FLG_MUSTMOD))
1241 (void) sRef_canModify (s, context_modList ());
1244 if (sRef_isRefsField (s))
1246 sRef_setModified (s);
1250 return FALSE;
1253 static
1254 bool checkModifyAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
1256 DPRINTF (("Check modify aux: %s", sRef_unparseFull (s)));
1258 if (sRef_isReference (s) && sRef_isObserver (s)
1259 && context_maybeSet (FLG_MODOBSERVER))
1261 cstring sname;
1263 if (sRef_isPointer (s))
1265 sRef base = sRef_getBase (s);
1266 sname = sRef_unparse (base);
1268 else
1270 if (sRef_isAddress (s))
1272 sRef p = sRef_constructPointer (s);
1273 sname = sRef_unparse (p);
1275 else
1277 sname = sRef_unparse (s);
1281 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1283 if (sRef_isMeaningful (s))
1285 if (optgenerror
1286 (FLG_MODOBSERVER,
1287 message ("Suspect modification of observer %s: %s",
1288 sname, exprNode_unparse (err)),
1289 exprNode_isDefined (f) ? f->loc : g_currentloc))
1291 sRef_showExpInfo (s);
1294 else
1296 voptgenerror
1297 (FLG_MODOBSERVER,
1298 message ("Suspect modification of observer returned by "
1299 "function call: %s",
1300 exprNode_unparse (err)),
1301 exprNode_isDefined (f) ? f->loc : g_currentloc);
1304 else
1306 if (optgenerror
1307 (FLG_MODOBSERVER,
1308 message ("Suspect modification of observer %s through alias %q: %s",
1309 sname, sRef_unparse (alias), exprNode_unparse (err)),
1310 exprNode_isDefined (f) ? f->loc : g_currentloc))
1312 sRef_showExpInfo (s);
1316 cstring_free (sname);
1319 (void) checkModifyAuxAux (s, f, alias, err);
1320 return FALSE;
1323 static
1324 bool checkModifyValAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
1326 (void) checkModifyAuxAux (s, f, alias, err);
1327 return FALSE;
1330 static
1331 bool checkCallModifyAux (/*@exposed@*/ sRef s, exprNode f, sRef alias, exprNode err)
1333 bool result = FALSE;
1335 DPRINTF (("Check modify aux: %s / %s",
1336 sRef_unparse (s), sRef_unparse (alias)));
1338 if (sRef_isObserver (s) && context_maybeSet (FLG_MODOBSERVER))
1340 sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
1341 cstring sname = sRef_unparse (p);
1343 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1345 if (sRef_isMeaningful (s))
1347 result = optgenerror
1348 (FLG_MODOBSERVER,
1349 message ("Suspect modification of observer %s: %s",
1350 sname, exprNode_unparse (err)),
1351 exprNode_isDefined (f) ? f->loc : g_currentloc);
1353 else
1355 result = optgenerror
1356 (FLG_MODOBSERVER,
1357 message ("Suspect modification of observer returned by "
1358 "function call: %s",
1359 exprNode_unparse (err)),
1360 exprNode_isDefined (f) ? f->loc : g_currentloc);
1363 else
1365 result = optgenerror
1366 (FLG_MODOBSERVER,
1367 message
1368 ("Suspect modification of observer %s through alias %q: %s",
1369 sname, sRef_unparse (alias), exprNode_unparse (err)),
1370 exprNode_isDefined (f) ? f->loc : g_currentloc);
1373 cstring_free (sname);
1375 else if (context_maybeSet (FLG_MODIFIES))
1377 DPRINTF (("can modify: %s / %s",
1378 sRef_unparse (s),
1379 sRefSet_unparse (context_modList ())));
1381 if (!(sRef_canModifyVal (s, context_modList ())))
1383 sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
1384 cstring sname = sRef_unparse (p);
1385 bool hasMods = context_hasMods ();
1386 sRef rb = sRef_getRootBase (s);
1387 flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
1388 bool check = TRUE;
1390 DPRINTF (("Can't modify! %s", sRef_unparse (s)));
1392 if (sRef_isFileOrGlobalScope (rb))
1394 uentry ue = sRef_getUentry (rb);
1396 /* be more specific here! */
1397 if (!uentry_isCheckedModify (ue))
1399 check = FALSE;
1403 if (check)
1405 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1407 if (sRef_isLocalVar (sRef_getRootBase (s)))
1409 voptgenerror
1410 (errCode,
1411 message
1412 ("Undocumented modification of internal "
1413 "state (%q) through call to %s: %s",
1414 sRef_unparse (s), exprNode_unparse (f),
1415 exprNode_unparse (err)),
1416 exprNode_isDefined (f) ? f->loc : g_currentloc);
1418 else
1420 if (sRef_isSystemState (s))
1422 if (errCode == FLG_MODNOMODS)
1424 if (context_getFlag (FLG_MODNOMODS))
1426 errCode = FLG_MODFILESYSTEM;
1429 else
1431 errCode = FLG_MODFILESYSTEM;
1435 result = optgenerror
1436 (errCode,
1437 message ("Undocumented modification of %s "
1438 "possible from call to %s: %s",
1439 sname,
1440 exprNode_unparse (f),
1441 exprNode_unparse (err)),
1442 exprNode_isDefined (f) ? f->loc : g_currentloc);
1445 else
1447 result = optgenerror
1448 (errCode,
1449 message ("Undocumented modification of %s possible "
1450 "from call to %s (through alias %q): %s",
1451 sname,
1452 exprNode_unparse (f),
1453 sRef_unparse (alias),
1454 exprNode_unparse (err)),
1455 exprNode_isDefined (f) ? f->loc : g_currentloc);
1458 cstring_free (sname);
1461 else
1463 if (context_maybeSet (FLG_MUSTMOD))
1465 (void) sRef_canModifyVal (s, context_modList ());
1469 return result;
1472 void exprNode_checkCallModifyVal (sRef s, exprNodeList args, exprNode f, exprNode err)
1474 s = sRef_fixBaseParam (s, args);
1475 DPRINTF (("Check call modify: %s", sRef_unparse (s)));
1476 sRef_aliasCheckPred (checkCallModifyAux, NULL, s, f, err);
1479 void
1480 exprChecks_checkExport (uentry e)
1482 if (context_checkExport (e))
1484 fileloc fl = uentry_whereDeclared (e);
1486 if (fileloc_isHeader (fl) && !fileloc_isLib (fl)
1487 && !fileloc_isImport (fl) && !uentry_isStatic (e))
1489 if (uentry_isFunction (e) ||
1490 (uentry_isVariable (e) && ctype_isFunction (uentry_getType (e))))
1492 voptgenerror
1493 (FLG_EXPORTFCN,
1494 message ("Function exported, but not specified: %q",
1495 uentry_getName (e)),
1496 fl);
1498 else if (uentry_isExpandedMacro (e))
1500 voptgenerror
1501 (FLG_EXPORTMACRO,
1502 message ("Expanded macro exported, but not specified: %q",
1503 uentry_getName (e)),
1504 fl);
1506 else if (uentry_isVariable (e) && !uentry_isParam (e))
1508 voptgenerror
1509 (FLG_EXPORTVAR,
1510 message ("Variable exported, but not specified: %q",
1511 uentry_getName (e)),
1512 fl);
1514 else if (uentry_isEitherConstant (e))
1516 voptgenerror
1517 (FLG_EXPORTCONST,
1518 message ("Constant exported, but not specified: %q",
1519 uentry_getName (e)),
1520 fl);
1522 else if (uentry_isIter (e) || uentry_isEndIter (e))
1524 voptgenerror
1525 (FLG_EXPORTITER,
1526 message ("Iterator exported, but not specified: %q",
1527 uentry_getName (e)),
1528 fl);
1531 else if (uentry_isDatatype (e))
1533 ; /* error already reported */
1535 else
1537 BADEXIT;
1543 static void checkSafeReturnExpr (/*@notnull@*/ exprNode e)
1545 ctype tr = ctype_getReturnType (context_currentFunctionType ());
1546 ctype te = exprNode_getType (e);
1548 /* evans 2001-08-21: added test to warn about void returns from void functions */
1549 if (ctype_isVoid (tr))
1551 (void) gentypeerror
1552 (te, e, tr, exprNode_undefined,
1553 message ("Return expression from function declared void: %s", exprNode_unparse (e)),
1554 e->loc);
1555 return;
1558 if (!ctype_forceMatch (tr, te) && !exprNode_matchLiteral (tr, e))
1560 (void) gentypeerror
1561 (te, e, tr, exprNode_undefined,
1562 message ("Return value type %t does not match declared type %t: %s",
1563 te, tr, exprNode_unparse (e)),
1564 e->loc);
1566 else
1568 sRef ret = e->sref;
1569 uentry rval = context_getHeader ();
1570 sRef resultref = uentry_getSref (rval);
1572 DPRINTF (("Check return: %s / %s / %s",
1573 exprNode_unparse (e),
1574 sRef_unparseFull (e->sref),
1575 uentry_unparse (rval)));
1577 transferChecks_return (e, rval);
1579 DPRINTF (("After return: %s / %s / %s",
1580 exprNode_unparse (e),
1581 sRef_unparseFull (e->sref),
1582 uentry_unparse (rval)));
1584 if (!(sRef_isExposed (uentry_getSref (context_getHeader ()))
1585 || sRef_isObserver (uentry_getSref (context_getHeader ())))
1586 && (context_getFlag (FLG_RETALIAS)
1587 || context_getFlag (FLG_RETEXPOSE)))
1589 sRef base = sRef_getRootBase (ret);
1590 ctype rtype = e->typ;
1592 if (ctype_isUnknown (rtype))
1594 rtype = tr;
1597 if (ctype_isVisiblySharable (rtype))
1599 if (context_getFlag (FLG_RETALIAS))
1601 sRef_aliasCheckPred (checkRefGlobParam, NULL, base,
1602 e, exprNode_undefined);
1605 if (context_getFlag (FLG_RETEXPOSE) && sRef_isIReference (ret)
1606 && !sRef_isExposed (resultref) && !sRef_isObserver (resultref))
1608 sRef_aliasCheckPred (checkRepExposed, NULL, base, e,
1609 exprNode_undefined);