]> andersk Git - splint.git/blame - src/exprChecks.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Added check of user specified post conditions.
[splint.git] / src / exprChecks.c
CommitLineData
616915dd 1/*
2** LCLint - annotation-assisted static program checker
3** Copyright (C) 1994-2000 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.
19**
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://lclint.cs.virginia.edu
23*/
24/*
25** exprChecks.c
26*/
27
28# include "lclintMacros.nf"
29# include "basic.h"
30# include "cgrammar.h"
31# include "cgrammar_tokens.h"
32# include "aliasChecks.h"
33# include "exprChecks.h"
34
35/*
36** for now, allow exprChecks to access exprNode.
37** may remove this in future
38*/
39
40/*@access exprNode@*/
41
42static bool checkCallModifyAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
43static bool checkModifyValAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
44static bool checkModifyAux (sRef p_s, exprNode p_f, sRef p_alias, exprNode p_err);
45static void checkSafeReturnExpr (/*@notnull@*/ exprNode p_e);
46
47/*
48** called at end of expression statement
49**
50** of e->kind is not an assign, empty, body or modop
51** verify the the value is void
52**
53*/
54
55void
56exprNode_checkStatement (exprNode e)
57{
58 bool hasError = FALSE;
59
60 if (!exprNode_isError (e))
61 {
62 exprKind ek = e->kind;
63
64 if (ek == XPR_CALL && !(ctype_isRealVoid (e->typ)))
65 {
66 if (ctype_isKnown (e->typ))
67 {
68 if (ctype_isManifestBool (ctype_realishType (e->typ)))
69 {
70 hasError = optgenerror
71 (FLG_RETVALBOOL,
72 message ("Return value (type %t) ignored: %s",
73 e->typ,
74 exprNode_unparseFirst (e)),
75 e->loc);
76 }
77 else if (ctype_isDirectInt (e->typ))
78 {
79 hasError = optgenerror
80 (FLG_RETVALINT,
81 message ("Return value (type %t) ignored: %s",
82 e->typ,
83 exprNode_unparseFirst (e)),
84 e->loc);
85 }
86 else
87 {
88 hasError = optgenerror
89 (FLG_RETVALOTHER,
90 message ("Return value (type %t) ignored: %s",
91 e->typ,
92 exprNode_unparseFirst (e)),
93 e->loc);
94 }
95 }
96 }
97
98 if (!hasError && !(exprNode_mayEscape (e))
99 && !(e->canBreak)) /* control changes are effects too! */
100 {
101 if (sRefSet_hasRealElement (e->sets)
102 || sRefSet_hasRealElement (e->msets))
103 {
104 ; /* okay */
105 }
106 else
107 {
108 if (sRefSet_isEmpty (e->sets) && sRefSet_isEmpty (e->msets))
109 {
110 voptgenerror
111 (FLG_NOEFFECT,
112 message ("Statement has no effect: %s",
113 exprNode_unparseFirst (e)),
114 e->loc);
115 }
116 else
117 {
118 if (context_maybeSet (FLG_NOEFFECTUNCON))
119 {
120 if (sRefSet_hasUnconstrained (e->sets))
121 {
122 voptgenerror
123 (FLG_NOEFFECTUNCON,
124 message ("Statement has no effect (possible "
125 "undected modification through "
126 "call to %q): %s",
127 sRefSet_unparseUnconstrained (e->sets),
128 exprNode_unparseFirst (e)),
129 e->loc);
130 }
131 else if (sRefSet_hasUnconstrained (e->msets))
132 {
133 voptgenerror
134 (FLG_NOEFFECTUNCON,
135 message ("Statement has no effect (possible "
136 "undected modification through "
137 "call to %q): %s",
138 sRefSet_unparseUnconstrained (e->msets),
139 exprNode_unparseFirst (e)),
140 e->loc);
141 }
142 else
143 {
144 ; /* statement has unknown modification */
145 }
146 }
147 }
148 }
149 }
150 }
151}
152
153static bool
154checkRepExposed (sRef base, /*@notnull@*/ exprNode e, sRef alias,
155 /*@unused@*/ exprNode unused)
156{
157 ctype btype;
158
159 if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
160 {
161 btype = sRef_getType (base);
162
163 if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
164 {
165 voptgenerror (FLG_RETEXPOSE,
166 message ("Return value exposes rep of %s: %s",
167 ctype_unparse (btype),
168 exprNode_unparse (e)),
169 e->loc);
170 return TRUE;
171 }
172 }
173 else
174 {
175 sRef rbase = sRef_getRootBase (base);
176 btype = sRef_getType (rbase);
177
178 if (ctype_isAbstract (btype) && ctype_isVisiblySharable (e->typ))
179 {
180 voptgenerror
181 (FLG_RETEXPOSE,
182 message ("Return value may expose rep of %s through alias %q: %s",
183 ctype_unparse (btype),
184 sRef_unparse (rbase),
185 exprNode_unparse (e)),
186 e->loc);
187 return TRUE;
188 }
189 }
190
191 return FALSE;
192}
193
194static bool
195checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e,
196 sRef alias, /*@unused@*/ exprNode unused)
197{
198 if (sRef_isInvalid (alias) || sRef_sameName (base, alias))
199 {
200 ctype ct = e->typ;
201
202 if (ctype_isUnknown (ct))
203 {
204 ct = sRef_getType (base);
205 }
206
207 if (ctype_isVisiblySharable (ct))
208 {
209 if (sRef_isGlobal (base))
210 {
211 voptgenerror
212 (FLG_RETALIAS,
213 message ("Function returns reference to global %q: %s",
214 sRef_unparse (base),
215 exprNode_unparse (e)),
216 e->loc);
217
218 return TRUE;
219 }
220 else if (sRef_isAnyParam (base))
221 {
222 uentryList params = context_getParams ();
223 int paramno = sRef_getParam (base);
224
225 if (paramno < uentryList_size (params))
226 {
227 uentry arg = uentryList_getN (params, paramno);
228 sRef ref = uentry_getSref (arg);
229
230 if (uentry_isReturned (arg)
231 || sRef_isOnly (ref)
232 || sRef_isExposed (ref)
233 || sRef_isRefCounted (ref))
234 {
235 ; /* okay */
236 }
237 else
238 {
239 voptgenerror
240 (FLG_RETALIAS,
241 message ("Function returns reference to parameter %q: %s",
242 sRef_unparse (base),
243 exprNode_unparse (e)),
244 e->loc);
245 }
246 }
247 else
248 {
249 llbuglit ("ret alias: bad paramno");
250 }
251
252 return TRUE;
253 }
254 else
255 {
256 return FALSE;
257 }
258 }
259 }
260 else
261 {
262 if (ctype_isVisiblySharable (e->typ))
263 {
264 if (sRef_isGlobal (base))
265 {
266 voptgenerror
267 (FLG_RETALIAS,
268 message ("Function may return reference to global %q through alias %q: %s",
269 sRef_unparse (alias),
270 sRef_unparse (base),
271 exprNode_unparse (e)),
272 e->loc);
273 return TRUE;
274 }
275 else if (sRef_isAnyParam (base) && !(sRef_isOnly (base)))
276 {
277 uentryList params = context_getParams ();
278 int paramno = sRef_getParam (base);
279
280 if (paramno < uentryList_size (params))
281 {
282 uentry arg = uentryList_getN (params, paramno);
283
284 if (!uentry_isReturned (arg))
285 {
286 voptgenerror
287 (FLG_RETALIAS,
288 message
289 ("Function may return reference to parameter %q through alias %q: %s",
290 sRef_unparse (base),
291 sRef_unparse (alias),
292 exprNode_unparse (e)),
293 e->loc);
294
295 return TRUE;
296 }
297 }
298 else
299 {
300 voptgenerror
301 (FLG_RETALIAS,
302 message
303 ("Function may return reference to parameter %q through alias %q: %s",
304 sRef_unparse (base),
305 sRef_unparse (alias),
306 exprNode_unparse (e)),
307 e->loc);
308
309 return TRUE;
310 }
311 }
312 else
313 {
314 return FALSE;
315 }
316 }
317 }
318 return FALSE;
319}
320
321
322void
323exprNode_checkModify (exprNode e, exprNode err)
324{
325 llassert (exprNode_isDefined (e));
326
327 DPRINTF (("Check modify: %s", exprNode_unparse (e)));
328
329 if (sRef_isValid (e->sref))
330 {
331 sRef_aliasCheckPred (checkModifyAux, sRef_isReference, e->sref, e, err);
332 }
333}
334
335void
336exprNode_checkModifyVal (exprNode e, exprNode err)
337{
338 llassert (exprNode_isDefined (e));
339
340 DPRINTF (("Check modify val: %s", exprNode_unparse (e)));
341
342 if (sRef_isValid (e->sref))
343 {
344 sRef_aliasCheckPred (checkModifyValAux, sRef_isReference, e->sref, e, err);
345 }
346}
347
348void
349exprChecks_checkNullReturn (fileloc loc)
350{
351 if (!context_inRealFunction ())
352 {
353 /*
354 llmsg ("exprChecks_checkNullReturnExpr: not in function context");
355 */
356 return;
357 }
358 else
359 {
360 if (ctype_isFunction (context_currentFunctionType ()))
361 {
362 ctype tr = ctype_returnValue (context_currentFunctionType ());
363
364 if (!ctype_isFirstVoid (tr))
365 {
366 if (ctype_isUnknown (tr))
367 {
368 voptgenerror
369 (FLG_CONTROL,
370 cstring_makeLiteral ("Empty return in function declared to implicitly return int"),
371 loc);
372 }
373 else
374 {
375 voptgenerror (FLG_CONTROL,
376 message ("Empty return in function declared to return %t", tr),
377 loc);
378 }
379 }
380 }
381 }
382}
383
384void
385exprNode_checkReturn (exprNode e)
386{
387 if (!exprNode_isError (e))
388 {
389 if (!context_inRealFunction ())
390 {
391 if (context_inMacro ())
392 {
393 llerror (FLG_CONTROL,
394 message ("Macro %s uses return (not functional)",
395 context_inFunctionName ()));
396 }
397 else
398 {
399 /*
400 llbuglit ("exprNode_checkReturn: not in function context");
401 */
402 }
403 }
404 else
405 {
406 if (ctype_isFunction (context_currentFunctionType ()))
407 {
408 checkSafeReturnExpr (e);
409 }
410 else
411 {
412 ;
413 }
414 }
415 }
416}
417
418void
419exprNode_checkPred (cstring c, exprNode e)
420{
421 ctype ct;
422
423 if (exprNode_isError (e))
424 return;
425
426 ct = exprNode_getType (e);
427
428 if (exprNode_isAssign (e))
429 {
430 voptgenerror
431 (FLG_PREDASSIGN,
432 message ("Test expression for %s is assignment expression: %s",
433 c, exprNode_unparse (e)),
434 e->loc);
435 }
436
437 if (ctype_isRealBool (ct))
438 {
439 ;
440 }
441 else if (ctype_isRealPointer (ct))
442 {
443 voptgenerror
444 (FLG_PREDBOOLPTR,
445 message ("Test expression for %s not %s, type %t: %s", c,
446 context_printBoolName (),
447 ct, exprNode_unparse (e)),
448 e->loc);
449 }
450 else if (ctype_isRealInt (ct))
451 {
452 voptgenerror
453 (FLG_PREDBOOLINT,
454 message ("Test expression for %s not %s, type %t: %s", c,
455 context_printBoolName (), ct, exprNode_unparse (e)),
456 e->loc);
457 }
458 else
459 {
460 voptgenerror
461 (FLG_PREDBOOLOTHERS,
462 message ("Test expression for %s not %s, type %t: %s", c,
463 context_printBoolName (), ct, exprNode_unparse (e)),
464 e->loc);
465 }
466}
467
468void
469exprChecks_checkUsedGlobs (globSet decl, globSet used)
470{
471 fileloc fl = uentry_whereSpecified (context_getHeader ());
472
473 if (fileloc_isUndefined (fl))
474 {
475 fl = uentry_whereDeclared (context_getHeader ());
476 }
477
478 globSet_allElements (decl, el)
479 {
480 if (!globSet_member (used, el))
481 {
482 if (sRef_isSpecInternalState (el)
483 || sRef_isNothing (el))
484 {
485 ;
486 }
487 else
488 {
489 cstring sname = sRef_unparse (el);
490
491 if (fileloc_isLib (fl))
492 {
493 voptgenerror (FLG_USEALLGLOBS,
494 message ("Global %s listed (%q) but not used",
495 sname, fileloc_unparse (fl)),
496 g_currentloc);
497 }
498 else
499 {
500 voptgenerror (FLG_USEALLGLOBS,
501 message ("Global %s listed but not used", sname),
502 fl);
503 }
504
505 cstring_free (sname);
506 }
507 }
508 } end_globSet_allElements;
509}
510
511void
512exprNode_checkAllMods (sRefSet mods, uentry ue)
513{
514 bool realParams = FALSE;
515 uentry le = context_getHeader ();
516 fileloc fl = uentry_whereSpecified (le);
517 uentryList specParamNames = uentryList_undefined;
518 uentryList paramNames = context_getParams ();
519
520 if (uentry_isFunction (le))
521 {
522 specParamNames = uentry_getParams (le);
523
524 if (uentryList_isUndefined (specParamNames))
525 {
526 ; /* unknown params */
527 }
528 else if (uentryList_size (paramNames) != uentryList_size (specParamNames))
529 {
530 llbug
531 (message ("exprNode_checkAllMods: parameter lists have different sizes: "
532 "%q (%d) / %q (%d)",
533 uentryList_unparse (paramNames),
534 uentryList_size (paramNames),
535 uentryList_unparse (specParamNames),
536 uentryList_size (specParamNames)));
537 }
538 else if (uentryList_size (paramNames) > 0
539 && !uentry_hasRealName (uentryList_getN (specParamNames, 0)))
540 {
541 /* loaded from a library */
542 }
543 else
544 {
545 realParams = TRUE;
546 }
547 }
548
549 sRefSet_allElements (mods, sr)
550 {
551 if (sRef_isNothing (sr) || sRef_isSpecState (sr))
552 {
553 ; /* should report on anything? */
554 }
555 else if (sRef_isInternalState (sr))
556 {
557 if (!sRef_isModified (sr))
558 {
559 if (sRefSet_hasStatic (mods))
560 {
561 ; /* okay */
562 }
563 else
564 {
565 if (optgenerror
566 (FLG_MUSTMOD,
567 message
568 ("Function %s specified to modify internal state "
569 "but no internal state is modified",
570 uentry_rawName (ue)),
571 uentry_whereLast (ue)))
572 {
573 uentry_showWhereSpecified (le);
574 }
575 }
576 }
577 }
578 else
579 {
580 if (!sRef_isModified (sr))
581 {
582 cstring sname = realParams ? sRef_unparse (sr) : sRef_unparse (sr);
583
584 if (fileloc_isLib (fl) && !realParams)
585 {
586 voptgenerror
587 (FLG_MUSTMOD,
588 message ("Suspect object listed (%q) in modifies "
589 "clause of %s not modified: %s",
590 fileloc_unparse (fl),
591 uentry_rawName (ue),
592 sname),
593 uentry_whereLast (ue));
594 }
595 else
596 {
597 if (optgenerror
598 (FLG_MUSTMOD,
599 message ("Suspect object listed in modifies of %s "
600 "not modified: %s",
601 uentry_rawName (ue),
602 sname),
603 uentry_whereLast (ue)))
604 {
605 uentry_showWhereSpecified (le);
606 }
607 }
608 cstring_free (sname);
609 }
610 }
611 } end_sRefSet_allElements;
612}
613
614void exprNode_checkMacroBody (/*@only@*/ exprNode e)
615{
616 if (!exprNode_isError (e))
617 {
618 uentry hdr;
619
620 if (!(context_inFunctionLike () || context_inMacroConstant ()
621 || context_inMacroUnknown ()))
622 {
623 llcontbug
624 (message
625 ("exprNode_checkMacroBody: not in macro function or constant: %q",
626 context_unparse ()));
627 exprNode_free (e);
628 return;
629 }
630
631 hdr = context_getHeader ();
632
633 if (e->kind == XPR_STMTLIST || e->kind == XPR_BODY)
634 {
635 voptgenerror
636 (FLG_MACROSTMT,
637 message
638 ("Macro %q definition is statement list (recommend "
639 "do { ... } while (0) constuction to ensure multiple "
640 "statement macro is syntactic function)",
641 uentry_getName (hdr)),
642 fileloc_isDefined (e->loc) ? e->loc : g_currentloc);
643 }
644
645 if (context_inMacroConstant ())
646 {
647 ctype t = uentry_getType (hdr);
648
649 uentry_setDefined (hdr, e->loc);
650
651 if (!(exprNode_matchType (t, e)))
652 {
653 cstring uname = uentry_getName (hdr);
654
655 if (cstring_equal (uname, context_getTrueName ())
656 || cstring_equal (uname, context_getFalseName ()))
657 {
658 /*
659 ** We need to do something special to allow FALSE and TRUE
660 ** to be defined without reporting errors. This is a tad
661 ** bogus, but otherwise lots of things would break.
662 */
663
664
665 llassert (ctype_isManifestBool (t));
666 /* Should also check type of e is a reasonable (?) bool type. */
667 }
668 else
669 {
670 if (optgenerror
671 (FLG_INCONDEFS,
672 message
673 ("Constant %q specified as %s, but defined as %s: %s",
674 uentry_getName (hdr),
675 ctype_unparse (t),
676 ctype_unparse (e->typ),
677 exprNode_unparse (e)),
678 e->loc))
679 {
680 uentry_showWhereSpecified (hdr);
681 }
682 }
683
684 cstring_free (uname);
685 }
686 else
687 {
688 if (context_maybeSet (FLG_NULLSTATE)
689 && ctype_isUA(t)
690 && ctype_isRealPointer (t)
691 && exprNode_isNullValue (e))
692 {
693 uentry ue = usymtab_getTypeEntry (ctype_typeId (t));
694 sRef sr = uentry_getSref (ue);
695
696 if (!sRef_possiblyNull (sr))
697 {
698 vgenhinterror
699 (FLG_NULLSTATE,
700 message ("Constant %q of non-null type %s defined "
701 "as null: %s",
702 uentry_getName (hdr), ctype_unparse (t),
703 exprNode_unparse (e)),
704 message ("If %s can be null, add a /*@null@*/ "
705 "qualifer to its typedef.",
706 ctype_unparse (t)),
707 e->loc);
708 }
709
710 uentry_mergeConstantValue (hdr, e->val);
711 e->val = multiVal_undefined;
712 }
713 }
714 }
715 else if (context_inMacroFunction () || context_inMacroUnknown ())
716 {
717 ctype rettype = context_getRetType ();
718
719 if (context_isMacroMissingParams ())
720 {
721 llassert (context_inMacroFunction ());
722
723 /*
724 ** # define newname oldname
725 **
726 ** newname is a function
727 ** specification of oldname should match
728 ** specification of newname.
729 */
730
731 if (!ctype_isFunction (e->typ))
732 {
733 voptgenerror
734 (FLG_INCONDEFS,
735 message ("Function %s defined by unparameterized "
736 "macro not corresponding to function",
737 context_inFunctionName ()),
738 e->loc);
739 }
740 else
741 {
742 uentry ue = exprNode_getUentry (e);
743
744 if (uentry_isValid (ue))
745 {
746 /*
747 ** Okay, for now --- should check for consistency
748 */
749 /*
750 ** uentry oldue = usymtab_lookup (cfname);
751 */
752
753 /* check var conformance here! */
754 }
755 else
756 {
757 voptgenerror
758 (FLG_INCONDEFS,
759 message ("Function %s defined by unparameterized "
760 "macro not corresponding to function",
761 context_inFunctionName ()),
762 e->loc);
763 }
764
765 e->typ = ctype_returnValue (e->typ);
766 rettype = e->typ; /* avoid aditional errors */
767 }
768 }
769
770 if (ctype_isVoid (rettype) || ctype_isUnknown (rettype))
771 {
772 ; /* don't complain when void macros have values */
773 }
774 else if (!exprNode_matchType (rettype, e))
775 {
776 if (optgenerror
777 (FLG_INCONDEFS,
778 message ("Function %q specified to return %s, "
779 "implemented as macro having type %s: %s",
780 uentry_getName (hdr),
781 ctype_unparse (rettype), ctype_unparse (e->typ),
782 exprNode_unparse (e)),
783 e->loc))
784 {
785 uentry_showWhereSpecified (hdr);
786 }
787 }
788 else
789 {
790 switch (e->kind)
791 {
792 /* these expressions have values: */
793 case XPR_PARENS: case XPR_ASSIGN:
794 case XPR_EMPTY: case XPR_VAR:
795 case XPR_OP: case XPR_POSTOP:
796 case XPR_PREOP: case XPR_CALL:
797 case XPR_SIZEOFT: case XPR_SIZEOF:
798 case XPR_ALIGNOFT: case XPR_ALIGNOF:
799 case XPR_CAST: case XPR_FETCH:
800 case XPR_COMMA: case XPR_COND:
801 case XPR_ARROW: case XPR_CONST:
802 case XPR_STRINGLITERAL: case XPR_NUMLIT:
803 case XPR_FACCESS: case XPR_OFFSETOF:
804
805 checkReturnTransfer (e, hdr);
806 break;
807
808 /* these expressions don't */
809 case XPR_LABEL:
810 case XPR_VAARG: case XPR_ITER:
811 case XPR_FOR: case XPR_FORPRED:
812 case XPR_GOTO: case XPR_CONTINUE:
813 case XPR_BREAK: case XPR_RETURN:
814 case XPR_NULLRETURN: case XPR_IF:
815 case XPR_IFELSE: case XPR_DOWHILE:
816 case XPR_WHILE: case XPR_STMT:
817 case XPR_STMTLIST: case XPR_SWITCH:
818 case XPR_INIT: case XPR_BODY:
819 case XPR_NODE: case XPR_ITERCALL:
820 case XPR_TOK: case XPR_CASE:
821 case XPR_FTCASE: case XPR_FTDEFAULT:
822 case XPR_DEFAULT: case XPR_WHILEPRED:
823 case XPR_BLOCK: case XPR_INITBLOCK:
824 if (optgenerror
825 (FLG_INCONDEFS,
826 message ("Function %q specified to return %s, "
827 "implemented as macro with no result: %s",
828 uentry_getName (hdr),
829 ctype_unparse (rettype),
830 exprNode_unparse (e)),
831 e->loc))
832 {
833 uentry_showWhereSpecified (hdr);
834 }
835 }
836 }
837
838 usymtab_checkFinalScope (FALSE);
839 }
840 else
841 {
842 llbug (message ("exprNode_checkMacroBody: not in macro function: %q", context_unparse ()));
843 }
844
845 exprNode_free (e);
846 }
847
848 context_exitFunction ();
849 return;
850}
851
852void exprNode_checkFunctionBody (exprNode body)
853{
854 if (!exprNode_isError (body))
855 {
856 bool noret = context_getFlag (FLG_NORETURN);
857 bool checkret = exprNode_mustEscape (body);
858
859 if (!checkret
860 && noret
861 && !exprNode_errorEscape (body)
862 && context_inRealFunction ()
863 && ctype_isFunction (context_currentFunctionType ()))
864 {
865 ctype tr = ctype_returnValue (context_currentFunctionType ());
866
867 if (!ctype_isFirstVoid (tr))
868 {
869 if (ctype_isUnknown (tr))
870 {
871 voptgenerror
872 (FLG_NORETURN,
873 cstring_makeLiteral ("Path with no return in function declared to implicity return int"),
874 g_currentloc);
875 }
876 else
877 {
878 voptgenerror
879 (FLG_NORETURN,
880 message ("Path with no return in function declared to return %t",
881 tr),
882 g_currentloc);
883 }
884 }
885 }
886
4ab867d6 887 /*@i44*/ /* drl added call*/
888 // exprNode_checkFunction (context_getHeader (), body);
616915dd 889
890 if (!checkret)
891 {
892 context_returnFunction ();
893 }
894 }
895}
896/*drl modified */
897
470b7798 898extern constraintList implicitFcnConstraints;
899
bb25bea6 900void exprNode_checkFunction (/*@unused@*/ uentry ue, exprNode body)
616915dd 901{
8f299805 902 constraintList c, t, post;
9280addf 903 constraintList c2, fix;
616915dd 904
9280addf 905 // return;
90bc41f7 906
907 // context_setFlag(FLG_ORCONSTRAINT, TRUE);
bb25bea6 908 context_enterInnerContext ();
909
616915dd 910 exprNode_generateConstraints (body);
911
912 c = uentry_getFcnPreconditions (ue);
913 DPRINTF(("function constraints\n"));
914 DPRINTF (("\n\n\n\n\n\n\n"));
915
616915dd 916
917 if (c)
918 {
84c9ffbf 919
616915dd 920 DPRINTF ( (message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
921
bb25bea6 922 body->requiresConstraints = reflectChangesFreePre (body->requiresConstraints, c);
923
9280addf 924 c2 = constraintList_copy (c);
925 fix = constraintList_makeFixedArrayConstraints (body->uses);
bb25bea6 926 c2 = reflectChangesFreePre (c2, fix);
927 constraintList_free(fix);
90bc41f7 928 if ( context_getFlag (FLG_ORCONSTRAINT) )
929 {
bb25bea6 930 t = reflectChangesOr (body->requiresConstraints, c2 );
90bc41f7 931 }
932 else
933 {
bb25bea6 934 t = reflectChanges (body->requiresConstraints, c2);
90bc41f7 935 }
bb25bea6 936
937 constraintList_free(body->requiresConstraints);
470b7798 938 DPRINTF ( (message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
616915dd 939
bb25bea6 940 body->requiresConstraints = t;
941
942 t = constraintList_mergeEnsures (c, body->ensuresConstraints);
943 constraintList_free(body->ensuresConstraints);
944
945 body->ensuresConstraints = t;
946
947 DPRINTF ( (message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
948 constraintList_free(c2);
616915dd 949 }
bb25bea6 950
616915dd 951 if (c)
952 {
953 DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
954 }
955 else
956 {
957 DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
958 }
959
470b7798 960 if ( implicitFcnConstraints)
961 {
962 if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
963 {
bb25bea6 964 body->requiresConstraints = reflectChangesFreePre (body->requiresConstraints, implicitFcnConstraints );
470b7798 965 }
966 }
967
616915dd 968 constraintList_printError(body->requiresConstraints, g_currentloc);
8f299805 969
970
971 post = uentry_getFcnPostconditions (ue);
972
973 if ( context_getFlag (FLG_CHECKPOST) )
974 {
975 if (post)
976 {
977
978 constraintList post2;
979
980 DPRINTF ( (message ("The declared function postconditions are %s \n\n\n\n\n", constraintList_printDetailed (post) ) ) );
981
982 post = reflectChangesFreePre (post, body->ensuresConstraints);
983
984 post2 = constraintList_copy (post);
985 fix = constraintList_makeFixedArrayConstraints (body->uses);
986 post2 = reflectChangesFreePre (post2, fix);
987 constraintList_free(fix);
988 if ( context_getFlag (FLG_ORCONSTRAINT) )
989 {
990 t = reflectChangesOr (post2, body->ensuresConstraints);
991 }
992 else
993 {
994 t = reflectChanges (post2, body->ensuresConstraints);
995 }
996
997 constraintList_free(post2);
998
999 constraintList_free(post);
1000 post = t;
1001
1002
1003
1004 printf("Unresolved post conditions\n");
1005 constraintList_printErrorPostConditions(post, g_currentloc);
1006 }
1007 }
1008
1009 if (post)
1010 constraintList_free(post);
1011
1012
616915dd 1013 constraintList_printError(body->ensuresConstraints, g_currentloc);
1014
8f299805 1015
616915dd 1016 // ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc);
1017
1018 // ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
1019
1020 // printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
1021 // printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
1022
bb25bea6 1023 if (c)
1024 constraintList_free(c);
4ab867d6 1025
1026 context_exitInnerPlain();
1027
bb25bea6 1028 /*is it okay not to free this?*/
4ab867d6 1029 exprNode_free (body);
616915dd 1030}
1031
1032void exprChecks_checkEmptyMacroBody (void)
1033{
1034 uentry hdr;
1035
1036 if (!(context_inFunctionLike () || context_inMacroConstant ()
1037 || context_inMacroUnknown ()))
1038 {
1039 llcontbug
1040 (message ("exprNode_checkEmptyMacroBody: not in macro function or constant: %q",
1041 context_unparse ()));
1042 return;
1043 }
1044
1045 hdr = context_getHeader ();
1046
1047 beginLine ();
1048
1049 if (uentry_isFunction (hdr))
1050 {
1051 voptgenerror
1052 (FLG_MACROEMPTY,
1053 message
1054 ("Macro definition for %q is empty", uentry_getName (hdr)),
1055 g_currentloc);
1056
1057 usymtab_checkFinalScope (FALSE);
1058 }
1059
1060 context_exitFunction ();
1061 return;
1062}
1063
1064void exprNode_checkIterBody (/*@only@*/ exprNode body)
1065{
1066 context_exitAllClauses ();
1067
1068 context_exitFunction ();
1069 exprNode_free (body);
1070}
1071
1072void exprNode_checkIterEnd (/*@only@*/ exprNode body)
1073{
1074 context_exitAllClauses ();
1075 context_exitFunction ();
1076 exprNode_free (body);
1077}
1078
1079static
1080bool checkModifyAuxAux (sRef s, exprNode f, sRef alias, exprNode err)
1081{
1082 bool hasMods = context_hasMods ();
1083 flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
1084
1085 if (exprNode_isDefined (f))
1086 {
1087 f->sets = sRefSet_insert (f->sets, s);
1088 }
1089
1090 if (context_getFlag (FLG_MODIFIES)
1091 && (hasMods || context_getFlag (FLG_MODNOMODS)))
1092 {
1093 sRefSet mods = context_modList ();
1094
1095 if (!sRef_canModify (s, mods))
1096 {
1097 sRef rb = sRef_getRootBase (s);
1098
1099
1100 if (sRef_isGlobal (rb))
1101 {
1102 if (!context_checkGlobMod (rb))
1103 {
1104 return FALSE;
1105 }
1106 }
1107
1108 if (sRef_isInvalid (alias) || sRef_sameName (s, alias))
1109 {
1110 if (sRef_isLocalVar (sRef_getRootBase (s)))
1111 {
1112 voptgenerror
1113 (errCode,
1114 message
1115 ("Undocumented modification of internal state (%q): %s",
1116 sRef_unparse (s), exprNode_unparse (err)),
1117 exprNode_isDefined (f) ? f->loc : g_currentloc);
1118 }
1119 else
1120 {
1121 if (sRef_isSystemState (s))
1122 {
1123 if (errCode == FLG_MODNOMODS)
1124 {
1125 if (context_getFlag (FLG_MODNOMODS))
1126 {
1127 errCode = FLG_MODFILESYSTEM;
1128 }
1129 }
1130 else
1131 {
1132 errCode = FLG_MODFILESYSTEM;
1133 }
1134 }
1135
1136 voptgenerror
1137 (errCode,
1138 message ("Undocumented modification of %q: %s",
1139 sRef_unparse (s), exprNode_unparse (err)),
1140 exprNode_isDefined (f) ? f->loc : g_currentloc);
1141 }
1142
1143 return TRUE;
1144 }
1145 else
1146 {
1147 if (sRef_isReference (s) && !sRef_isAddress (alias))
1148 {
1149 voptgenerror
1150 (errCode,
1151 message
1152 ("Possible undocumented modification of %q through alias %q: %s",
1153 sRef_unparse (s),
1154 sRef_unparse (alias),
1155 exprNode_unparse (err)),
1156 exprNode_isDefined (f) ? f->loc : g_currentloc);
1157 return TRUE;
1158 }
1159 }
1160 }
1161 }
1162 else
1163 {
1164 if (context_maybeSet (FLG_MUSTMOD))
1165 {
1166 (void) sRef_canModify (s, context_modList ());
1167 }
1168
1169 if (sRef_isRefsField (s))
1170 {
1171 sRef_setModified (s);
1172 }
1173 }
1174
1175 return FALSE;
1176}
1177
1178static
1179bool checkModifyAux (sRef s, exprNode f, sRef alias, exprNode err)
1180{
1181 DPRINTF (("Check modify aux: %s", sRef_unparseFull (s)));
1182
1183 if (sRef_isReference (s) && sRef_isObserver (s)
1184 && context_maybeSet (FLG_MODOBSERVER))
1185 {
1186 cstring sname;
1187
1188 if (sRef_isPointer (s))
1189 {
1190 sRef base = sRef_getBase (s);
1191 sname = sRef_unparse (base);
1192 }
1193 else
1194 {
1195 if (sRef_isAddress (s))
1196 {
1197 sRef p = sRef_constructPointer (s);
1198 sname = sRef_unparse (p);
1199 }
1200 else
1201 {
1202 sname = sRef_unparse (s);
1203 }
1204 }
1205
1206 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1207 {
1208 if (sRef_isMeaningful (s))
1209 {
1210 if (optgenerror
1211 (FLG_MODOBSERVER,
1212 message ("Suspect modification of observer %s: %s",
1213 sname, exprNode_unparse (err)),
1214 exprNode_isDefined (f) ? f->loc : g_currentloc))
1215 {
1216 sRef_showExpInfo (s);
1217 }
1218 }
1219 else
1220 {
1221 voptgenerror
1222 (FLG_MODOBSERVER,
1223 message ("Suspect modification of observer returned by "
1224 "function call: %s",
1225 exprNode_unparse (err)),
1226 exprNode_isDefined (f) ? f->loc : g_currentloc);
1227 }
1228 }
1229 else
1230 {
1231 if (optgenerror
1232 (FLG_MODOBSERVER,
1233 message ("Suspect modification of observer %s through alias %q: %s",
1234 sname, sRef_unparse (alias), exprNode_unparse (err)),
1235 exprNode_isDefined (f) ? f->loc : g_currentloc))
1236 {
1237 sRef_showExpInfo (s);
1238 }
1239 }
1240
1241 cstring_free (sname);
1242 }
1243
1244 (void) checkModifyAuxAux (s, f, alias, err);
1245 return FALSE;
1246}
1247
1248static
1249bool checkModifyValAux (sRef s, exprNode f, sRef alias, exprNode err)
1250{
1251 (void) checkModifyAuxAux (s, f, alias, err);
1252 return FALSE;
1253}
1254
1255static
1256bool checkCallModifyAux (sRef s, exprNode f, sRef alias, exprNode err)
1257{
1258 bool result = FALSE;
1259
1260 if (sRef_isObserver (s) && context_maybeSet (FLG_MODOBSERVER))
1261 {
1262 sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
1263 cstring sname = sRef_unparse (p);
1264
1265 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1266 {
1267 if (sRef_isMeaningful (s))
1268 {
1269 result = optgenerror
1270 (FLG_MODOBSERVER,
1271 message ("Suspect modification of observer %s: %s",
1272 sname, exprNode_unparse (err)),
1273 exprNode_isDefined (f) ? f->loc : g_currentloc);
1274 }
1275 else
1276 {
1277 result = optgenerror
1278 (FLG_MODOBSERVER,
1279 message ("Suspect modification of observer returned by "
1280 "function call: %s",
1281 exprNode_unparse (err)),
1282 exprNode_isDefined (f) ? f->loc : g_currentloc);
1283 }
1284 }
1285 else
1286 {
1287 result = optgenerror
1288 (FLG_MODOBSERVER,
1289 message
1290 ("Suspect modification of observer %s through alias %q: %s",
1291 sname, sRef_unparse (alias), exprNode_unparse (err)),
1292 exprNode_isDefined (f) ? f->loc : g_currentloc);
1293 }
1294
1295 cstring_free (sname);
1296 }
1297 else if (context_maybeSet (FLG_MODIFIES))
1298 {
1299 if (!(sRef_canModifyVal (s, context_modList ())))
1300 {
1301 sRef p = sRef_isAddress (s) ? sRef_constructPointer (s) : s;
1302 cstring sname = sRef_unparse (p);
1303 bool hasMods = context_hasMods ();
1304 sRef rb = sRef_getRootBase (s);
1305 flagcode errCode = hasMods ? FLG_MODIFIES : FLG_MODNOMODS;
1306 bool check = TRUE;
1307
1308 if (sRef_isGlobal (rb))
1309 {
1310 uentry ue = sRef_getUentry (rb);
1311
1312 /* be more specific here! */
1313 if (!uentry_isCheckedModify (ue))
1314 {
1315 check = FALSE;
1316 }
1317 }
1318
1319 if (check)
1320 {
1321 if (!sRef_isValid (alias) || sRef_sameName (s, alias))
1322 {
1323 if (sRef_isLocalVar (sRef_getRootBase (s)))
1324 {
1325 voptgenerror
1326 (errCode,
1327 message
1328 ("Undocumented modification of internal "
1329 "state (%q) through call to %s: %s",
1330 sRef_unparse (s), exprNode_unparse (f),
1331 exprNode_unparse (err)),
1332 exprNode_isDefined (f) ? f->loc : g_currentloc);
1333 }
1334 else
1335 {
1336 if (sRef_isSystemState (s))
1337 {
1338 if (errCode == FLG_MODNOMODS)
1339 {
1340 if (context_getFlag (FLG_MODNOMODS))
1341 {
1342 errCode = FLG_MODFILESYSTEM;
1343 }
1344 }
1345 else
1346 {
1347 errCode = FLG_MODFILESYSTEM;
1348 }
1349 }
1350
1351 result = optgenerror
1352 (errCode,
1353 message ("Undocumented modification of %s "
1354 "possible from call to %s: %s",
1355 sname,
1356 exprNode_unparse (f),
1357 exprNode_unparse (err)),
1358 exprNode_isDefined (f) ? f->loc : g_currentloc);
1359 }
1360 }
1361 else
1362 {
1363 result = optgenerror
1364 (errCode,
1365 message ("Undocumented modification of %s possible "
1366 "from call to %s (through alias %q): %s",
1367 sname,
1368 exprNode_unparse (f),
1369 sRef_unparse (alias),
1370 exprNode_unparse (err)),
1371 exprNode_isDefined (f) ? f->loc : g_currentloc);
1372 }
1373 }
1374 cstring_free (sname);
1375 }
1376 }
1377 else
1378 {
1379 if (context_maybeSet (FLG_MUSTMOD))
1380 {
1381 (void) sRef_canModifyVal (s, context_modList ());
1382 }
1383 }
1384
1385 return result;
1386}
1387
1388void exprNode_checkCallModifyVal (sRef s, exprNodeList args, exprNode f, exprNode err)
1389{
1390 s = sRef_fixBaseParam (s, args);
1391 sRef_aliasCheckPred (checkCallModifyAux, NULL, s, f, err);
1392}
1393
1394void
1395exprChecks_checkExport (uentry e)
1396{
1397 if (context_checkExport (e))
1398 {
1399 fileloc fl = uentry_whereDeclared (e);
1400
1401 if (fileloc_isHeader (fl) && !fileloc_isLib (fl)
1402 && !fileloc_isImport (fl) && !uentry_isStatic (e))
1403 {
1404 if (uentry_isFunction (e) ||
1405 (uentry_isVariable (e) && ctype_isFunction (uentry_getType (e))))
1406 {
1407 voptgenerror
1408 (FLG_EXPORTFCN,
1409 message ("Function exported, but not specified: %q",
1410 uentry_getName (e)),
1411 fl);
1412 }
1413 else if (uentry_isExpandedMacro (e))
1414 {
1415 voptgenerror
1416 (FLG_EXPORTMACRO,
1417 message ("Expanded macro exported, but not specified: %q",
1418 uentry_getName (e)),
1419 fl);
1420 }
1421 else if (uentry_isVariable (e) && !uentry_isParam (e))
1422 {
1423 voptgenerror
1424 (FLG_EXPORTVAR,
1425 message ("Variable exported, but not specified: %q",
1426 uentry_getName (e)),
1427 fl);
1428 }
1429 else if (uentry_isEitherConstant (e))
1430 {
1431 voptgenerror
1432 (FLG_EXPORTCONST,
1433 message ("Constant exported, but not specified: %q",
1434 uentry_getName (e)),
1435 fl);
1436 }
1437 else if (uentry_isIter (e) || uentry_isEndIter (e))
1438 {
1439 voptgenerror
1440 (FLG_EXPORTITER,
1441 message ("Iterator exported, but not specified: %q",
1442 uentry_getName (e)),
1443 fl);
1444 }
1445
1446 else if (uentry_isDatatype (e))
1447 {
1448 ; /* error already reported */
1449 }
1450 else
1451 {
1452 BADEXIT;
1453 }
1454 }
1455 }
1456}
1457
1458static void checkSafeReturnExpr (/*@notnull@*/ exprNode e)
1459{
1460 ctype tr = ctype_returnValue (context_currentFunctionType ());
1461 ctype te = exprNode_getType (e);
1462
1463 if (!ctype_forceMatch (tr, te) && !exprNode_matchLiteral (tr, e))
1464 {
1465 (void) gentypeerror
1466 (te, e, tr, exprNode_undefined,
1467 message ("Return value type %t does not match declared type %t: %s",
1468 te, tr, exprNode_unparse (e)),
1469 e->loc);
1470 }
1471 else
1472 {
1473 sRef ret = e->sref;
1474 uentry rval = context_getHeader ();
1475 sRef resultref = uentry_getSref (rval);
1476
1477 checkReturnTransfer (e, rval);
1478
1479 if (!(sRef_isExposed (uentry_getSref (context_getHeader ()))
1480 || sRef_isObserver (uentry_getSref (context_getHeader ())))
1481 && (context_getFlag (FLG_RETALIAS)
1482 || context_getFlag (FLG_RETEXPOSE)))
1483 {
1484 sRef base = sRef_getRootBase (ret);
1485 ctype rtype = e->typ;
1486
1487 if (ctype_isUnknown (rtype))
1488 {
1489 rtype = tr;
1490 }
1491
1492 if (ctype_isVisiblySharable (rtype))
1493 {
1494 if (context_getFlag (FLG_RETALIAS))
1495 {
1496 sRef_aliasCheckPred (checkRefGlobParam, NULL, base,
1497 e, exprNode_undefined);
1498 }
1499
1500 if (context_getFlag (FLG_RETEXPOSE) && sRef_isIReference (ret)
1501 && !sRef_isExposed (resultref) && !sRef_isObserver (resultref))
1502 {
1503 sRef_aliasCheckPred (checkRepExposed, NULL, base, e,
1504 exprNode_undefined);
1505 }
1506 }
1507 }
1508 }
1509}
1510
git-cvsimport mirror of splint
This page took 0.304273 seconds and 5 git commands to generate.