/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "basic.h"
# include "cgrammar.h"
# include "cscanner.h"
+# include "cscannerHelp.h"
# include "cgrammar_tokens.h"
# include "exprChecks.h"
}
e->guards = guardSet_new ();
+
e->sets = sRefSet_new ();
e->msets = sRefSet_new ();
e->uses = sRefSet_new ();
if (context_justPopped ()) /* watch out! c could be dead */
{
- uentry ce = usymtab_lookupSafe (cscanner_observeLastIdentifier ());
+ uentry ce = usymtab_lookupSafe (cscannerHelp_observeLastIdentifier ());
if (uentry_isValid (ce))
{
{
if (!usymtab_isGuarded (arr->sref))
{
- if (optgenerror (FLG_NULLDEREF,
- message ("Index of %s pointer %q: %s",
- sRef_nullMessage (arr->sref),
- sRef_unparse (arr->sref),
- exprNode_unparse (arr)),
- arr->loc))
- {
- DPRINTF (("ref: %s", sRef_unparseFull (arr->sref)));
- sRef_showNullInfo (arr->sref);
-
- /* suppress future messages */
- sRef_setNullError (arr->sref);
+ if (!context_inSizeof() )
+ {
+ if (optgenerror (FLG_NULLDEREF,
+ message ("Index of %s pointer %q: %s",
+ sRef_nullMessage (arr->sref),
+ sRef_unparse (arr->sref),
+ exprNode_unparse (arr)),
+ arr->loc))
+ {
+ DPRINTF (("ref: %s", sRef_unparseFull (arr->sref)));
+ sRef_showNullInfo (arr->sref);
+
+ /* suppress future messages */
+ sRef_setNullError (arr->sref);
+ }
}
}
}
exprNode_unparse (e1), exprNode_unparse (e2)),
arr->loc);
}
+ else if (ctype_isNumAbstract (rt))
+ {
+ vnoptgenerror
+ (FLG_NUMABSTRACTINDEX,
+ message ("Array fetch using numabstract type, %t: %s[%s]",
+ ind->typ,
+ exprNode_unparse (e1), exprNode_unparse (e2)),
+ arr->loc);
+ }
else
{
voptgenerror
expecttype = ctype_makeConj (ctype_int,
ctype_makeConj (ctype_char,
ctype_uchar));
- /*@i231@*/
/* evans 2001-10-05 - changed to reflect correct ISO spec:
int converted to char */
- /* expecttype = ctype_makeConj (ctype_char, ctype_uchar); */
/*@switchbreak@*/ break;
case 's': /* string */
case 'i':
case 'd':
+ expecttype = ctype_makePointer (ctype_combine (ctype_int, modtype));
+ /*@switchbreak@*/ break;
+
case 'x':
case 'X': /* unsigned int */
- expecttype = ctype_makePointer (ctype_combine (ctype_int, modtype));
+ expecttype = ctype_makePointer (ctype_combine (ctype_uint, modtype));
/*@switchbreak@*/ break;
case 'e':
codetext, expecttype,
a->typ, exprNode_unparse (a)),
a->loc))
- {
+ {
if (fileloc_isDefined (formatloc)
&& context_getFlag (FLG_SHOWCOL))
{
f->guards = guardSet_union (f->guards, a->guards);
DPRINTF (("match arg: %s / %s", ctype_unparse (ct), ctype_unparse (a->typ)));
-
+
if (!(exprNode_matchArgType (ct, a)))
{
DPRINTF (("Args mismatch!"));
uentry_unparse (le)));
params = ctype_argsFunction (ct);
- return; /*@32 ! remove this? */
+ return; /* No checking for non-function */
}
/*
if (sRef_isResult (sRef_getRootBase (sel)))
{
- ; /*@i423 what do we do about results */
+ ; /* what do we do about results? */
}
else
{
exprNode_checkModify (e, ret);
/* added 7/11/2000 D.L */
- /*@i223*/
- /*DRL 6/8/01 I decided to disable all Splint warnings here since the code
- probably needs a rewrite any way */
-
- /*@i65234@*/
- /*@ignore@*/
/* updateEnvironmentForPostOp (e); */
printf ("ret->sref is Possibly Null Terminated\n");
else if (sRef_isNotNullTerminated (ret->sref))
printf ("ret->sref is Not Null Terminated\n");
+ else
+ {}
}
}
}
}
}
- /*@end@*/
/* end modifications */
return ret;
ret->edata = exprData_makeCast (tok, e, q);
ret->sref = sRef_copy (e->sref);
-
- DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
+
+ DPRINTF (("Cast: -> %s", sRef_unparseFull (ret->sref)));
if (!sRef_isConst (e->sref))
{
if (opid == OR_OP)
{
+ exprNode_produceGuards (e2);
ret->guards = guardSet_or (ret->guards, e2->guards);
}
else if (opid == AND_OP)
{
+ exprNode_produceGuards (e2); /* evans 2003-08-13: need to produce guards for expression */
+ /* Shouldn't this have already happened? */
+ DPRINTF (("Anding guards: %s / %s", guardSet_unparse (ret->guards), guardSet_unparse (e2->guards)));
ret->guards = guardSet_and (ret->guards, e2->guards);
}
else
status */
if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) {
- int val = (int) multiVal_forceInt (e1->val);
-
- /* Operator : + or += */
- if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
- if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by
- val should not result in a
- size < 0 (size = 0 is ok !) */
+ if (multiVal_isDefined (e1->val))
+ {
+ int val = (int) multiVal_forceInt (e1->val);
- sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
+ /* Operator : + or += */
+ if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
+ if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by
+ val should not result in a
+ size < 0 (size = 0 is ok !) */
+
+ sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
+
+ if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
+ sRef_setNotNullTerminatedState(ret->sref);
+ sRef_resetLen (ret->sref);
+ } else {
+ sRef_setNullTerminatedState(ret->sref);
+ sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
+ }
+ }
+ }
- if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
- sRef_setNotNullTerminatedState(ret->sref);
- sRef_resetLen (ret->sref);
- } else {
- sRef_setNullTerminatedState(ret->sref);
- sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
+ /* Operator : - or -= */
+ if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
+ if (sRef_getSize(e2->sref) >= 0) {
+ sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
+ sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
+ }
}
}
- }
-
- /* Operator : - or -= */
- if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
- if (sRef_getSize(e2->sref) >= 0) {
- sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
- sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
- }
- }
}
+
/* end modifications */
sRef_setNullError (ret->sref);
}
else
{
- voptgenerror
- (FLG_REALCOMPARE,
- message ("Dangerous comparison involving %s types: %s",
- ctype_unparse (rtype),
- exprNode_unparse (ret)),
- ret->loc);
+ if (opid == EQ_OP || opid == NE_OP)
+ {
+ voptgenerror
+ (FLG_REALCOMPARE,
+ message ("Dangerous equality comparison involving %s types: %s",
+ ctype_unparse (rtype),
+ exprNode_unparse (ret)),
+ ret->loc);
+ }
+ else
+ {
+ voptgenerror
+ (FLG_REALRELATECOMPARE,
+ message ("Possibly dangerous relational comparison involving %s types: %s",
+ ctype_unparse (rtype),
+ exprNode_unparse (ret)),
+ ret->loc);
+ }
}
}
/*@fallthrough@*/
*/
if (!ctype_isUA (targ) ||
- (!usymId_equal (ctype_typeId (targ),
- usymtab_getTypeId (cstring_makeLiteralTemp ("va_list")))))
+ (!typeId_equal (ctype_typeId (targ),
+ usymtab_getTypeId (cstring_makeLiteralTemp ("va_list")))))
{
voptgenerror
(FLG_TYPE,
exprNode exprNode_createTok (/*@only@*/ lltok t)
{
- exprNode ret; /*@i23 if on same line, bad things happen...!@*/
- ret = exprNode_create (ctype_unknown);
+ exprNode ret = exprNode_create (ctype_unknown);
ret->kind = XPR_TOK;
ret->edata = exprData_makeTok (t);
return ret;
exprNode_loc (pred));
}
- /*! exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); */ /*@i523@*/
exprNode_checkUse (pred, pred->sref, pred->loc);
if (!exprNode_isError (tclause))
exprNode_loc (pred));
}
- /*@i3423 exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);*/
exprNode_checkUse (ret, pred->sref, pred->loc);
-
exprNode_mergeCondUSs (ret, tclause, eclause);
}
{
uentry ue = usymtab_lookup (idDecl_observeId (t));
ret = exprNode_createId (ue);
-
- /*@i723 don't do this...but why? */
-# if 0
- ct = ctype_realishType (ret->typ);
-
- DPRINTF (("Type: %s", ctype_unparse (ret->typ)));
-
- if (ctype_isUnknown (ct))
- {
- if (uentry_isAnyTag (ue))
- {
- voptgenerror
- (FLG_IMPTYPE,
- message ("%s used but not previously declared: %s",
- uentry_ekindName (ue),
- idDecl_getName (t)),
- g_currentloc);
-
- }
- else
- {
- voptgenerror
- (FLG_IMPTYPE,
- message ("Variable has unknown (implicitly int) type: %s",
- idDecl_getName (t)),
- g_currentloc);
- }
-
- ct = ctype_int;
- }
-# endif
}
else
{
DPRINTF (("Unrecognized: %s", idDecl_unparse (t)));
ue = uentry_makeUnrecognized (idDecl_observeId (t), fileloc_copy (g_currentloc));
- /*!! fileloc_copy (g_currentloc)); */
- /*@i32!!! should get error without this */
-
ret = exprNode_fromIdentifierAux (ue);
/*
}
else if (multiVal_isChar (m))
{
- char val = multiVal_forceChar (m);
+ /*signed? */ char val = multiVal_forceChar (m);
if (ctype_isChar (expected))
{
- if (ctype_isUnsigned (expected) && ((int)val) < 0)
+ if (ctype_isUnsigned (expected) && ((int) val) < 0)
{
return FALSE;
}
{
lastRef = errorRef;
errorRef = s;
+ DPRINTF (("Setting ERROR: %s", sRef_unparseFull (s)));
deadRef = sRef_isDead (errorRef);
unuseable = sRef_isUnuseable (errorRef);
errorMaybe = FALSE;
}
+ /*
if (!sRef_isPartial (s))
{
DPRINTF (("Defining! %s", sRef_unparseFull (s)));
- sRef_setDefined (s, fileloc_undefined);
+ sRef_setDefined (s, loc);
+ DPRINTF (("Defining! %s", sRef_unparseFull (s)));
}
+ */
}
s = sRef_getBaseSafe (s);
&& sRef_isPointer (errorRef))
{
errorRef = lastRef;
+ DPRINTF (("errorRef: %s", sRef_unparseFull (errorRef)));
}
if (deadRef)
}
else
{
- DPRINTF (("HERE: %s", sRef_unparse (errorRef)));
+ DPRINTF (("HERE: %s", sRef_unparseFull (errorRef)));
if (optgenerror
(FLG_USERELEASED,
{
DPRINTF (("HERE: %s", sRef_unparseFull (errorRef)));
- voptgenerror
- (FLG_USEDEF,
- message ("%q %q%qused before definition",
- sRef_unparseKindName (errorRef),
- sRef_unparseOpt (errorRef),
- cstring_makeLiteral (errorMaybe ? "may be " : "")),
- loc);
+ if (optgenerror
+ (FLG_USEDEF,
+ message ("%q %q%qused before definition",
+ sRef_unparseKindName (errorRef),
+ sRef_unparseOpt (errorRef),
+ cstring_makeLiteral (errorMaybe ? "may be " : "")),
+ loc))
+ {
+ ;
+ }
DPRINTF (("Error: %s", sRef_unparseFull (errorRef)));
}
DPRINTF (("No error: [%s] %s / [%s] %s",
exprNode_unparse (e1), ctype_unparse (tr1),
exprNode_unparse (e2), ctype_unparse (tr2)));
+
+ /*
+ ** evans 2003-06-15: changed this so if either type is a literal,
+ ** the other type is used.
+ ** (Need to look at the ISO C99 rules on this...)
+ */
- ret = ctype_biggerType (tr1, tr2);
+ if (exprNode_isNumLiteral (e1)) {
+ ret = tr2;
+ } else if (exprNode_isNumLiteral (e2)) {
+ ret = tr1;
+ } else {
+ ret = ctype_biggerType (tr1, tr2);
+ }
}
else
{
}
else
{
- return optgenerror
- (FLG_ABSTRACT,
- message ("Operands of %s are abstract type (%t): %s %s %s",
- lltok_unparse (op), tr1,
- exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)),
- loc1);
+ if (lltok_isEqOp (op) || lltok_isNotEqOp (op))
+ {
+ return optgenerror
+ (FLG_ABSTRACTCOMPARE,
+ message ("Object equality comparison (%s) on objects of abstract type (%t): %s %s %s",
+ lltok_unparse (op), tr1,
+ exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)),
+ loc1);
+ }
+ else
+ {
+ return optgenerror
+ (FLG_ABSTRACT,
+ message ("Operands of %s are abstract type (%t): %s %s %s",
+ lltok_unparse (op), tr1,
+ exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)),
+ loc1);
+ }
}
}
else
ctype ct = sRef_getType (sr);
if (ctype_isAbstract (t2)
+ && !ctype_isNumAbstract (t2)
&& !(uentry_isMutableDatatype (usymtab_getTypeEntry (ctype_typeId (t2)))))
{
/* it is immutable, okay to reference */
} end_exprNodeList_elements;
}
-long exprNode_getLongValue (exprNode e) {
+long exprNode_getLongValue (exprNode e)
+{
long value;
-
- if (exprNode_hasValue (e)
- && multiVal_isInt (exprNode_getValue (e)))
+
+ if (exprNode_hasValue (e) && multiVal_isInt (exprNode_getValue (e)))
{
value = multiVal_forceInt (exprNode_getValue (e));
}
else
{
- /*@!! BADBRANCH;*/
- value = 0;
+ value = 0; /* Unknown value */
}
return value;
}
-/*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e)
-{
- if (exprNode_isDefined (p_e) )
- return ( p_e->loc );
- else
- return fileloc_undefined;
-}
-
/*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode e)
{
/*
{
return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK);
}
+
+/*drl 3/2/2003 moved this function out of constraint.c */
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
+{
+
+ llassert (exprNode_isDefined (dst) );
+ llassert (exprNode_isDefined (src) );
+
+ constraintList_free (dst->ensuresConstraints);
+ constraintList_free (dst->requiresConstraints);
+ constraintList_free (dst->trueEnsuresConstraints);
+ constraintList_free (dst->falseEnsuresConstraints);
+
+ dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints);
+ dst->requiresConstraints = constraintList_copy (src->requiresConstraints);
+ dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints);
+ dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
+ return dst;
+}
+
+void exprNode_revealState (exprNode e)
+{
+ if (exprNode_isDefined (e)) {
+ llmsg (message ("%s: State of %s: %s", fileloc_unparse (exprNode_loc (e)),
+ exprNode_unparse (e), sRef_unparseFull (e->sref)));
+ } else {
+ llmsg (message ("%s: Reveal state undefined", fileloc_unparse (g_currentloc)));
+ }
+}
andersk / splint.git / blobdiff