/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
*/
# ifndef UENTRY_H
** vkind --- need to fix value for consistency in dump files
*/
-typedef struct _ucinfo
+typedef struct
{
- /*@only@*/ multiVal val;
- typeIdSet access;
+ typeIdSet access;
+ bool macro;
} *ucinfo;
typedef enum
} chkind;
/* start modifications */
-typedef enum _bbufstate {
+typedef enum {
BB_POSSIBLYNULLTERMINATED, /* buffer is possibly nullterm(can't decide statically) */
BB_NULLTERMINATED, /*buffer is known to be nullterminated */
BB_NOTNULLTERMINATED /* buffer is known to be not nullterm */
} bbufstate;
-typedef struct _bbufinfo {
+typedef /*@null@*/ struct s_bbufinfo {
bbufstate bufstate; /* state of the buffer */
int size; /* size of the buffer allocated */
int len; /* len of the buffer VALID ONLY IF state is NULLTERM */
} *bbufinfo ;
-typedef struct _uvinfo
+typedef struct
{
vkind kind; /* kind (parameter, specified) */
chkind checked; /* how is it checked */
} *uvinfo ;
/* end modifications */
-typedef struct _udinfo
+typedef struct
{
- ynm abs;
+ qual abs; /* oneof QU_UNKNOWN, QU_ABSTRACT, QU_NUMABSTRACT, QU_CONCRETE */
ynm mut;
ctype type;
} *udinfo ;
SPC_LAST
} specCode;
-typedef struct _ufinfo
+typedef struct
{
qual nullPred;
specCode specialCode;
/*@owned@*/ globSet globs; /* globals list */
/*@owned@*/ sRefSet mods; /* modifies */
- specialClauses specclauses;
+ stateClauseList specclauses;
/*@dependent@*/ uentryList defparams;
bool hasGlobs BOOLBITS;
bool hasMods BOOLBITS;
+
+ functionConstraint preconditions;
+ functionConstraint postconditions;
+
} *ufinfo ;
-typedef struct _uiinfo
+typedef struct
{
typeIdSet access;
/*@owned@*/ globSet globs; /* globals list */
/*@owned@*/ sRefSet mods; /* modifies */
} *uiinfo ;
-typedef struct _ueinfo
+typedef struct
{
- typeIdSet access;
+ typeIdSet access;
} *ueinfo ;
-typedef union _uinfo
+typedef union
{
ucinfo uconst;
uvinfo var;
ueinfo enditer;
} *uinfo ;
-struct _uentry
+struct s_uentry
{
ekind ukind;
cstring uname;
** functions state of return value
** types state of datatype
*/
+
/*@exposed@*/ /*@null@*/ sRef sref;
+ warnClause warn;
+
/* Location list is complete only if showalluses is set. */
filelocList uses;
/*
** There is no uentry_isDefined to avoid confusion with
** uentry_isCodeDefined (which was previously called
-** uentry_isDefined.
+** uentry_isDefined).
*/
-extern /*@truenull@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e)
+extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e)
/*@*/ ;
-extern /*@truenull@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e)
+extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e)
/*@*/ ;
-extern /*@falsenull@*/ bool uentry_isValid (/*@special@*/ uentry p_e)
+extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e)
/*@*/ ;
/*@constant null uentry uentry_undefined; @*/
extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ;
extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ;
-extern /*@falsenull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
+extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
# define uentry_isLset(e) \
(uentry_isValid(e) && (e)->lset)
-extern /*@falsenull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
+extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
# define uentry_isUsed(e) (uentry_isValid(e) && (e)->used)
-extern /*@unused@*/ /*@falsenull@*/ bool
+extern /*@unused@*/ /*@falsewhennull@*/ bool
uentry_isAbstractType (uentry p_e) /*@*/ ;
# define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e))
-extern /*@falsenull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isConstant(e) \
(uentry_isValid(e) && ekind_isConst ((e)->ukind))
-extern /*@falsenull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isEitherConstant(e) \
(uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind)))
-extern /*@falsenull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isEnumConstant(e) \
(uentry_isValid(e) && ekind_isEnumConst ((e)->ukind))
-extern /*@falsenull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isExternal(c) \
(uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c)))
-extern /*@falsenull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isExtern(c) \
(uentry_isValid(c) && (c)->storageclass == SCEXTERN)
extern bool uentry_isForward (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isFunction(e) \
(uentry_isValid(e) && ekind_isFunction ((e)->ukind))
-extern /*@falsenull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isPriv(e) \
(uentry_isValid(e) && (e)->isPrivate)
-extern /*@falsenull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
# define uentry_isStatic(c) \
(uentry_isValid(c) && (c)->storageclass == SCSTATIC)
extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ;
extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ;
-extern void uentry_checkName (uentry p_ue) /*@modifies g_msgstream, p_ue@*/ ;
+extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
# define uentry_sameObject(e1,e2) ((e1) == (e2))
extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ;
extern void uentry_showWhereAny (uentry p_spec)
- /*@modifies g_msgstream@*/ ;
+ /*@modifies g_warningstream@*/ ;
extern void uentry_checkParams (uentry p_ue);
extern void uentry_mergeUses (uentry p_res, uentry p_other);
extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ;
extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ;
extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
/*@uses p_ue->ukind@*/
/*@*/ ;
-extern /*@falsenull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e)
+extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e)
/*@uses p_e->whereDeclared@*/ /*@*/ ;
extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ;
+extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ;
+
extern void uentry_showWhereDefined (uentry p_spec);
-extern /*@falsenull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
/*@uses p_ue->ukind@*/ /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u)
+extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u)
/*@uses p_u->ukind, p_u->info@*/
/*@*/ ;
-extern /*@falsenull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue)
/*@uses p_ue->ukind@*/ /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
/*@uses p_ue->ukind@*/ /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isVar (/*@special@*/ uentry p_e)
+extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e)
/*@uses p_e->ukind@*/
/*@*/ ;
-extern /*@falsenull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e)
+extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e)
/*@uses p_e->ukind@*/
/*@*/ ;
extern cstring uentry_dump (uentry p_v) ;
extern cstring uentry_dumpParam (uentry p_v);
+
+extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ;
+
extern cstring uentry_getName (/*@special@*/ uentry p_e)
/*@uses p_e->ukind, p_e->info, p_e->uname@*/
/*@*/ ;
extern /*@observer@*/ sRefSet uentry_getMods (uentry p_l) /*@*/ ;
extern typeIdSet uentry_accessType (uentry p_e) /*@*/ ;
extern /*@observer@*/ fileloc uentry_whereEither (uentry p_e) /*@*/ ;
+
+extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s,
/*@temp@*/ fileloc p_f)
/*@*/ ;
-extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_msgstream@*/ ;
+extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ;
-extern /*@observer@*/ specialClauses uentry_getSpecialClauses (uentry p_ue) /*@*/ ;
+extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ;
extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra)
- /*@modifies g_msgstream@*/ ;
+ /*@modifies g_warningstream@*/ ;
-# ifndef NOLCL
extern void uentry_setRefCounted (uentry p_e);
extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t);
+extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/;
extern /*@notnull@*/ uentry
uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access,
uentry_makeSpecFunction (cstring p_n, ctype p_t,
typeIdSet p_access, /*@only@*/ globSet p_globs,
/*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
-# endif
extern /*@notnull@*/ uentry
uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ;
extern /*@notnull@*/ /*@only@*/ uentry
uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
/*@*/ ;
+
+extern /*@only@*/ /*@notnull@*/ uentry
+ uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
+ bool p_priv, /*@only@*/ multiVal p_val)
+ /*@*/ ;
+
extern /*@notnull@*/ /*@only@*/ uentry
- uentry_makeConstantAux (/*@temp@*/ cstring p_n, ctype p_t,
- /*@keep@*/ fileloc p_f, bool p_priv,
- /*@only@*/ multiVal p_m) /*@*/ ;
+ uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
+ /*@*/ ;
+
extern /*@notnull@*/ /*@only@*/ uentry
- uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abs,
+ uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, qual p_abstract,
/*@only@*/ fileloc p_f) /*@*/ ;
extern /*@notnull@*/ /*@only@*/ uentry
uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut,
- ynm p_abs, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
+ qual p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
+extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ;
# define uentry_isElipsisMarker(u) \
uentry_makeFunction (cstring p_n, ctype p_t,
typeId p_access,
/*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods,
+ /*@only@*/ warnClause p_warn,
/*@only@*/ fileloc p_f);
extern /*@notnull@*/ uentry
extern /*@notnull@*/ /*@only@*/ uentry
uentry_makeVariableLoc (cstring p_n, ctype p_t);
-# ifndef NOLCL
extern /*@notnull@*/ /*@only@*/
- uentry uentry_makeVariableParam (cstring p_n, ctype p_t);
-# endif
+ uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
extern /*@notnull@*/ /*@only@*/
- uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t,
- sRef p_s);
+uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
+ /*@exposed@*/ sRef p_s);
extern /*@notnull@*/ /*@only@*/
uentry uentry_makeIdFunction (idDecl p_id);
extern /*@notnull@*/ /*@only@*/
uentry uentry_makeIdDatatype (idDecl p_id);
extern /*@notnull@*/ /*@only@*/
- uentry uentry_makeBoolDatatype (ynm p_abs);
+ uentry uentry_makeBoolDatatype (qual p_abstract);
extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew);
extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def);
extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e);
extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ;
extern qual uentry_nullPred (uentry p_u);
extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e);
-extern void uentry_setDatatype (uentry p_e, usymId p_uid);
+extern void uentry_setDatatype (uentry p_e, typeId p_uid);
extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f)
/*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/
extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr)
/*@modifies p_ue, p_sr@*/;
-extern void uentry_setSpecialClauses (uentry p_ue, /*@only@*/ specialClauses p_clauses)
+extern bool uentry_hasWarning (uentry p_ue) /*@*/ ;
+
+extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn)
+ /*@modifies p_ue*/;
+
+extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses)
/*@modifies p_ue@*/ ;
extern void uentry_setType (uentry p_e, ctype p_t);
extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue);
-extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_msgstream@*/ ;
+extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ;
extern void
uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s)
- /*@modifies g_msgstream@*/ ;
+ /*@modifies g_warningstream@*/ ;
-extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_msgstream@*/ ;
-extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_msgstream@*/ ;
-extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_msgstream@*/ ;
+extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ;
+extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ;
+extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ;
extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ;
extern uentry uentry_copy (uentry p_e) /*@*/ ;
+extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */
extern void uentry_freeComplete (/*@only@*/ uentry p_e) ;
extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/;
extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ;
extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/;
extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ;
-extern bool uentry_isGlobal (uentry p_ue) /*@*/;
+extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/;
+extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/;
extern bool uentry_isRefParam (uentry p_u) /*@*/ ;
extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ;
extern bool uentry_hasMods (uentry p_ue) /*@*/ ;
-extern bool uentry_hasSpecialClauses (uentry p_ue) /*@*/ ;
+extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ;
+extern bool uentry_hasConditions (uentry p_ue) /*@*/ ;
+
extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ;
extern void uentry_checkYieldParam (uentry p_old, uentry p_unew);
extern exkind uentry_getExpKind (uentry p_u) /*@*/ ;
extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ;
extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ;
-extern void uentry_setGlobals (uentry p_ue, /*@owned@*/ globSet p_globs) /*@modifies p_ue@*/ ;
+extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
extern bool uentry_isYield (uentry p_ue) /*@*/ ;
extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ;
extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ;
extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ;
extern void uentry_copyState (uentry p_res, uentry p_other);
extern bool uentry_sameKind (uentry p_u1, uentry p_u2);
-extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args);
+extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc);
extern bool uentry_isReturned (uentry p_u);
extern bool uentry_isRefCountedDatatype (uentry p_e);
extern sstate uentry_getDefState (uentry p_u);
extern bool uentry_hasAccessType (uentry p_e);
-extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@keep@*/ fileloc p_loc);
+/*@constant cstring GLOBAL_MARKER_NAME@*/
+# define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
+/* Null Termination */
-/* start modifications */
-//extern void uentry_setBufferSize (uentry p_e, exprNode cconstant);
-
-/* functions for making modification to null-term info */
extern void uentry_setNullTerminatedState (uentry p_e);
extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
-extern void uentry_setNotNullTerminated (uentry p_e);
extern void uentry_setSize(uentry p_e, int p_size);
extern void uentry_setLen(uentry p_e, int p_len);
-/*@i66*/
-/*@-nullderef@*/
-extern bool uentry_hasBufStateInfo (uentry p_ue);
-# define uentry_hasBufStateInfo(p_ue) \
- (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE)
-
-extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
-# define uentry_isNullTerminated(p_ue) \
- ( uentry_hasBufStateInfo( (p_ue ) ) ? ( (p_ue)->info->var->bufinfo->bufstate \
- == BB_NULLTERMINATED) : FALSE)
-
-extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
-# define uentry_isPossiblyNullTerminated(p_ue) \
- ( uentry_hasBufStateInfo((p_ue)) ? ( (p_ue)->info->var->bufinfo->bufstate \
- == BB_POSSIBLYNULLTERMINATED) : FALSE)
+extern /*@falsewhennull@*/ bool uentry_hasBufStateInfo (uentry p_ue) /*@*/ ;
+extern bool uentry_isNullTerminated (uentry p_ue) /*@*/ ;
+extern bool uentry_isPossiblyNullTerminated (uentry p_ue) /*@*/ ;
+extern bool uentry_isNotNullTerminated (uentry p_ue) /*@*/ ;
-extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
-# define uentry_isNotNullTerminated(p_ue) \
- ( uentry_hasBufStateInfo( (p_ue) ) ? ( (p_ue)->info->var->bufinfo->bufstate \
- == BB_NOTNULLTERMINATED) : FALSE)
-/*@=nullderef@*/
+/* Global Markers */
-/* end modifications */
+extern uentry uentry_makeGlobalMarker (void) ;
+extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
# ifdef DOANNOTS
-typedef enum { AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
- AN_CONST, AN_LAST
- } ancontext;
+typedef enum
+{
+ AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
+ AN_CONST, AN_LAST
+} ancontext;
extern void initAnnots ();
extern void printAnnots (void);
extern void uentry_tallyAnnots (uentry u, ancontext kind);
# endif /* DOANNOTS */
+extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ;
+extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e);
+
/* start modifications */
-extern void uentry_setBufferSize (uentry p_e, exprNode p_cconstant);
+
+/*drl7x*/
+extern constraintList uentry_getFcnPreconditions (uentry p_ue);
+extern constraintList uentry_getFcnPostconditions (uentry p_ue);
+
+extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions);
+
+extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
+/*end mods*/
+
+/*
+** For debugging only
+*/
+
+# ifdef DEBUGSPLINT
+extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ;
+# endif
# else
# error "Multiple include"
andersk / splint.git / blobdiff