/*
** 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 "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "cgrammar.h"
-
-# ifndef NOLCL
# include "usymtab_interface.h"
-# endif
# include "structNames.h"
# include "nameChecks.h"
+# include "cscannerHelp.h"
+
# ifdef SANITIZER
# include "sgrammar_tokens.h"
# else
/*drl added 3-28-2002*/
/* this function takes a list of paramentar and generates a list
of constraints.
- Currently the only constraints gnerated are MaxSet(p) >= 0 for all pointers
*/
-void setImplictfcnConstraints (void)
+/* drl modified 10/23/2002
+
+The current semantics are generated constraints of the form MaxSet(p) >= 0 and MaxRead(p) >= 0 for all pointers
+unless the @out@ annotation has been applied to a parameter, then we only want to generate maxSet(p) > = 0
+*/
+
+void setImplictfcnConstraints (void)
{
uentryList params;
sRef s;
constraint c;
params = currentParamList;
- if (constraintList_isDefined(implicitFcnConstraints) )
- constraintList_free(implicitFcnConstraints);
-
- implicitFcnConstraints = constraintList_makeNew();
+ if (constraintList_isDefined (implicitFcnConstraints))
+ {
+ constraintList_free (implicitFcnConstraints);
+ }
+
+ implicitFcnConstraints = constraintList_makeNew();
uentryList_elements (params, el)
{
- DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+ DPRINTF (("setImplictfcnConstraints doing: %s", uentry_unparse(el)));
- s = uentry_getSref(el);
- if (sRef_isReference (s) )
+ if (uentry_isVariable (el))
+ {
+ s = uentry_getSref(el);
+
+ if (sRef_isReference (s))
+ {
+ DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ /*drl 4/26/01
+ chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */
+ c = constraint_makeSRefWriteSafeInt (s, 0);
+
+ implicitFcnConstraints = constraintList_add (implicitFcnConstraints , c);
+
+ /*drl 10/23/2002 added support for out*/
+
+ if (!uentry_isOut(el))
+ {
+ c = constraint_makeSRefReadSafeInt (s, 0);
+ implicitFcnConstraints = constraintList_add (implicitFcnConstraints , c);
+ }
+ }
+ else
+ {
+ DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ }
+ } /*end uentry_isVariable*/
+ else if (uentry_isElipsisMarker (el) )
{
- DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ /* just ignore these*/
+ ;
}
+
else
{
- DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ /* just ignore this
+ I'm not sure if this is possible though
+ */
+ ;
}
- /*drl 4/26/01
- chagned this is MaxSet(s) == 0 to MaxSet(s) >= 0 */
-
- c = constraint_makeSRefWriteSafeInt (s, 0);
- /* constraint_makeSRefSetBufferSize (s, 0); */
- implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
- }
- end_uentryList_elements;
+ } end_uentryList_elements;
}
-/*@observer@*/ constraintList getImplicitFcnConstraints (void)
+/*@observer@*/ constraintList getImplicitFcnConstraints (void)
{
return implicitFcnConstraints;
}
void clearCurrentParams (void)
{
- currentParamList = uentryList_undefined;
+ currentParamList = uentryList_undefined;
}
/*
vgenhinterror
(FLG_SYNTAX,
message ("Member of boolean enumerated type definition "
- "does not match name set to represent TRUE "
- "or FALSE: %s",
+ "does not match name set to represent true "
+ "or false: %s",
ye),
message ("Use -boolfalse and -booltrue to set the "
"name of false and true boolean values."),
if (usymtab_exists (n))
{
usymId llm = usymtab_getId (n);
- uentry le = usymtab_getTypeEntry (llm);
+ uentry le = usymtab_getTypeEntry (typeId_fromUsymId (llm));
uentry_setDeclared (e, g_currentloc);
uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le), stateInfo_currentLoc ()));
uentryList_elements (params, current)
{
uentry_setParam (current);
- uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (uentry_whereLast (current))));
+ uentry_setSref (current, sRef_makeParam
+ (paramno, ctype_unknown,
+ stateInfo_makeLoc (uentry_whereLast (current), SA_DECLARED)));
paramno++;
} end_uentryList_elements;
setGenericParamList (params);
- g_expectingTypeName = TRUE;
+ cscannerHelp_setExpectingTypeName ();
return params;
}
setGenericParamList (params);
flipOldStyle = FALSE;
- g_expectingTypeName = TRUE;
+ cscannerHelp_setExpectingTypeName ();
}
return (params);
if (i >= 0)
{
fileloc loc = context_getSaveLocation ();
- e = uentry_makeVariableSrefParam (id, c, loc, sRef_makeParam (i, c, stateInfo_makeLoc (loc)));
+ e = uentry_makeVariableSrefParam
+ (id, c, loc,
+ sRef_makeParam (i, c, stateInfo_makeLoc (loc, SA_DECLARED)));
}
else
{
voptgenerror
(FLG_COMMENTERROR,
message ("Global variable %s used state clause. (Global variables "
- "are not recognized in state clauses. If there is "
+ "are not recognized in state clauses. If they are present "
+ "they are ignored. "
+ " If there is "
"sufficient interest in support for this, it may be "
"added to a future release. Send mail to "
"info@splint.org.)",
sRef checkbufferConstraintClausesId (uentry ue)
{
+ sRef sr;
cstring s = uentry_rawName (ue);
if (cstring_equalLit (s, "result"))
}
}
- DPRINTF (("constrant id: %s", uentry_unparseFull (ue)));
- return sRef_saveCopy (uentry_getSref (ue)); /*@i523 why the saveCopy? */
+ sr = uentry_getSref (ue);
+
+ if (sRef_isInvalid (sr))
+ {
+ llfatalerrorLoc (cstring_makeLiteral ("Macro defined constants can not be used in function "
+ "constraints unless they are specifed with the constant "
+ "annotation. To use a macro defined constant include an "
+ "annotation of the form /*@constant <type> <name>=<value>@*/ "
+ "somewhere before the function constraint. This restriction "
+ "may be removed in future releases."));
+ }
+
+ /* saveCopy to used to mitigate danger of accessing freed memory*/
+ return sRef_saveCopy (sr);
}
void checkModifiesId (uentry ue)
}
else
{
- /*@i222@*/
- /*drl handle structure invariant */
- /*@i222@*/
+ /* drl This is the code for structure invariants
+
+ It is no yet stable enough to be included in a Splint release.
+ */
+
/*check that we're in a structure */
-# if 0\r
+#if 0
/*@unused@*/ uentryList ueL;
/*@unused@*/ uentry ue2;
/*@unused@*/ ctype ct;\r
-# endif
+#endif
fileloc loc = fileloc_decColumn (g_currentloc, size_toInt (cstring_length (s)));
ret = sRef_undefined;
# if 0
- /*drl commenting this out for now
+
ct = context_getLastStruct ( ct );
llassert( ctype_isStruct(ct) );
return ret;
}
- */\r
-# endif\r
+
+#endif
voptgenerror
(FLG_UNRECOG,
andersk / splint.git / blobdiff