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 "transferChecks.h"
31 # include "exprChecks.h"
34 ** for now, allow exprChecks to access exprNode.
35 ** may remove this in future
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;
56 exprChecks_inCompoundStatementExpression (void)
58 inCompoundStatementExpression
++;
62 exprChecks_leaveCompoundStatementExpression (void)
64 inCompoundStatementExpression
--;
65 llassert (inCompoundStatementExpression
>= 0);
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).
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
95 message ("Return value (type %t) ignored: %s",
97 exprNode_unparseFirst (e
)),
100 else if (ctype_isDirectInt (e
->typ
))
102 hasError
= optgenerror
104 message ("Return value (type %t) ignored: %s",
106 exprNode_unparseFirst (e
)),
111 hasError
= optgenerror
113 message ("Return value (type %t) ignored: %s",
115 exprNode_unparseFirst (e
)),
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
))
131 if (sRefSet_isEmpty (e
->sets
) && sRefSet_isEmpty (e
->msets
))
135 message ("Statement has no effect: %s",
136 exprNode_unparseFirst (e
)),
141 if (context_maybeSet (FLG_NOEFFECTUNCON
))
143 if (sRefSet_hasUnconstrained (e
->sets
))
147 message ("Statement has no effect (possible "
148 "undected modification through "
150 sRefSet_unparseUnconstrained (e
->sets
),
151 exprNode_unparseFirst (e
)),
154 else if (sRefSet_hasUnconstrained (e
->msets
))
158 message ("Statement has no effect (possible "
159 "undected modification through "
161 sRefSet_unparseUnconstrained (e
->msets
),
162 exprNode_unparseFirst (e
)),
167 ; /* statement has unknown modification */
177 checkRepExposed (sRef base
, /*@notnull@*/ exprNode e
, sRef alias
,
178 /*@unused@*/ exprNode unused
)
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
)),
198 sRef rbase
= sRef_getRootBase (base
);
199 btype
= sRef_getType (rbase
);
201 if (ctype_isAbstract (btype
) && ctype_isVisiblySharable (e
->typ
))
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
)),
218 checkRefGlobParam (sRef base
, /*@notnull@*/ exprNode e
,
219 sRef alias
, /*@unused@*/ exprNode unused
)
221 if (sRef_isInvalid (alias
) || sRef_sameName (base
, alias
))
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
))
254 message ("Function returns reference to global %q: %s",
256 exprNode_unparse (e
)),
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
)
274 || sRef_isExposed (ref
)
275 || sRef_isRefCounted (ref
))
283 message ("Function returns reference to parameter %q: %s",
285 exprNode_unparse (e
)),
291 llbuglit ("ret alias: bad paramno");
304 if (ctype_isVisiblySharable (e
->typ
))
306 if (sRef_isFileOrGlobalScope (base
))
310 message ("Function may return reference to global %q through alias %q: %s",
311 sRef_unparse (alias
),
313 exprNode_unparse (e
)),
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
))
331 ("Function may return reference to parameter %q through alias %q: %s",
333 sRef_unparse (alias
),
334 exprNode_unparse (e
)),
345 ("Function may return reference to parameter %q through alias %q: %s",
347 sRef_unparse (alias
),
348 exprNode_unparse (e
)),
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
);
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
);
391 exprChecks_checkNullReturn (fileloc loc
)
393 if (!context_inRealFunction ())
396 llmsg ("exprChecks_checkNullReturnExpr: not in function context");
402 if (ctype_isFunction (context_currentFunctionType ()))
404 ctype tr
= ctype_getReturnType (context_currentFunctionType ());
406 if (!ctype_isFirstVoid (tr
))
408 if (ctype_isUnknown (tr
))
412 cstring_makeLiteral ("Empty return in function declared to implicitly return int"),
417 voptgenerror (FLG_EMPTYRETURN
,
418 message ("Empty return in function declared to return %t", tr
),
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 ()));
442 llbuglit ("exprNode_checkReturn: not in function context");
448 if (ctype_isFunction (context_currentFunctionType ()))
450 checkSafeReturnExpr (e
);
461 exprNode_checkPred (cstring c
, exprNode e
)
465 if (exprNode_isError (e
))
468 ct
= exprNode_getType (e
);
470 if (exprNode_isAssign (e
))
474 message ("Test expression for %s is assignment expression: %s",
475 c
, exprNode_unparse (e
)),
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
))
488 message ("Test expression for %s not %s, type %t: %s", c
,
489 context_printBoolName (),
490 ct
, exprNode_unparse (e
)),
493 else if (ctype_isRealInt (ct
))
497 message ("Test expression for %s not %s, type %t: %s", c
,
498 context_printBoolName (), ct
, exprNode_unparse (e
)),
505 message ("Test expression for %s not %s, type %t: %s", c
,
506 context_printBoolName (), ct
, exprNode_unparse (e
)),
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
))
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
)),
543 voptgenerror (FLG_USEALLGLOBS
,
544 message ("Global %s listed but not used", sname
),
548 cstring_free (sname
);
551 } end_globSet_allElements
;
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
))
573 (message ("exprNode_checkAllMods: parameter lists have different sizes: "
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 */
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
))
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
);
622 if (!sRef_isModified (sr
))
624 cstring sname
= realParams
? sRef_unparse (sr
) : sRef_unparse (sr
);
626 if (fileloc_isLib (fl
) && !realParams
)
630 message ("Suspect object listed (%q) in modifies "
631 "clause of %s not modified: %s",
632 fileloc_unparse (fl
),
635 uentry_whereLast (ue
));
641 message ("Suspect object listed in modifies of %s "
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
))
662 if (!(context_inFunctionLike () || context_inMacroConstant ()
663 || context_inUnknownMacro ()))
667 ("exprNode_checkMacroBody: not in macro function or constant: %q",
668 context_unparse ()));
673 hdr
= context_getHeader ();
675 if (e
->kind
== XPR_STMTLIST
|| e
->kind
== XPR_BODY
)
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. */
715 ("Constant %q specified as %s, but defined as %s: %s",
716 uentry_getName (hdr
),
718 ctype_unparse (e
->typ
),
719 exprNode_unparse (e
)),
722 uentry_showWhereSpecified (hdr
);
726 cstring_free (uname
);
730 if (context_maybeSet (FLG_NULLSTATE
)
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
))
742 message ("Constant %q of non-null type %s defined "
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.",
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
))
777 message ("Function %s defined by unparameterized "
778 "macro not corresponding to function",
779 context_inFunctionName ()),
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! */
801 message ("Function %s defined by unparameterized "
802 "macro not corresponding to function",
803 context_inFunctionName ()),
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
))
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
)),
827 uentry_showWhereSpecified (hdr
);
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
);
850 /* these expressions don't */
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
:
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
)),
875 uentry_showWhereSpecified (hdr
);
880 usymtab_checkFinalScope (FALSE
);
884 llbug (message ("exprNode_checkMacroBody: not in macro function: %q", context_unparse ()));
890 context_exitFunction ();
894 void exprNode_checkFunctionBody (exprNode body
)
896 if (!exprNode_isError (body
))
898 bool noret
= context_getFlag (FLG_NORETURN
);
899 bool checkret
= exprNode_mustEscape (body
);
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
))
915 cstring_makeLiteral ("Path with no return in function declared to implicity return int"),
922 message ("Path with no return in function declared to return %t",
931 context_returnFunction ();
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();
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
);
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
))));
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
);
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
);
1065 t
= constraintList_reflectChanges(post2
, body
->ensuresConstraints
);
1068 constraintList_free(post2
);
1069 constraintList_free(post
);
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)
1111 if (!(context_inFunctionLike () || context_inMacroConstant ()
1112 || context_inUnknownMacro ()))
1115 (message ("exprNode_checkEmptyMacroBody: not in macro function or constant: %q",
1116 context_unparse ()));
1120 hdr
= context_getHeader ();
1124 if (uentry_isFunction (hdr
))
1129 ("Macro definition for %q is empty", uentry_getName (hdr
)),
1132 usymtab_checkFinalScope (FALSE
);
1135 context_exitFunction ();
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
);
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
))
1183 if (sRef_isInvalid (alias
) || sRef_sameName (s
, alias
))
1185 if (sRef_isLocalVar (sRef_getRootBase (s
)))
1190 ("Undocumented modification of internal state (%q): %s",
1191 sRef_unparse (s
), exprNode_unparse (err
)),
1192 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1196 if (sRef_isSystemState (s
))
1198 if (errCode
== FLG_MODNOMODS
)
1200 if (context_getFlag (FLG_MODNOMODS
))
1202 errCode
= FLG_MODFILESYSTEM
;
1207 errCode
= FLG_MODFILESYSTEM
;
1213 message ("Undocumented modification of %q: %s",
1214 sRef_unparse (s
), exprNode_unparse (err
)),
1215 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1222 if (sRef_isReference (s
) && !sRef_isAddress (alias
))
1227 ("Possible undocumented modification of %q through alias %q: %s",
1229 sRef_unparse (alias
),
1230 exprNode_unparse (err
)),
1231 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1239 if (context_maybeSet (FLG_MUSTMOD
))
1241 (void) sRef_canModify (s
, context_modList ());
1244 if (sRef_isRefsField (s
))
1246 sRef_setModified (s
);
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
))
1263 if (sRef_isPointer (s
))
1265 sRef base
= sRef_getBase (s
);
1266 sname
= sRef_unparse (base
);
1270 if (sRef_isAddress (s
))
1272 sRef p
= sRef_constructPointer (s
);
1273 sname
= sRef_unparse (p
);
1277 sname
= sRef_unparse (s
);
1281 if (!sRef_isValid (alias
) || sRef_sameName (s
, alias
))
1283 if (sRef_isMeaningful (s
))
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
);
1298 message ("Suspect modification of observer returned by "
1299 "function call: %s",
1300 exprNode_unparse (err
)),
1301 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
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
);
1324 bool checkModifyValAux (/*@exposed@*/ sRef s
, exprNode f
, sRef alias
, exprNode err
)
1326 (void) checkModifyAuxAux (s
, f
, alias
, err
);
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
1349 message ("Suspect modification of observer %s: %s",
1350 sname
, exprNode_unparse (err
)),
1351 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1355 result
= optgenerror
1357 message ("Suspect modification of observer returned by "
1358 "function call: %s",
1359 exprNode_unparse (err
)),
1360 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1365 result
= optgenerror
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",
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
;
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
))
1405 if (!sRef_isValid (alias
) || sRef_sameName (s
, alias
))
1407 if (sRef_isLocalVar (sRef_getRootBase (s
)))
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
);
1420 if (sRef_isSystemState (s
))
1422 if (errCode
== FLG_MODNOMODS
)
1424 if (context_getFlag (FLG_MODNOMODS
))
1426 errCode
= FLG_MODFILESYSTEM
;
1431 errCode
= FLG_MODFILESYSTEM
;
1435 result
= optgenerror
1437 message ("Undocumented modification of %s "
1438 "possible from call to %s: %s",
1440 exprNode_unparse (f
),
1441 exprNode_unparse (err
)),
1442 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1447 result
= optgenerror
1449 message ("Undocumented modification of %s possible "
1450 "from call to %s (through alias %q): %s",
1452 exprNode_unparse (f
),
1453 sRef_unparse (alias
),
1454 exprNode_unparse (err
)),
1455 exprNode_isDefined (f
) ? f
->loc
: g_currentloc
);
1458 cstring_free (sname
);
1463 if (context_maybeSet (FLG_MUSTMOD
))
1465 (void) sRef_canModifyVal (s
, context_modList ());
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
);
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
))))
1494 message ("Function exported, but not specified: %q",
1495 uentry_getName (e
)),
1498 else if (uentry_isExpandedMacro (e
))
1502 message ("Expanded macro exported, but not specified: %q",
1503 uentry_getName (e
)),
1506 else if (uentry_isVariable (e
) && !uentry_isParam (e
))
1510 message ("Variable exported, but not specified: %q",
1511 uentry_getName (e
)),
1514 else if (uentry_isEitherConstant (e
))
1518 message ("Constant exported, but not specified: %q",
1519 uentry_getName (e
)),
1522 else if (uentry_isIter (e
) || uentry_isEndIter (e
))
1526 message ("Iterator exported, but not specified: %q",
1527 uentry_getName (e
)),
1531 else if (uentry_isDatatype (e
))
1533 ; /* error already reported */
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
))
1552 (te
, e
, tr
, exprNode_undefined
,
1553 message ("Return expression from function declared void: %s", exprNode_unparse (e
)),
1558 if (!ctype_forceMatch (tr
, te
) && !exprNode_matchLiteral (tr
, e
))
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
)),
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
))
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
);