-boolfalse FALSE
+numliteral
++numabstractindex
++numabstractlit
+-numabstractprint
-indentspaces 3
# include "varKinds.h"
# include "sRefSet.h"
# include "ekind.h"
+# include "usymId.h"
+# include "typeId.h"
# include "usymIdSet.h"
# include "sRefList.h"
# include "uentryList.h"
# include "mtincludes.h"
# include "functionConstraint.h"
# include "fileIdList.h"
-
# include "context.h"
# include "constants.h"
+# include "llglobals.h"
# else
# error "Multiple include"
extern cstring cstringList_unparseSep (cstringList p_s, cstring p_sep) /*@*/ ;
-extern /*@exposed@*/ /*@null@*/ bn_mstring *cstringList_getElements (cstringList) /*@*/ ;
+extern /*@exposed@*/ /*@null@*/ ob_cstring *cstringList_getElements (cstringList) /*@*/ ;
extern /*@unused@*/ /*@only@*/ cstringList cstringList_new (void) /*@*/ ;
extern cstring fileLib_removePath (cstring p_s) /*@*/ ;
extern cstring fileLib_removePathFree (/*@only@*/ cstring p_s) /*@*/ ;
extern cstring fileLib_removeAnyExtension (cstring p_s) /*@*/ ;
-extern /*@only@*/ cstring fileLib_cleanName (/*@temp@*/ cstring p_s) /*@*/ ;
+extern /*@only@*/ cstring fileLib_cleanName (/*@only@*/ cstring p_s) /*@*/ ;
extern bool fileLib_hasExtension (cstring p_s, cstring p_ext) /*@*/ ;
extern /*@observer@*/ cstring
fileIdList p_lclfiles,
fileIdList p_mtfiles,
cstringList *p_passThroughArgs,
- int p_argc, /*@null@*/ char **p_argv)
+ int p_argc,
+ /*@null@*/ char **p_argv)
/*@requires maxRead(p_argv) >= (p_argc - 1) @*/
/* returns true if normal, false if execution should exit */ ;
functionClauseList_add (/*@returned@*/ functionClauseList p_s, /*@keep@*/ functionClause p_el)
/*@modifies p_s@*/ ;
-extern functionClauseList
- functionClauseList_prepend (/*@returned@*/ functionClauseList p_s, /*@keep@*/ functionClause p_el)
+extern /*@only@*/ functionClauseList
+ functionClauseList_prepend (/*@only@*/ functionClauseList p_s, /*@keep@*/ functionClause p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring functionClauseList_unparse (functionClauseList p_s) ;
+++ /dev/null
-/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
-** See ../LICENSE for license information.
-**
-*/
-
-# ifndef LLBASIC_H
-# define LLBASIC_H
-
-# include "basic.h"
-# include "llglobals.h"
-
-# else
-# error "Multiple include"
-# endif
-
-
-
-
-
extern /*@observer@*/ cstring lldecodeerror (int) /*@*/ ;
-/*@i523@*/
/*
** should be static, but used in cpperror (which shouldn't exist)
*/
# include "mstring.h"
-
extern int int_compare (/*@sef@*/ int p_x, /*@sef@*/ int p_y) /*@*/ ;
# define int_compare(x,y) (((x) > (y)) ? 1 : (((x) < (y)) ? -1 : 0))
# ifndef MTANNOTATIONLIST_H
# define MTANNOTATIONLIST_H
+typedef /*@only@*/ mtAnnotationDecl o_mtAnnotationDecl;
+
struct s_mtAnnotationList
{
int nelements;
int nspace;
- /*@reldef@*/ /*@relnull@*/ mtAnnotationDecl *elements;
+ /*@reldef@*/ /*@relnull@*/ o_mtAnnotationDecl *elements;
} ;
/*@constant null mtAnnotationList mtAnnotationList_undefined;@*/
extern /*@unused@*/ /*@only@*/ mtAnnotationList mtAnnotationList_new (void) /*@*/ ;
-extern /*@only@*/ mtAnnotationList mtAnnotationList_single (/*@keep@*/ mtAnnotationDecl p_el) /*@*/ ;
+extern /*@only@*/ mtAnnotationList mtAnnotationList_single (/*@only@*/ mtAnnotationDecl p_el) /*@*/ ;
extern mtAnnotationList
- mtAnnotationList_add (/*@returned@*/ mtAnnotationList p_s, /*@keep@*/ mtAnnotationDecl p_el)
+ mtAnnotationList_add (/*@returned@*/ mtAnnotationList p_s, /*@only@*/ mtAnnotationDecl p_el)
/*@modifies p_s@*/ ;
-extern mtAnnotationList
- mtAnnotationList_prepend (/*@returned@*/ mtAnnotationList p_s, /*@keep@*/ mtAnnotationDecl p_el)
+extern /*@only@*/ mtAnnotationList
+ mtAnnotationList_prepend (/*@only@*/ mtAnnotationList p_s, /*@only@*/ mtAnnotationDecl p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring mtAnnotationList_unparse (mtAnnotationList p_s) ;
/*@modifies p_s@*/ ;
extern mtDefaultsDeclList
- mtDefaultsDeclList_prepend (/*@returned@*/ mtDefaultsDeclList p_s, /*@keep@*/ mtDefaultsDecl p_el)
+ mtDefaultsDeclList_prepend (/*@only@*/ mtDefaultsDeclList p_s, /*@keep@*/ mtDefaultsDecl p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring
extern /*@unused@*/ /*@only@*/ mtLoseReferenceList mtLoseReferenceList_new (void) /*@*/ ;
-extern /*@only@*/ mtLoseReferenceList mtLoseReferenceList_single (/*@keep@*/ mtLoseReference p_el) /*@*/ ;
+extern /*@only@*/ mtLoseReferenceList mtLoseReferenceList_single (/*@only@*/ mtLoseReference p_el) /*@*/ ;
extern mtLoseReferenceList
- mtLoseReferenceList_add (/*@returned@*/ mtLoseReferenceList p_s, /*@keep@*/ mtLoseReference p_el)
+ mtLoseReferenceList_add (/*@only@*/ mtLoseReferenceList p_s, /*@only@*/ mtLoseReference p_el)
/*@modifies p_s@*/ ;
extern mtLoseReferenceList
- mtLoseReferenceList_prepend (/*@returned@*/ mtLoseReferenceList p_s, /*@keep@*/ mtLoseReference p_el)
+ mtLoseReferenceList_prepend (/*@only@*/ mtLoseReferenceList p_s, /*@only@*/ mtLoseReference p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring mtLoseReferenceList_unparse (mtLoseReferenceList p_s) ;
/*@modifies p_s@*/ ;
extern mtMergeClauseList
- mtMergeClauseList_prepend (/*@returned@*/ mtMergeClauseList p_s, /*@keep@*/ mtMergeClause p_el)
+ mtMergeClauseList_prepend (/*@only@*/ mtMergeClauseList p_s, /*@only@*/ mtMergeClause p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring mtMergeClauseList_unparse (mtMergeClauseList p_s) ;
extern /*@unused@*/ /*@only@*/ mtTransferClauseList mtTransferClauseList_new (void) /*@*/ ;
-extern /*@only@*/ mtTransferClauseList mtTransferClauseList_single (/*@keep@*/ mtTransferClause p_el) /*@*/ ;
+extern /*@only@*/ mtTransferClauseList mtTransferClauseList_single (/*@only@*/ mtTransferClause p_el) /*@*/ ;
extern mtTransferClauseList
- mtTransferClauseList_add (/*@returned@*/ mtTransferClauseList p_s, /*@keep@*/ mtTransferClause p_el)
+ mtTransferClauseList_add (/*@only@*/ mtTransferClauseList p_s, /*@only@*/ mtTransferClause p_el)
/*@modifies p_s@*/ ;
-extern mtTransferClauseList
- mtTransferClauseList_prepend (/*@returned@*/ mtTransferClauseList p_s, /*@keep@*/ mtTransferClause p_el)
+extern /*@only@*/ mtTransferClauseList
+ mtTransferClauseList_prepend (/*@only@*/ mtTransferClauseList p_s, /*@only@*/ mtTransferClause p_el)
/*@modifies p_s@*/ ;
extern /*@unused@*/ /*@only@*/ cstring mtTransferClauseList_unparse (mtTransferClauseList p_s) ;
extern cstring mtValuesNode_unparse (mtValuesNode p_node) /*@*/ ;
-/*@i32 why no warning without observer!??*/
extern /*@observer@*/ cstringList mtValuesNode_getValues (mtValuesNode p_node) /*@*/ ;
# define mtValuesNode_getValues(node) ((node)->values)
extern void checkPrefix (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
extern void checkAnsiName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
extern void checkParamNames (uentry p_ue) /*@modifies g_warningstream@*/;
-/*@i32! should get error without modifies p_ue@*/
# else
# error "Multiple include"
/*@notfunction@*/
# define NOALIAS(s,t) (/*@ignore@*/ (s == NULL) || (s != t) /*@end@*/)
-/*@i34@*/ /*fix this before release version*/
/* evans 2002-02-24: got rid of -formatconst */
/*@notfunction@*/
cstring msg;
} *stateEntry;
-/*@i23 typedef @only@ stateEntry o_stateEntry; */
+typedef /*@only@*/ stateEntry o_stateEntry;
typedef struct
{
int size;
- /*@only@*/ stateEntry *entries;
+ /*@only@*/ o_stateEntry *entries;
} *stateRow;
-# if 0
-this breaks comething? typedef /*@only@*/ stateRow o_stateRow; /*@i324*/
-# endif
+typedef /*@only@*/ stateRow o_stateRow;
abst_typedef struct
{
- int size;
- /*@only@*/ stateRow *rows;
+ int size;
+ /*@only@*/ o_stateRow *rows;
} *stateCombinationTable;
extern /*@only@*/ stateCombinationTable stateCombinationTable_create (int p_size);
extern int stateCombinationTable_lookup
(stateCombinationTable p_h, int p_from,
- int p_to, /*@out@*/ /*@observer@*/ cstring *p_msg);
+ int p_to, /*@out@*/ ob_cstring *p_msg);
extern int stateCombinationTable_lookupLoseReference
(stateCombinationTable p_h, int p_from,
--- /dev/null
+# ifndef TYPEID_H
+# define TYPEID_H
+
+typedef /*@numabstract@*/ usymId typeId;
+/*@access usymId@*/
+
+extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
+# define typeId_isInvalid(u) ((u) == typeId_invalid)
+
+extern bool typeId_isValid (typeId p_u) /*@*/ ;
+# define typeId_isValid(u) ((u) != typeId_invalid)
+
+extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
+# define typeId_equal(u1,u2) ((u1) == (u2))
+
+extern typeId typeId_fromInt (int p_i) /*@*/ ;
+# define typeId_fromInt(i) ((typeId) (i))
+
+extern typeId typeId_fromUsymId (usymId p_u) /*@*/ ;
+# define typeId_fromUsymId(u) ((typeId) (u))
+
+extern usymId typeId_toUsymId (typeId p_u) /*@*/ ;
+# define typeId_toUsymId(u) ((usymId) (u))
+
+extern int typeId_compare (/*@sef@*/ typeId p_x, /*@sef@*/ typeId p_y) /*@*/ ;
+# define typeId_compare(x,y) (int_compare(x, y))
+
+/*@constant typeId typeId_invalid;@*/
+# define typeId_invalid usymId_invalid
+
+/*@noaccess usymId@*/
+
+# else
+# error "Multiple include"
+# endif
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 /*@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@*/
/*@constant cstring GLOBAL_MARKER_NAME@*/
# define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
-/* functions for making modification to null-term info */
+/* Null Termination */
+
extern void uentry_setNullTerminatedState (uentry p_e);
extern void uentry_setPossiblyNullTerminatedState (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)
-
-/*@unused@*/ 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)
-
-/*@unused@*/ 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) /*@*/ ;
-/*@unused@*/ 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@*/
-
-/* end modifications */
+/* Global Markers */
extern uentry uentry_makeGlobalMarker (void) ;
extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
-extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
-
# ifdef DOANNOTS
typedef enum
{
extern cstring uentryList_unparseParams (uentryList p_s) /*@*/ ;
extern void uentryList_free (/*@only@*/ uentryList p_s) ;
+extern void uentryList_freeShallow (/*@only@*/ uentryList p_s) ;
extern bool uentryList_isVoid (uentryList p_cl) /*@*/ ;
extern /*@only@*/ uentryList uentryList_copy (uentryList p_s) /*@*/ ;
extern void uentryList_fixMissingNames (uentryList p_cl) /*@modifies p_cl@*/ ;
# ifndef USYMID_H
# define USYMID_H
-/*@i32 make them abstract/? */
-typedef int usymId;
-typedef usymId typeId;
+typedef /*@numabstract@*/ int usymId;
+
+extern usymId usymId_fromInt (int p_i) /*@*/ ;
+# define usymId_fromInt(i) ((usymId)(i))
+
+extern int usymId_toInt (usymId p_i) /*@*/ ;
+# define usymId_toInt(i) ((int)(i))
+
+extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
+# define usymId_isInvalid(u) ((u) == usymId_invalid)
+
+extern bool usymId_isValid (usymId p_u) /*@*/ ;
+# define usymId_isValid(u) ((u) != usymId_invalid)
extern bool usymId_equal (usymId p_u1, usymId p_u2) /*@*/ ;
# define usymId_equal(u1,u2) ((u1) == (u2))
-/*@constant usymId USYMIDINVALID;@*/
-# define USYMIDINVALID -17
+/*@constant usymId usymId_invalid;@*/
+# define usymId_invalid -17
-/*@constant typeId typeId_invalid;@*/
-# define typeId_invalid USYMIDINVALID
+/*@constant usymId usymId_notfound;@*/
+# define usymId_notfound NOT_FOUND
# else
# error "Multiple include"
# ifndef USYMIDSET_H
# define USYMIDSET_H
-# include "usymId.h"
-
abst_typedef /*@null@*/ struct
{
int entries;
/*@globals internalState@*/ ;
extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
-extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
+extern typeId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
extern void usymtab_supEntry (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
extern ctype usymtab_lookupAbstractType (cstring p_k)
/*@globals internalState@*/ /*@modifies nothing@*/ ;
-extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
+extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2)
/*@globals internalState@*/ ;
extern bool usymtab_existsEnumTag (cstring p_k)
extern bool usymtab_existsStructTag (cstring p_k)
/*@globals internalState@*/ ;
-extern usymId usymId_fromInt (int p_i) /*@*/ ;
-# define usymId_fromInt(i) ((usymId)(i))
-
-extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
-# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
-
-extern bool usymId_isValid (usymId p_u) /*@*/ ;
-# define usymId_isValid(u) ((u) != USYMIDINVALID)
-
-extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
-# define typeId_isInvalid(u) ((u) == typeId_invalid)
-
-extern bool typeId_isValid (typeId p_u) /*@*/ ;
-# define typeId_isValid(u) ((u) != typeId_invalid)
-
-extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
-# define typeId_equal(u1,u2) ((u1) == (u2))
-
-extern typeId typeId_fromInt (int p_i);
-# define typeId_fromInt(i) ((typeId)(i))
-
/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
# define usymtab_entries(x, m_i) \
{ int m_ind; \
/*@globals internalState@*/ ;
extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
+extern typeId usymtab_convertTypeId (typeId p_uid) /*@globals internalState@*/ ;
extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
extern void usymtab_destroyMod (void) /*@modifies internalState@*/ ;
extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
-extern int uentry_directParamNo (uentry p_ue)
+extern usymId usymtab_directParamNo (uentry p_ue)
/*@globals internalState@*/ ;
extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
Headers/letDeclNodeList.h Headers/typeNameNodeList.h \
Headers/lh.h Headers/typeNamePack.h \
Headers/limwr.h Headers/typeNode.h \
- Headers/llbasic.h Headers/uentry.h \
+ Headers/uentry.h \
Headers/llerror.h Headers/uentryList.h \
Headers/llglobals.h Headers/usymId.h \
Headers/llgrammar2.h Headers/usymIdSet.h \
- Headers/llgrammar_gen2.h Headers/usymtab-branch.h \
+ Headers/llgrammar_gen2.h \
Headers/llgrammar_gen.h Headers/usymtab.h \
Headers/llgrammar.h Headers/usymtab_interface.h \
Headers/llmain.h Headers/valueMatrix.h \
Headers/letDeclNodeList.h Headers/typeNameNodeList.h \
Headers/lh.h Headers/typeNamePack.h \
Headers/limwr.h Headers/typeNode.h \
- Headers/llbasic.h Headers/uentry.h \
+ Headers/uentry.h \
Headers/llerror.h Headers/uentryList.h \
Headers/llglobals.h Headers/usymId.h \
Headers/llgrammar2.h Headers/usymIdSet.h \
- Headers/llgrammar_gen2.h Headers/usymtab-branch.h \
+ Headers/llgrammar_gen2.h \
Headers/llgrammar_gen.h Headers/usymtab.h \
Headers/llgrammar.h Headers/usymtab_interface.h \
Headers/llmain.h Headers/valueMatrix.h \
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lslparse.h"
# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
# include "lclscan.h"
** in makeArrayNode.
*/
- /*@i3@*/ x->content.function.returntype = makeArrayNode (x, a);
- /*@i1@*/ return x;
+ /*@-usereleased@*/
+ x->content.function.returntype = makeArrayNode (x, a);
+ /*@=usereleased@*/
+ /*@-kepttrans@*/
+ return x;
+ /*@=kepttrans@*/
}
else
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "llgrammar.h"
# include "checking.h"
# include "lclscan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "cgrammar.h"
# include "usymtab_interface.h"
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 ()));
/*@-mustfree@*/
- /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
+ /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
# define constraintList_elements_private_only(x, m_el) \
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "usymtab_interface.h"
# include "exprChecks.h"
int counters[NUMVALUEFLAGS];
o_cstring strings[NUMSTRINGFLAGS];
- sRefSetList modrecs; /*@i32 ???? what is this for? */
+ sRefSetList modrecs; /* Keep track of file static symbols modified. */
metaStateTable stateTable; /* User-defined state information. */
annotationTable annotTable; /* User-defined annotations table. */
** These flags are true by default.
*/
- /*@i34 move this into flags.def */
+ /* eventually, move this into flags.def */
gc.flags[FLG_STREAMOVERWRITE] = TRUE;
-
gc.flags[FLG_OBVIOUSLOOPEXEC] = TRUE;
gc.flags[FLG_MODIFIES] = TRUE;
gc.flags[FLG_NESTCOMMENT] = TRUE;
gc.flags[FLG_FULLINITBLOCK] = TRUE;
gc.flags[FLG_INITSIZE] = TRUE;
gc.flags[FLG_INITALLELEMENTS] = TRUE;
+ gc.flags[FLG_NULLINIT] = TRUE;
gc.flags[FLG_STRINGLITTOOLONG] = TRUE;
{
FLG_BOOLINT, FLG_CHARINT, FLG_FLOATDOUBLE, FLG_LONGINT, FLG_SHORTINT,
FLG_ENUMINT, FLG_RELAXQUALS, FLG_FORWARDDECL,
- FLG_CHARINDEX, FLG_ABSTVOIDP, FLG_USEALLGLOBS,
+ FLG_CHARINDEX, FLG_NUMABSTRACTINDEX, FLG_ABSTVOIDP, FLG_USEALLGLOBS,
FLG_CHARUNSIGNEDCHAR,
FLG_PREDBOOLOTHERS,
FLG_NUMABSTRACTLIT,
FLG_SPECUNDEF, FLG_IMPCHECKMODINTERNALS,
FLG_DECLUNDEF, FLG_INCONDEFS, FLG_INCONDEFSLIB,
FLG_MISPLACEDSHAREQUAL, FLG_REDUNDANTSHAREQUAL,
+ FLG_NUMABSTRACTPRINT,
FLG_MATCHFIELDS,
FLG_MACROPARAMS,
FLG_MACROASSIGN,
FLG_MODFILESYSTEM,
FLG_MACROMATCHNAME,
FLG_FORMATCONST,
+ FLG_NUMABSTRACTPRINT,
FLG_STRINGLITNOROOM,
FLG_STRINGLITNOROOMFINALNULL,
FLG_STRINGLITSMALLER,
void context_exitClauseAux (exprNode pred, exprNode tbranch)
{
context_setJustPopped ();
- /*@i32 was makeAlt */
- usymtab_popTrueBranch (pred, tbranch, gc.inclause);
+ usymtab_popTrueBranch (pred, tbranch, gc.inclause); /* evans 2003-02-02?: was makeAlt */
clauseStack_pop (gc.clauses);
gc.inclause = topClause (gc.clauses);
}
{
; /* Okay not handle everything in this switch */
}
- /*@i523@*/ } /* evans 2002-03-24: splintme reports a spurious (I think) warning here...need to look into it */
-
+ /*@-branchstate@*/
+ } /* evans 2002-03-24: splintme reports a spurious (I think) warning here...need to look into it */
+ /*@=branchstate@*/
+
if (cstring_length (val) >= 1
&& cstring_firstChar (val) == '\"')
{
if (metaStateTable_size (gc.stateTable) > 0)
{
valueTable res = valueTable_create (metaStateTable_size (gc.stateTable));
- /*@i32 should use smaller value... */
+ /* should use smaller value... */
DPRINTF (("Value table for: %s", sRef_unparse (s)));
metaStateTable_elements (gc.stateTable, msname, msi)
if (metaStateTable_size (gc.stateTable) > 0)
{
valueTable res = valueTable_create (metaStateTable_size (gc.stateTable));
- /*@i32 should use smaller value... */
+ /* should use smaller value... */
metaStateTable_elements (gc.stateTable, msname, msi)
{
- /*@i23 only add global...*/
+ /* only add global...*/
DPRINTF (("Create: %s", metaStateInfo_unparse (msi)));
llassert (cstring_equal (msname, metaStateInfo_getName (msi)));
# define FATAL_EXIT_CODE EXIT_FAILURE
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "cpplib.h"
# include "cpperror.h"
# include <string.h>
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "cpplib.h"
# include "cpphash.h"
# include "cppexp.h"
if (overflow)
{
- /*@i23 add flags for all these...*/
cppReader_pedwarnLit
(pfile,
cstring_makeLiteralTemp ("Integer constant out of range"));
what you give them. Help stamp out software-hoarding! */
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include <string.h>
# include "cpplib.h"
# include "cpphash.h"
# include <errno.h>
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lcllib.h"
# include "cpplib.h"
# include "cpperror.h"
return FALSE;
}
-/* Return TRUE if two parts of two macro definitions are effectively different.
- One of the parts starts at BEG1 and has LEN1 chars;
- the other has LEN2 chars at BEG2.
- Any sequence of whitespace matches any other sequence of whitespace.
- FIRST means these parts are the first of a macro definition;
- so ignore leading whitespace entirely.
- LAST means these parts are the last of a macro definition;
- so ignore trailing whitespace entirely. */
- /*@i2@*/
+/*
+** Return TRUE if two parts of two macro definitions are effectively different.
+** One of the parts starts at BEG1 and has LEN1 chars;
+** the other has LEN2 chars at BEG2.
+** Any sequence of whitespace matches any other sequence of whitespace.
+** FIRST means these parts are the first of a macro definition;
+** so ignore leading whitespace entirely.
+** LAST means these parts are the last of a macro definition;
+** so ignore trailing whitespace entirely.
+*/
+
static bool
comp_def_part (bool first, char *beg1, int len1, char *beg2, int len2, bool last)
{
return (beg1 != end1) || (beg2 != end2);
}
-/* Process a #define command.
- BUF points to the contents of the #define command, as a contiguous string.
- LIMIT points to the first character past the end of the definition.
- KEYWORD is the keyword-table entry for #define,
- or NULL for a "predefined" macro. */
- /*@i2@*/
+/*
+** Process a #define command.
+** BUF points to the contents of the #define command, as a contiguous string.
+** LIMIT points to the first character past the end of the definition.
+** KEYWORD is the keyword-table entry for #define,
+** or NULL for a "predefined" macro.
+*/
+
static int
do_defineAux (cppReader *pfile, struct directive *keyword,
/*@exposed@*/ char *buf, char *limit, bool noExpand)
int hashcode;
macroDef mdef;
hashNode hp;
- /*@i2@*/
- DPRINTF (("Define aux: %d", noExpand));
- /*@i2@*/
+
mdef = create_definition (buf, limit, pfile, keyword == NULL, noExpand);
if (mdef.defn == 0)
goto nope;
- /*@i2@*/
+
hashcode = cpphash_hashCode (mdef.symnam, mdef.symlen, CPP_HASHSIZE);
- /*@i2@*/
- DPRINTF (("Macro: %s / %s",
- cstring_copyLength (mdef.symnam, mdef.symlen),
- bool_unparse (noExpand)));
- /*@i2@*/
+
if ((hp = cpphash_lookup (mdef.symnam, size_toInt (mdef.symlen), hashcode)) != NULL)
{
bool ok = FALSE;
else {
BADBRANCH;
}
- /*@i2@*/
+
/* Print the warning if it's not ok. */
if (!ok)
{
}
cpp_setLocation (pfile);
- /*@i2@*/
+
if (hp->type == T_MACRO)
{
if (hp->value.defn->noExpand)
message ("Macro %q already defined",
cstring_copyLength (mdef.symnam,
mdef.symlen)));
- /*@i2@*/
}
}
*/
hashNode hn;
- /*@i2@*/
+
if (CPPOPTIONS (pfile)->debug_output && (keyword != NULL))
{
pass_thru_directive (buf, limit, pfile, keyword);
} /*@=branchstate@*/
return 0;
- /*@i2@*/
+
nope:
- /*@i2@*/
return 1;
}
DPRINTF (("Regular do define"));
return do_defineAux (pfile, keyword, buf, limit, FALSE);
}
- /*@i2@*/
-/* This structure represents one parsed argument in a macro call.
- `raw' points to the argument text as written (`raw_length' is its length).
- `expanded' points to the argument's macro-expansion
- (its length is `expand_length').
- `stringified_length' is the length the argument would have
- if stringified.
- `use_count' is the number of times this macro arg is substituted
- into the macro. If the actual use count exceeds 10,
- the value stored is 10. */
- /*@i2@*/
+
+/*
+** This structure represents one parsed argument in a macro call.
+** `raw' points to the argument text as written (`raw_length' is its length).
+** `expanded' points to the argument's macro-expansion
+** (its length is `expand_length').
+** `stringified_length' is the length the argument would have
+** if stringified.
+** `use_count' is the number of times this macro arg is substituted
+** into the macro. If the actual use count exceeds 10,
+** the value stored is 10.
+*/
+
/* raw and expanded are relative to ARG_BASE */
/*@notfunction@*/
#define ARG_BASE ((pfile)->token_buffer)
- /*@i2@*/
+
struct argdata {
/* Strings relative to pfile->token_buffer */
long raw;
int use_count;
};
-/* Allocate a new cppBuffer for PFILE, and push it on the input buffer stack.
- If BUFFER != NULL, then use the LENGTH characters in BUFFER
- as the new input buffer.
- Return the new buffer, or NULL on failure. */
- /*@i2@*/
+/*
+** Allocate a new cppBuffer for PFILE, and push it on the input buffer stack.
+** If BUFFER != NULL, then use the LENGTH characters in BUFFER
+** as the new input buffer.
+** Return the new buffer, or NULL on failure.
+*/
+
/*@null@*/ /*@exposed@*/ cppBuffer *
cppReader_pushBuffer (cppReader *pfile, char *buffer, size_t length)
{
return buf;
}
- /*@i2@*/
+
cppBuffer *
cppReader_popBuffer (cppReader *pfile)
{
return ++CPPBUFFER (pfile);
}
-/* Scan until CPPBUFFER (PFILE) is exhausted into PFILE->token_buffer.
- Pop the buffer when done. */
- /*@i2@*/
+/*
+** Scan until CPPBUFFER (PFILE) is exhausted into PFILE->token_buffer.
+** Pop the buffer when done.
+*/
+
void
cppReader_scanBuffer (cppReader *pfile)
{
}
}
}
- /*@i2@*/
/*
* Rescan a string (which may have escape marks) into pfile's buffer.
}
else if (ap->raw_before || ap->raw_after || cppReader_isTraditional (pfile))
{
- /* Add 4 for two newline-space markers to prevent
- token concatenation. */
- assertSet (args); /*@i534 shouldn't need this */
+ /* Add 4 for two newline-space markers to prevent token concatenation. */
+ assertSet (args); /* Splint shouldn't need this */
xbuf_len += args[ap->argno].raw_length + 4;
}
else
/* We have an ordinary (expanded) occurrence of the arg.
So compute its expansion, if we have not already. */
- assertSet (args); /*@i534 shouldn't need this */
+ assertSet (args); /* shouldn't need this */
if (args[ap->argno].expand_length < 0)
{
if (f == IMPORT_FOUND)
{
- return 0; /* Already included this file */
+ return 0; /* Already included this file */
}
#ifdef EACCES
else if (f == IMPORT_NOT_FOUND && errno == EACCES)
nlist->got_name_map = 0;
nlist->next = NULL;
- /*@i2523@*/ if (opts->first_system_include == NULL)
+ /* Spurious warning reported for opts->first_system_include */
+ /*@-usereleased@*/ if (opts->first_system_include == NULL)
{
opts->first_system_include = nlist;
}
-
+ /*@=usereleased@*/
+
cppReader_addIncludeChain (pfile, nlist);
}
}
cppReader_appendIncludeChain (pfile, opts->after_include,
opts->last_after_include);
- /*@i523@*/ if (opts->first_system_include == NULL)
+ /* Spurious warnings for opts->first_system_include */
+ /*@-usereleased@*/
+ if (opts->first_system_include == NULL)
{
opts->first_system_include = opts->after_include;
}
-
+ /*@=usereleased@*/
+
/* With -v, print the list of dirs to search. */
if (opts->verbose) {
struct file_name_list *p;
what you give them. Help stamp out software-hoarding! */
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "cpplib.h"
# include "cpphash.h"
# include "cpperror.h"
}
else /* if (c == '@') */
{
- llassert (FALSE); /*@i23@*/
+ llassert (FALSE);
+
if (cscannerHelp_handleLlSpecial () != BADTOK)
{
llerrorlit (FLG_SYNTAX, "Macro cannot use special syntax");
s = mstring_append (s, c);
charsread++;
}
- /*@i888@*/ }
+ /*@-branchstate@*/
+ } /* spurious (?) warnings about s */
+ /*@=branchstate@*/
DPRINTF (("Read: %s / %s", s, fileloc_unparse (g_currentloc)));
if (annotationInfo_isDefined (ainfo)) {
DPRINTF (("Found annotation: %s", annotationInfo_unparse (ainfo)));
- /*@i324@*/ yylval.annotation = ainfo;
+ yylval.annotation = ainfo;
s_tokLength = 0;
sfree (os);
sfree (t);
message ("Semantic comment unrecognized: %s",
cstring_fromChars (os)),
loc);
- /*@i888@*/ }
+ /*@-branchstate@*/
+ } /* spurious (?) warning about t */
+ /*@=branchstate@*/
sfree (t);
}
if (annotationInfo_isDefined (ainfo))
{
DPRINTF (("Found annotation: %s", annotationInfo_unparse (ainfo)));
- /*@i324@*/ yylval.annotation = ainfo;
+ yylval.annotation = ainfo;
return CANNOTATION;
}
else
if (uentry_isIter (le))
{
- /*@i32@*/ yylval.entry = le;
+ yylval.entry = le;
return (ITER_NAME);
}
else if (uentry_isEndIter (le))
{
- /*@i32@*/ yylval.entry = le;
+ yylval.entry = le;
return (ITER_ENDNAME);
}
else if (uentry_isUndefined (le))
}
else
{
- /*@i32@*/ yylval.entry = le;
+ yylval.entry = le;
return (IDENTIFIER);
}
}
}
else
{
- /*@i32@*/ yylval.entry = le;
+ yylval.entry = le;
return (IDENTIFIER);
}
{
return (tok == QMAXSET || tok == QMAXREAD);
/* || tok == QMINREAD || tok == QMINSET */
- /*@i4523@*/
/* uncomment the additional if statement tests when minSet and minRead are supported */
}
return s->elements[index];
}
-ob_mstring *
+ob_cstring *
cstringList_getElements (cstringList s)
{
if (cstringList_isDefined (s))
{
- /*@i423@*/ return s->elements;
+ /*@-compmempass@*/
+ return s->elements;
+ /*@=compmempass@*/ /* This is exposed */
}
else
{
h->key = key;
h->val = val;
- llassert (val != HBUCKET_DNE); /*@i523 way bogus! */
-
+ llassert (val != HBUCKET_DNE);
return (h);
}
for (i = 0; i < h->size; i++)
{
- newentries[i] = h->entries[i];
+ newentries[i] = h->entries[i];
}
- /*@i32@*/ sfree (h->entries);
+ sfree (h->entries);
h->entries = newentries;
-/*@i23@*/ }
+ /*@-compmempass@*/
+} /*@=compmempass@*/ /* Spurious warnings reported - shouldn't need this */
static int hbucket_lookup (hbucket p_h, cstring p_key);
abst_typedef /*@null@*/ struct s_ctbase *ctbase;
/*@function static bool ctuid_isAnyUserType (sef ctuid p_cid) @*/
-/*@i888@*/
+
/*@-macrofcndecl@*/ /*@-macroparams@*/
# define ctuid_isAnyUserType(cid) \
((cid) == CT_ABST || (cid) == CT_USER || (cid) == CT_NUMABST)
case CT_PRIM:
return (message ("p%d|", c->contents.prim));
case CT_USER:
- return (message ("s%d|",
- usymtab_convertId (c->contents.tid)));
+ return (message ("s%d|", usymtab_convertTypeId (c->contents.tid)));
case CT_ABST:
- return (message ("a%d|", usymtab_convertId (c->contents.tid)));
+ return (message ("a%d|", usymtab_convertTypeId (c->contents.tid)));
case CT_NUMABST:
- return (message ("n%d|", usymtab_convertId (c->contents.tid)));
+ return (message ("n%d|", usymtab_convertTypeId (c->contents.tid)));
case CT_PTR:
return (message ("t%q|", ctype_dump (c->contents.base)));
case CT_ARRAY:
sfree (c);
break;
case CT_FCN:
- /*@i32@*/ /* uentryList_free (c->contents.fcn->params); */
+ /* Cannot free params: uentryList_free (c->contents.fcn->params); */
+ uentryList_freeShallow (c->contents.fcn->params);
sfree (c);
break;
case CT_STRUCT:
case CT_BOOL:
return 0;
case CT_USER:
- return (int_compare (c1->contents.tid, c2->contents.tid));
+ return (typeId_compare (c1->contents.tid, c2->contents.tid));
case CT_ENUMLIST:
return 1;
case CT_ENUM: /* for now, keep like abstract */
case CT_ABST:
case CT_NUMABST:
- return (int_compare (c1->contents.tid, c2->contents.tid));
+ return (typeId_compare (c1->contents.tid, c2->contents.tid));
case CT_PTR:
return (ctype_compare (c1->contents.base, c2->contents.base));
case CT_FIXEDARRAY:
ctb = ctype_getCtbase (i);
- /*@i32 is this optimization really worthwhile??? */
+ /* is this optimization really worthwhile? */
if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb))
{
if (ctype_isUA (c))
{
- cstring tname = usymtab_getTypeEntryName
- (usymtab_convertId (ctype_typeId (c)));
+ cstring tname = usymtab_getTypeEntryName (usymtab_convertTypeId (ctype_typeId (c)));
if (cstring_equal (tname, context_getBoolName ()))
{
bool ctype_isVisiblySharable (ctype t)
{
- if (ctype_isUnknown (t)) return TRUE;
+ if (ctype_isUnknown (t))
+ {
+ return TRUE;
+ }
if (ctype_isConj (t))
{
if (rt == t)
{
- return TRUE;
+ if (ctype_isNumAbstract (t))
+ {
+ return FALSE;
+ }
+ else
+ {
+ return TRUE;
+ }
}
else
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
declaratorInvNodeList
declaratorInvNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
declaratorNodeList
declaratorNodeList_new ()
else if (sRef_isAnyParam (base))
{
uentryList params = context_getParams ();
- int paramno = sRef_getParam (base);
+ int paramno = usymId_toInt (sRef_getParam (base));
if (paramno < uentryList_size (params))
{
uentry arg = uentryList_getN (params, paramno);
sRef ref = uentry_getSref (arg);
-
+
if (uentry_isReturned (arg)
|| sRef_isOnly (ref)
|| sRef_isExposed (ref)
else if (sRef_isAnyParam (base) && !(sRef_isOnly (base)))
{
uentryList params = context_getParams ();
- int paramno = sRef_getParam (base);
+ int paramno = usymId_toInt (sRef_getParam (base));
if (paramno < uentryList_size (params))
{
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 */
codetext, expecttype,
a->typ, exprNode_unparse (a)),
a->loc))
- {
+ {
if (fileloc_isDefined (formatloc)
&& context_getFlag (FLG_SHOWCOL))
{
if (sRef_isObserver (b))
{
- exprNode e = exprNodeList_nth (args, sRef_getParam (rb));
+ exprNode e = exprNodeList_nth (args, usymId_toInt (sRef_getParam (rb)));
if (optgenerror
(FLG_MODOBSERVER,
if (sRef_isResult (sRef_getRootBase (sel)))
{
- ; /*@i423 what do we do about results */
+ ; /* what do we do about results? */
}
else
{
*/
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);
/*
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 */
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
fcnNodeList
fcnNodeList_new ()
{
if (cstring_equalPrefixLit (s, "./"))
{
- return cstring_copySegment (s, 2, cstring_length (s) - 1);
+ cstring res = cstring_copySegment (s, 2, cstring_length (s) - 1);
+ cstring_free (s);
+ return res;
}
- return cstring_copy (s);
+ return s;
}
# include <sys/stat.h>
# include <fcntl.h>
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "llmain.h"
# include "portab.h"
cstring absname = osd_absolutePath (NULL, name);
int tindex = fileTable_getIndex (ft, absname);
- /*@i534 fprintf (stderr, "Got abs path: %s", absname); */
llassert (ft != fileTable_undefined);
if (tindex != NOT_FOUND)
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "portab.h"
{
res = cstring_makeLiteral ("< Location unknown >");
}
- /*@=branchstate@*/ /*@i2523 this is a spurious warning because of the break */
+ /*@=branchstate@*/ /* this is a spurious warning because of the break */
in_funparse = FALSE;
return res;
cstringSList_elements (fl, el)
{
- /*@i22@*/ /*find out why this is necessary*/
cstring tmp;
tmp = cstring_copy(el);
llmsg (message ("%q\n\n", describeFlag (tmp)));
"a possibly null pointer.",
0, 0
},
+ {
+ FK_NULL, FK_MEMORY, plainFlag,
+ "nullinit",
+ FLG_NULLINIT,
+ "inconsistent initialization involving null pointer",
+ "A reference with no null annotation is initialized "
+ "to NULL. Use /*@null@*/ to declare the reference as "
+ "a possibly null pointer.",
+ 0, 0
+ },
/*
** Undefined Values (Section 3)
"numabstractlit",
FLG_NUMABSTRACTLIT,
"numeric literal can used as numabstract type",
- "A numeric literal can be used as a numabstract type.",
+ "To allow a numeric literal to be used as a numabstract type, use +numabstractlit.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_TYPEEQ, modeFlag,
+ "numabstractindex",
+ FLG_NUMABSTRACTINDEX,
+ "a numabstract type can be used to index an array",
+ "To allow numabstract types to index arrays, use +numabstractindex.",
+ 0, 0
+ },
+ {
+ FK_ABSTRACT, FK_NONE, modeFlag,
+ "numabstractprint",
+ FLG_NUMABSTRACTPRINT,
+ "a numabstract value is printed using %d format code",
+ "A numabstract value is printed usind %d format code in a printf.",
0, 0
},
{
# include "splintMacros.nf"
# include "basic.h"
-static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause /*@i32 need special? @*/
+static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause
functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
{
functionClause res = (functionClause) dmalloc (sizeof (*res));
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ functionClause el)
if (!functionClauseList_isDefined (s))
{
- /*@i32@*/ return functionClauseList_single (el);
+ return functionClauseList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
-
- /*@i32@*/ return s;
+
+ return s;
}
cstring
else
{
llassert (FALSE);
- /*@i2523 fix this */
}
}
}
# include "splintMacros.nf"
# include "basic.h"
-static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint /*@i32 need special? @*/
+static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint
functionConstraint_alloc (functionConstraintKind kind) /*@defines result->kind@*/
{
functionConstraint res = (functionConstraint) dmalloc (sizeof (*res));
{
if (node->kind == FCT_CONJUNCT)
{
- /*@i223*/ /*make sure this is safe*/
+ /* make sure this is safe*/
return constraintList_addListFree (functionConstraint_getBufferConstraints (node->constraint.conjunct.op1),
functionConstraint_getBufferConstraints (node->constraint.conjunct.op2));
}
return (h);
}
+static void
+ghentry_free (/*@only@*/ ghentry ghe)
+{
+ cstring_free (ghe->key);
+ /* can't free val contents */
+ sfree (ghe->val);
+ sfree (ghe);
+}
+
static bool
ghbucket_isEmpty (ghbucket h)
{
h->size = 1;
h->nspace = GHBUCKET_BASESIZE - 1;
h->entries = (ghentry *) dmalloc (GHBUCKET_BASESIZE * sizeof (*h->entries));
- /*@i23@*/ h->entries[0] = e;
+ h->entries[0] = e;
return (h);
}
newentries[i] = h->entries[i];
}
- /*@i32@*/ sfree (h->entries);
+ sfree (h->entries);
h->entries = newentries;
-/*@i32@*/ }
+ /*@-compmempass@*/
+} /*@=compmempass*/ /* Spurious warnings reported for h->entries */
static /*@null@*/ /*@exposed@*/ void *ghbucket_lookup (ghbucket p_h, cstring p_key);
h->entries[h->size] = e;
h->size++;
h->nspace--;
-/*@i23@*/ }
+}
static int
ghbucket_ncollisions (ghbucket h)
{
if (!ghbucket_isNull (h))
{
- /*@i32@*/ sfree (h->entries);
+ int i;
+
+ for (i = 0; i < h->size; i++)
+ {
+ ghentry_free (h->entries[i]);
+ }
+
+ sfree (h->entries);
sfree (h);
}
}
}
static void
-genericTable_addEntry (/*@notnull@*/ genericTable h, /*@keep@*/ ghentry e)
+genericTable_addEntry (/*@notnull@*/ genericTable h, /*@only@*/ ghentry e)
{
unsigned int hindex = genericTable_hashValue (h, e->key);
/*
}
else
{
- /*@i23@*/ ghbucket_add (h->buckets[hindex], e);
- /*@i23@*/ }
+ ghbucket_add (h->buckets[hindex], e);
+ }
}
void
if (ghbucket_isNull (hb))
{
- /*@i23@*/ h->buckets[hindex] = ghbucket_single (e);
+ h->buckets[hindex] = ghbucket_single (e);
}
else
{
- ghbucket_add (hb, e);
- /*@i23@*/ }
-/*@i23@*/ }
+ ghbucket_add (hb, e);
+ }
+}
/*@null@*/ /*@exposed@*/ void *
genericTable_lookup (genericTable h, cstring key)
globalsClause res = (globalsClause) dmalloc (sizeof (*res));
res->globs = gl;
res->loc = fileloc_copy (lltok_getLoc (tok));
- /*@i423@*/ return res; /* releases doesn't seem to work right here... */
+ lltok_free (tok);
+ return res; /* releases doesn't seem to work right here... */
}
globSet globalsClause_getGlobs (globalsClause gclause)
{
if (gclause == NULL)
{
- return; /*@i435 shouldn't ever need this? */
+ return; /* shouldn't ever need this? */
}
globSet_free (gclause->globs);
llmsglit (" --- path used to find #include'd files");
llmsg (message
- ("systemdirs = %s (set by -systemdirs or environment variable %s)", /*@i413223@*/
+ ("systemdirs = %s (set by -systemdirs or environment variable %s)",
context_getString (FLG_SYSTEMDIRS),
INCLUDEPATH_VAR));
{
if (idDecl_isDefined (t))
{
- /*@i523 functionClauseList_free (t->clauses); */ /* evans 2002-01-03: splint catches this now! */
+ /* don't: functionClauseList_free (t->clauses); */ /* evans 2002-01-03: splint catches this now! */
qtype_free (t->typ);
cstring_free (t->id);
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ importNodeList
importNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */
# include "lclscan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ initDeclNodeList
initDeclNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "portab.h"
{
char *ps;
inputStream s = (inputStream) dmalloc (sizeof (*s));
- cstring oname;
s->name = name;
s->file = NULL;
/*@access cstring@*/
llassert (cstring_isDefined (s->name));
- /*@i534 clean this up...*/
ps = strrchr (s->name, CONNECTCHAR);
if (ps == NULL)
s->name = cstring_concatFree1 (s->name, suffix);
}
- oname = s->name;
s->name = fileLib_cleanName (s->name);
- /*@i523@*/ cstring_free (oname); /* evans 2002-07-12: why no error without this?! */
s->lineNo = 0;
s->charNo = 0;
s->stringSourceTail = NULL;
s->buffer[0] = '\0';
- /*@i523@*/ return s;
+ return s;
}
extern /*@only@*/ inputStream
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ interfaceNodeList
interfaceNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
typedef struct
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "gram.h"
# include "lclscan.h"
# include "scanline.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "version.h"
/*@-nullstate@*/
return TRUE;
/*@=nullstate@*/
- /*@i233@*/
+
/* evans 2002-03-02:
- the returned reference is possibly null,
- but this should not change the null state of the parameter
- investigate this warning
+ the returned reference is possibly null,
+ but this should not change the null state of the parameter
*/
}
}
cstring_free (xname);
/*@noaccess cstring@*/
- /*@-nullstate@*/ /*@i233@*/ /* same problem as above */
+ /*@-nullstate@*/ /* same problem as above */
return FALSE;
/*@=nullstate@*/
}
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@-redecl@*/ /* from llgrammar.y */
extern bool g_inTypeDef;
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "gram.h"
# include "lclscan.h"
# include "scanline.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lcltokentable.h"
static long unsigned MaxToken;
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ letDeclNodeList
letDeclNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "lh.h"
# include "llmain.h"
if (LhFile.f == NULL)
{
- /*@i25534 check this! does it report the right filename? */
lldiagmsg (message ("Cannot open lh file for output: %s", LhFile.name));
}
else
# include "splintMacros.nf"
# include <string.h>
# include <errno.h>
-# include "llbasic.h"
+# include "basic.h"
# include "llmain.h"
# include "cpperror.h"
# include "Headers/version.h" /* Visual C++ finds a different version.h on some path! */
{
if (!context_suppressFlagMsg (FLG_FORMATTYPE, fl))
{
- return llgentypeerroraux (srcFile, srcLine, FLG_FORMATTYPE, t1, e1, t2, e2, s, fl);
+ if (ctype_isInt (t1)
+ && ctype_isNumAbstract (t2))
+ {
+ if (!context_suppressFlagMsg (FLG_NUMABSTRACTPRINT, fl))
+ {
+ return llgentypeerroraux (srcFile, srcLine, FLG_NUMABSTRACTPRINT, t1, e1, t2, e2, s, fl);
+ }
+ else
+ {
+ return FALSE;
+ }
+ }
+ else
+ {
+ return llgentypeerroraux (srcFile, srcLine, FLG_FORMATTYPE, t1, e1, t2, e2, s, fl);
+ }
}
else
{
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lclscan.h"
# include "checking.h"
# include "lslparse.h"
%{
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lclscan.h"
# include "checking.h"
# include "lslparse.h"
# endif
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "help.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ lslOpList
lslOpList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "checking.h" /* for lslOp_equal */
static bool lslOpSet_member (lslOpSet p_s, lslOp p_el);
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "signature.h"
# include "signature2.h"
# include "scan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lclscan.h"
# include "signature.h"
# include "signature2.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ lsymbolList
lsymbolList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
lsymbolSet lsymbolSet_new ()
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "llgrammar.h"
# include "scanline.h"
# include "lclscanline.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@notnull@*/ /*@only@*/ ltokenList
ltokenList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "llmain.h"
/*@constant int MCEBASESIZE;@*/
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@constant int MAPPING_SIZE; @*/
# define MAPPING_SIZE 127
s->elements = newelements;
}
-mtAnnotationList mtAnnotationList_single (/*@keep@*/ mtAnnotationDecl el)
+mtAnnotationList mtAnnotationList_single (/*@only@*/ mtAnnotationDecl el)
{
mtAnnotationList s = mtAnnotationList_new ();
s = mtAnnotationList_add (s, el);
return s;
}
-mtAnnotationList mtAnnotationList_add (mtAnnotationList s, /*@keep@*/ mtAnnotationDecl el)
+mtAnnotationList mtAnnotationList_add (mtAnnotationList s, mtAnnotationDecl el)
{
if (!mtAnnotationList_isDefined (s))
{
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
-mtAnnotationList mtAnnotationList_prepend (mtAnnotationList s, /*@keep@*/ mtAnnotationDecl el)
+mtAnnotationList mtAnnotationList_prepend (mtAnnotationList s, mtAnnotationDecl el)
{
int i;
if (!mtAnnotationList_isDefined (s))
{
- /*@i32@*/ return mtAnnotationList_single (el);
+ return mtAnnotationList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
cstring
mvals = mtValuesNode_getValues (mtv);
}
- /*@-usedef@*/ /*@i34 splint should figure this out... */
+ /*@-usedef@*/ /* splint should figure this out... */
nvalues = cstringList_size (mvals);
/*@=usedef@*/
{
for (j = low2index; j <= high2index; j++)
{
- /*@i32 check for multiple definitions! */
+ /* Need to add checks for multiple definitions! */
if (mtTransferAction_isError (taction))
{
res->kind = kind;
res->node = node;
- /*@i32@*/ return res;
+ return res;
}
extern mtDeclarationPiece mtDeclarationPiece_createContext (mtContextNode node) /*@*/
message ("Metastate declaration has duplicate pieces: %q / %q",
mtDeclarationPiece_unparse (res),
mtDeclarationPiece_unparse (pieces->thisPiece)),
- g_currentloc); /*@i43 pieces's should have locs! */
+ g_currentloc);
}
else
{
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
mtDefaultsDeclList mtDefaultsDeclList_prepend (mtDefaultsDeclList s, /*@keep@*/ mtDefaultsDecl el)
if (!mtDefaultsDeclList_isDefined (s))
{
- /*@i32@*/ return mtDefaultsDeclList_single (el);
+ return mtDefaultsDeclList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
cstring
s->elements = newelements;
}
-mtLoseReferenceList mtLoseReferenceList_single (/*@keep@*/ mtLoseReference el)
+mtLoseReferenceList mtLoseReferenceList_single (mtLoseReference el)
{
mtLoseReferenceList s = mtLoseReferenceList_new ();
s = mtLoseReferenceList_add (s, el);
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
-mtLoseReferenceList mtLoseReferenceList_prepend (mtLoseReferenceList s, /*@keep@*/ mtLoseReference el)
+mtLoseReferenceList mtLoseReferenceList_prepend (mtLoseReferenceList s, mtLoseReference el)
{
int i;
if (!mtLoseReferenceList_isDefined (s))
{
- /*@i32@*/ return mtLoseReferenceList_single (el);
+ return mtLoseReferenceList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
cstring
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
mtMergeClauseList mtMergeClauseList_prepend (mtMergeClauseList s, /*@keep@*/ mtMergeClause el)
if (!mtMergeClauseList_isDefined (s))
{
- /*@i32@*/ return mtMergeClauseList_single (el);
+ return mtMergeClauseList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
cstring
s->elements = newelements;
}
-mtTransferClauseList mtTransferClauseList_single (/*@keep@*/ mtTransferClause el)
+mtTransferClauseList mtTransferClauseList_single (mtTransferClause el)
{
mtTransferClauseList s = mtTransferClauseList_new ();
s = mtTransferClauseList_add (s, el);
}
s->nspace--;
- /*@i32@*/ s->elements[s->nelements] = el;
+ s->elements[s->nelements] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
-mtTransferClauseList mtTransferClauseList_prepend (mtTransferClauseList s, /*@keep@*/ mtTransferClause el)
+mtTransferClauseList mtTransferClauseList_prepend (mtTransferClauseList s, mtTransferClause el)
{
int i;
if (!mtTransferClauseList_isDefined (s))
{
- /*@i32@*/ return mtTransferClauseList_single (el);
+ return mtTransferClauseList_single (el);
}
if (s->nspace <= 0)
s->elements[i] = s->elements [i - 1];
}
- /*@i32@*/ s->elements[0] = el;
+ s->elements[0] = el;
s->nelements++;
- /*@i32@*/ return s;
+ return s;
}
cstring
# include "bison.reset"
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# ifndef S_SPLINT_S
extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ;
# include "bison.reset"
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# ifndef S_SPLINT_S
extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ;
# include "bison.reset"
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# ifndef S_SPLINT_S
extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ;
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "mtgrammar.h"
# include "mtscanner.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "mtgrammar.h"
# include "mtscanner.h"
** No file scope checks (yet)
*/
- /*@i423 add a file scope naming convention policy? */
+ /* add a file scope naming convention policy? */
return;
}
}
}
-/*@i523 POSIX p. 527 - applications should not declare any symbols that end _MAX @*/
+/* not yet checked: POSIX p. 527 - applications should not declare any symbols that end _MAX */
cstring osd_outputPath (cstring filename)
{
- /*@i2534 fix this junky code once and for all! */
# if defined (UNIX) || defined (OS2)
char *rel_buffer;
char *rel_buf_p;
}
else
{
- /*@i324 ! splint didn't report an errors for: return ++path_p; */
cstring_free (rel_buffer);
return cstring_fromCharsNew (path_p + 1);
}
while ((*rel_buf_p++ = *path_p++) != '\0') ;
- /*@=usereleased@*/ /*@i523! shouldn't need these */
+ /*@=usereleased@*/ /* Splint limitation: shouldn't need these */
--rel_buf_p;
if (osd_isConnectChar (*(rel_buf_p-1)))
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ pairNodeList
pairNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ paramNodeList
paramNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ programNodeList
programNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ quantifierNodeList
quantifierNodeList_new ()
fileIdList_undefined,
passThroughArgs,
cstringList_size (args),
- cstringList_getElements (args));
+ /*@-nullstate@*/ /*@-type@*/ /* exposes cstring type */
+ cstringList_getElements (args)
+ /*@=nullstate@*/ /*@=type@*/
+ );
cstringList_free (args);
check (fileTable_closeFile (context_fileTable (), rcfile));
}
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ replaceNodeList
replaceNodeList_new ()
case SK_PARAM:
llassert (s->info->paramno >= -1);
- llassert (s->info->paramno <= 50); /*@i32 bogus...*/
+ llassert (s->info->paramno <= 999); /* sanity check */
break;
case SK_ARRAYFETCH:
/* start modifications */
s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
- s->bufinfo.size = -1; /*@i24 unknown@*/
- s->bufinfo.len = -1; /*@i24 unknown@*/
+ s->bufinfo.size = -1;
+ s->bufinfo.len = -1;
/* end modifications */
s->aliaskind = AK_UNKNOWN;
switch (base->kind)
{
case SK_PARAM:
- res = usymtab_getRefQuiet (paramsScope, base->info->paramno);
+ res = usymtab_getRefQuiet (paramsScope, usymId_fromInt (base->info->paramno));
break;
case SK_CVAR:
switch (s->kind)
{
case SK_PARAM:
- return (usymtab_getRefQuiet (paramsScope, s->info->paramno));
+ return (usymtab_getRefQuiet (paramsScope, usymId_fromInt (s->info->paramno)));
case SK_CVAR:
return (usymtab_getRefQuiet (s->info->cvar->lexlevel, s->info->cvar->index));
case SK_CONJ:
}
}
-int
+usymId
sRef_getParam (sRef s)
{
llassert (sRef_isReasonable (s));
llassert (s->kind == SK_PARAM);
- return s->info->paramno;
+ return usymId_fromInt (s->info->paramno);
}
bool
return ce;
}
case SK_PARAM:
- llassert(exprNodeList_size (args) > s->info->paramno);
- {
- exprNode e = exprNodeList_nth (args, s->info->paramno);
-
- llassert( !(exprNode_isError (e)) );
- ce = constraintExpr_makeExprNode (e);
- return ce;
- }
+ {
+ exprNode e;
+ llassert (exprNodeList_size (args) > s->info->paramno);
+ e = exprNodeList_nth (args, s->info->paramno);
+
+ llassert (!(exprNode_isError (e)));
+ ce = constraintExpr_makeExprNode (e);
+ return ce;
+ }
default:
{
sRef
sRef_makeObject (ctype o)
{
- sRef s = sRef_newRef (); /*@i423 same line is bad...@*/
+ sRef s = sRef_newRef ();
s->kind = SK_OBJECT;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->kind = SK_EXTERNAL;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->type = t->type;
- s->info->ref = t; /* sRef_copy (t); */ /*@i32 was exposed@*/
+ s->info->ref = t;
llassert (valueTable_isUndefined (s->state));
s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_DECLARED));
return s;
s->kind = SK_DERIVED;
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->ref = t; /* sRef_copy (t); */ /*@i32@*/
+ s->info->ref = t;
s->type = t->type;
llassert (valueTable_isUndefined (s->state));
** Merge value table states
*/
-
- /*@i3245@*/
# if 0
/*
** This doesn't do anything. And its broken too...
s->kind = SK_CONJ;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->conj = (cjinfo) dmalloc (sizeof (*s->info->conj));
- s->info->conj->a = a; /* sRef_copy (a) */ /*@i32*/ ;
- s->info->conj->b = b; /* sRef_copy (b);*/ /*@i32@*/ ;
+ s->info->conj->a = a;
+ s->info->conj->b = b;
if (ctype_equal (a->type, b->type)) s->type = a->type;
else s->type = ctype_makeConj (a->type, b->type);
return ((s->kind == SK_CVAR) &&
(s->info->cvar->lexlevel == functionScope) &&
(context_inFunction () &&
- (s->info->cvar->index <= uentryList_size (context_getParams ()))));
+ (s->info->cvar->index <= usymId_fromInt (uentryList_size (context_getParams ())))));
}
bool sRef_isPointer (sRef s)
s->definfo = stateInfo_undefined;
s->nullinfo = stateInfo_undefined;
- /*@i32@*/ sfree (s);
+ sfree (s);
}
}
s->kind = SK_FIELD;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->field = (fldinfo) dmalloc (sizeof (*s->info->field));
- s->info->field->rec = rec; /* sRef_copy (rec); */ /*@i32@*/
+ s->info->field->rec = rec;
s->info->field->field = f; /* doesn't copy f */
if (ctype_isKnown (ct) && ctype_isSU (ct))
s->info->arrayfetch = (ainfo) dmalloc (sizeof (*s->info->arrayfetch));
s->info->arrayfetch->indknown = FALSE;
s->info->arrayfetch->ind = 0;
- s->info->arrayfetch->arr = arr; /* sRef_copy (arr); */ /*@i32@*/
+ s->info->arrayfetch->arr = arr;
sRef_setArrayFetchState (s, arr);
s->kind = SK_ARRAYFETCH;
s->info = (sinfo) dmalloc (sizeof (*s->info));
s->info->arrayfetch = (ainfo) dmalloc (sizeof (*s->info->arrayfetch));
- s->info->arrayfetch->arr = arr; /* sRef_copy (arr); */ /*@i32@*/
+ s->info->arrayfetch->arr = arr;
s->info->arrayfetch->indknown = TRUE;
s->info->arrayfetch->ind = i;
s->kind = SK_PTR;
s->info = (sinfo) dmalloc (sizeof (*s->info));
- s->info->ref = t; /* sRef_copy (t); */ /*@i32*/
+ s->info->ref = t;
if (ctype_isRealAP (rt))
{
s1->nullstate = s2->nullstate;
s1->nullinfo = stateInfo_update (s1->nullinfo, s2->nullinfo);
- /*@-mustfree@*/
- /*@i834 don't free it: valueTable_free (s1->state); */
- /*@i32@*/ s1->state = valueTable_copy (s2->state);
- /*@=mustfree@*/
+ valueTable_free (s1->state);
+ s1->state = valueTable_copy (s2->state);
s1->safe = s2->safe;
}
}
ret->arrayfetch = (ainfo) dmalloc (sizeof (*ret->arrayfetch));
ret->arrayfetch->indknown = s->info->arrayfetch->indknown;
ret->arrayfetch->ind = s->info->arrayfetch->ind;
- ret->arrayfetch->arr = s->info->arrayfetch->arr; /* sRef_copy (s->info->arrayfetch->arr); */ /*@i32@*/
+ ret->arrayfetch->arr = s->info->arrayfetch->arr;
break;
case SK_FIELD:
ret = (sinfo) dmalloc (sizeof (*ret));
ret->field = (fldinfo) dmalloc (sizeof (*ret->field));
- ret->field->rec = s->info->field->rec; /* sRef_copy (s->info->field->rec); */ /*@i32@*/
+ ret->field->rec = s->info->field->rec;
ret->field->field = s->info->field->field;
break;
case SK_PTR:
case SK_ADR:
case SK_DERIVED:
- case SK_EXTERNAL: /*@i32 is copy now! */
+ case SK_EXTERNAL: /* is copy now! */
break;
case SK_CONJ:
** Default defined state can be made special.
*/
- llassert (sRef_isReasonable (s)); /*@i523 why doesn't null-checking work!??? */
+ llassert (sRef_isReasonable (s));
if (s->defstate == SS_UNKNOWN || s->defstate == SS_DEFINED || s->defstate == SS_SPECIAL)
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "signature.h"
# include "signature2.h"
# include "scan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "signature.h"
# include "signature2.h"
# include "scan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "shift.h"
/*@constant static int SHIFTMAX=200;@*/
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "intSet.h"
static bool sigNodeSet_member (sigNodeSet p_s, sigNode p_el);
# include <stdio.h>
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lslparse.h"
# include "signature.h"
# include <stdio.h>
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "lslparse.h"
# include "signature.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "llgrammar.h"
# include "lclscan.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ sortList
sortList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
sortSet sortSet_new ()
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ sortSetList
sortSetList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ stDeclNodeList
stDeclNodeList_new ()
}
else if (qual_isAliasQual (sq))
{
- return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
+ return (sRefModVal) sRef_setAliasKind;
}
else
{
llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
sq = cl->squal;
-
- /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
- /*@+enumint@*/
+
+ /*@+enumint@*/
+ /*
+ ** Since this can be many different types of state kinds, we need to allow all
+ ** enum's to be returned as int.
+ */
if (qual_isNotNull (sq))
{
if (stateClause_isGlobal (cl))
{
- /*@i232@*/
+ ;
}
else
{
{
voptgenerror
(FLG_ANNOTATIONERROR,
- /*@-sefparams@*/ /* This is okay because its fresh storage. */ /*@i32@*/
+ /*@-sefparams@*/ /* This is okay because its fresh storage. */
message
("%q clauses includes %q of "
"non-dynamically allocated type %s",
{
if (stateClause_isGlobal (cl))
{
- ; /*@i32@*/
+ ; /* Don't handle globals for now */
}
else
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*
** (key, value, value) => value
s->value = i;
llassert (cstring_isUndefined (s->msg));
- /*@-usedef@*/ /*@i534 why necessary? */
+ /*@-usedef@*/
res->rows[i]->entries[j] = s;
/*@=usedef@*/
}
}
- /*@i32@*/ return res;
+ /*@-compmempass@*/ /*@-compdef@*/
+ return res;
+ /*@=compmempass@*/ /*@=compdef@*/
}
cstring stateCombinationTable_unparse (stateCombinationTable t)
{
int i;
- for (i = 0; i < r->size + 1; i++) {
- /*@i32@*/ stateEntry_free (r->entries[i]);
- }
+ for (i = 0; i < r->size + 1; i++)
+ {
+ stateEntry_free (r->entries[i]);
+ }
sfree (r->entries);
sfree (r);
int i;
for (i = 0; i < t->size; i++) {
- /*@i32@*/ stateRow_free (t->rows[i]);
+ stateRow_free (t->rows[i]);
}
sfree (t->rows);
p_from, p_to, cstring_toCharsSafe (msg)));
}
-int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, /*@out@*/ cstring *msg)
+int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, /*@out@*/ ob_cstring *msg)
{
stateEntry entry;
llassert (p_from != stateValue_error);
entry = stateCombintationTable_getEntry (h, p_from, p_to);
llassert (entry != NULL);
- DPRINTF (("Lookup: %d / %d => %s [%p]",
- p_from, p_to, cstring_toCharsSafe (entry->msg), entry));
-
- /*@i32@*/ *msg = entry->msg;
+ *msg = entry->msg;
return entry->value;
}
if (!fileloc_lessthan (sinfo->loc, snext->loc))
{
- /*@i888@*/ sinfo->previous = sfirst;
+ /*@i2@*/ sinfo->previous = sfirst; /* spurious? */
DPRINTF (("Sorted ==> %s", stateInfo_unparse (sinfo)));
- /*@i888@*/ return sinfo;
+ /*@i2@*/ return sinfo; /* spurious? */
}
else
{
snext->loc = sinfo->loc;
snext->action = sinfo->action;
- /*@i888@*/ snext->ref = sinfo->ref;
+ /*@-modobserver@*/
+ snext->ref = sinfo->ref; /* Doesn't actually modifie sfirst */
+ /*@=modobserver@*/
sinfo->loc = tloc;
sinfo->action = taction;
sinfo->ref = tref;
- /*@i888@*/ sinfo->previous = snext->previous;
+ /*@-mustfreeonly@*/
+ sinfo->previous = snext->previous;
+ /*@=mustfreeonly@*/
snext = snext->previous;
DPRINTF (("in while: sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
}
DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
- /*@i888@*/ return sfirst;
+ /*@-compmempass@*/
+ return sfirst;
+ /*@=compmempass@*/
}
}
}
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
extern
/*@notnull@*/ stateValue stateValue_create (int value, stateInfo info) {
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ storeRefNodeList
storeRefNodeList_new ()
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "gram.h"
# include "lclscan.h"
# include "lclsyntable.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
termNodeList termNodeList_new ()
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "osd.h"
# include "tokentable.h"
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
/*@only@*/ traitRefNodeList
traitRefNodeList_new ()
{
if (stateClause_isGlobal (cl))
{
- ; /*@i32@*/
+ ;
}
else if (stateClause_setsMetaState (cl))
{
exprNode_loc (fexp)))
{
sRef_showAliasInfo (sr);
- /*@i32@*/
}
}
}
if (sRef_isNotNull (tref))
{
if (optgenerror
- (FLG_SYNTAX, /*@i432 kuldge flag... */
+ (FLG_NULLINIT, /* kuldge flag... */
message ("%s %q initialized to %s value: %q",
sRef_getScopeName (tref),
sRef_unparse (tref),
static void
checkMetaStateTransfer (exprNode fexp, sRef fref, exprNode texp, sRef tref,
exprNode fcn,
- fileloc loc, transferKind /*@i32@*/ transferType)
+ fileloc loc, transferKind transferType)
{
valueTable fvalues = sRef_getValueTable (fref);
valueTable tvalues = sRef_getValueTable (tref);
{
if (nval == stateValue_error)
{
- /*@i32 print extra info for assignments@*/
-
if (optgenerror
(FLG_STATETRANSFER,
message
tistable_addDirectEntry (u);
s = reader_readLine (fin, os, MAX_DUMP_LINE_LENGTH);
}
-
- /*@i32 free os? @*/
}
static void tistable_grow (void)
bool typeIdSet_member (typeIdSet t, typeId el)
{
usymIdSet u = tistable_fetch (t);
-
- return usymIdSet_member (u, el);
+ return usymIdSet_member (u, typeId_toUsymId (el));
}
bool typeIdSet_isEmpty (typeIdSet t)
typeIdSet typeIdSet_single (typeId t)
{
- return (tistable_addEntry (usymIdSet_single (t)));
+ return (tistable_addEntry (usymIdSet_single (typeId_toUsymId (t))));
}
typeIdSet typeIdSet_singleOpt (typeId t)
{
if (typeId_isValid (t))
{
- return (tistable_addEntry (usymIdSet_single (t)));
+ return (tistable_addEntry (usymIdSet_single (typeId_toUsymId (t))));
}
else
{
{
usymIdSet u = tistable_fetch (t);
- if (usymIdSet_member (u, el))
+ if (usymIdSet_member (u, typeId_toUsymId (el)))
{
return t;
}
else
{
- return (tistable_addEntry (usymIdSet_add (u, el)));
+ return (tistable_addEntry (usymIdSet_add (u, typeId_toUsymId (el))));
}
}
typeIdSet typeIdSet_removeFresh (typeIdSet t, typeId el)
{
- return (tistable_addEntry (usymIdSet_removeFresh (tistable_fetch (t), el)));
+ return (tistable_addEntry (usymIdSet_removeFresh (tistable_fetch (t), typeId_toUsymId (el))));
}
cstring typeIdSet_unparse (typeIdSet t)
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
typeNameNodeList typeNameNodeList_new ()
{
static /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/
{
uentry ue = (uentry) dmalloc (sizeof (*ue));
- ue->warn = warnClause_undefined; /*@i32@*/
+ ue->warn = warnClause_undefined;
nuentries++;
totuentries++;
}
else
{
- if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype)))
+ if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype))
+ || ctype_isNumAbstract (ctype_getReturnType (ue->utype)))
{
; /* Immutable objects are not shared. */
}
uentry e = uentry_alloc ();
ctype ret;
- llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
-
- DPRINTF (("Make function: %s", n));
+ llassert (warnClause_isUndefined (warn));
if (ctype_isFunction (t))
{
**
*/
- uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); /*@i32@*/
+ uentry_combineModifies (ue, modifiesClause_takeMods (mlc));
}
else
{
static /*@only@*/ /*@notnull@*/ uentry
uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s,
- /*@only@*/ fileloc loc, sstate defstate) /*@i32 exposed*/
+ /*@only@*/ fileloc loc, sstate defstate)
{
cstring pname = makeParam (n);
uentry e;
if (uentry_isVariable (ue))
{
-
- /*@i634 ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
+ /* removed this: no need to copy? ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
sRef_setDefState (sr, ue->info->var->defstate, fileloc_undefined);
sRef_setNullState (sr, ue->info->var->nullstate, fileloc_undefined);
}
{
/*
** Okay to allow multiple clauses of the same kind.
- */ /*@i834 is this true?@*/
+ */
ue->info->fcn->specclauses =
stateClauseList_add (ue->info->fcn->specclauses, sc);
e->utype = t;
e->storageclass = SCNONE;
- e->warn = warnClause_undefined; /*@i32 warnings for constants? */
+ e->warn = warnClause_undefined; /* Don't support warnings for constants */
e->sref = sRef_makeConst (t);
e->storageclass = SCNONE;
- e->warn = warnClause_undefined; /*@i32 warnings for variable @*/
+ e->warn = warnClause_undefined; /* Don't support warnings for variables yet @*/
e->sref = s;
e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
e->info->var->kind = kind;
- /*@i523 e->info->var->origsref = sRef_saveCopy (e->sref); */
+ /* removed: e->info->var->origsref = sRef_saveCopy (e->sref); */
e->info->var->checked = CH_UNKNOWN;
DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref)));
if (ctype_isArray (t) || ctype_isPointer(t))
{
- /*@i222@*/ e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
+ e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
sRef_setNotNullTerminatedState (s);
}
/*@only@*/ warnClause warn,
fileloc f)
{
- llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
+ llassert (warnClause_isUndefined (warn));
return (uentry_makeFunctionAux (n, t,
((typeId_isInvalid (access)) ? typeIdSet_emptySet ()
: typeIdSet_single (access)),
uentry_setSpecDef (e, f);
- e->warn = warnClause_undefined; /*@i634@*/
+ e->warn = warnClause_undefined;
e->uses = filelocList_new ();
e->isPrivate = priv;
e->hasNameError = FALSE;
uentry_setSpecDef (e, f);
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->uses = filelocList_new ();
e->isPrivate = FALSE;
e->hasNameError = FALSE;
e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
e->info->enditer->access = access;
+ e->warn = warnClause_undefined;
- e->warn = warnClause_undefined; /*@i452@*/
return (e);
}
e->info->datatype->abs = qual_createUnknown ();
e->info->datatype->mut = (kind == KENUMTAG) ? NO : MAYBE;
e->info->datatype->type = t;
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
if (uentry_isDeclared (e))
{
e->used = FALSE;
e->lset = FALSE;
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
e->info->uconst->access = access;
- e->info->uconst->macro = FALSE; /*@i523! fix this when macro info added to library */
+ e->info->uconst->macro = FALSE; /* fix this when macro info added to library */
uentry_setConstantValue (e, m);
sRef_storeState (e->sref);
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
e->isPrivate = FALSE;
e->hasNameError = FALSE;
-
- e->warn = warnClause_undefined; /*@i452@*/
-
+ e->warn = warnClause_undefined;
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->datatype = (udinfo) dmalloc (sizeof (*e->info->datatype));
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->iter = (uiinfo) dmalloc (sizeof (*e->info->iter));
e->used = FALSE;
e->lset = FALSE;
e->uses = filelocList_new ();
- e->warn = warnClause_undefined; /*@i452@*/
+ e->warn = warnClause_undefined;
e->info = (uinfo) dmalloc (sizeof (*e->info));
e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
bool
uentry_isMutableDatatype (uentry e)
{
- bool res = uentry_isDatatype (e)
- && (ynm_toBoolRelaxed (e->info->datatype->mut));
-
- return res;
+ if (uentry_isDatatype (e))
+ {
+ if (ctype_isNumAbstract (e->info->datatype->type))
+ {
+ return FALSE;
+ }
+ else
+ {
+ return ynm_toBoolRelaxed (e->info->datatype->mut);
+ }
+ }
+
+ return FALSE;
}
bool
sRef uentry_getOrigSref (uentry e)
{
- /*@i523*/ /* evans 2001-09-09 - need to fix this
+ /* evans 2003-04-12 - removed for now */
+ /* evans 2001-09-09 - need to fix this
if (uentry_isValid (e))
{
if (uentry_isVariable (e))
ctype uentry_getRealType (uentry e)
{
ctype ct;
- typeId uid = USYMIDINVALID;
+ typeId uid = typeId_invalid;
if (uentry_isInvalid (e))
{
if (ctype_isUA (ct))
{
- usymId iid = ctype_typeId (ct);
+ typeId iid = ctype_typeId (ct);
- if (usymId_equal (iid, uid))
+ if (typeId_equal (iid, uid))
{
llcontbug (message ("uentry_getRealType: recursive type! %s",
ctype_unparse (ct)));
ctype uentry_getForceRealType (uentry e)
{
ctype ct;
- typeId uid = USYMIDINVALID;
+ typeId uid = typeId_invalid;
if (uentry_isInvalid (e))
{
if (ctype_isUA (ct))
{
- usymId iid = ctype_typeId (ct);
+ typeId iid = ctype_typeId (ct);
- if (usymId_equal (iid, uid))
+ if (typeId_equal (iid, uid))
{
llcontbug (message ("uentry_getRealType: recursive type! %s",
ctype_unparse (ct)));
}
void
-uentry_setDatatype (uentry e, usymId uid)
+uentry_setDatatype (uentry e, typeId uid)
{
llassert (uentry_isDatatype (e));
}
*/
- /*@i23 need checking @*/
-
+ /* need to add some checking @*/
old->info->fcn->specclauses = unew->info->fcn->specclauses;
}
else
{
- /*@i43 should be able to append? @*/
+ /* should be able to append? */
stateClauseList_checkEqual (old, unew);
stateClauseList_free (unew->info->fcn->specclauses);
/*@-branchstate@*/
}
}
- /*@=branchstate@*/ /*@i23 shouldn't need this@*/
+ /*@=branchstate@*/ /* shouldn't need this */
if (fileloc_isUndefined (old->whereDeclared))
{
{
/* no change */
}
-/*@i523 @*/ }
+ /*@-compmempass@*/
+} /*@=compmempass@*/ /* I think this is a spurious warning */
void
uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m)
}
else
{
- fileloc_free (unew->whereSpecified); /*@i523 why no error without this? */
+ fileloc_free (unew->whereSpecified);
unew->whereSpecified = fileloc_copy (old->whereSpecified);
}
}
else
{
- fileloc_free (unew->whereDefined); /*@i523 why no error without this? */
+ fileloc_free (unew->whereDefined);
unew->whereDefined = fileloc_copy (old->whereDefined);
}
}
else
{
- fileloc_free (unew->whereDeclared); /*@i523 why no error without this? */
+ fileloc_free (unew->whereDeclared);
unew->whereDeclared = fileloc_copy (old->whereDeclared);
}
if (nval == stateValue_error)
{
- /*@i32 print extra info for assignments@*/
-
if (uentry_isGlobalMarker (res))
{
if (optgenerror
if (uentry_isValid (e))
{
- int dp;
-
if (warnClause_isDefined (e->warn))
{
flagSpec flg = warnClause_getFlag (e->warn);
}
}
- if ((dp = uentry_directParamNo (e)) >= 0)
+ if (usymId_isValid (usymtab_directParamNo (e)))
{
- uentry_setUsed (usymtab_getParam (dp), loc);
+ uentry_setUsed (usymtab_getParam (usymId_toInt (usymtab_directParamNo (e))), loc);
}
e->used = TRUE;
|| u->info->var->kind == VKSEFRETPARAM));
}
-/*@i52323@*/
-# if 0
-/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
-{
- llassert (uentry_isRealFunction (u));
-
- if (ctype_isFunction (u->utype) && sRef_isStateSpecial (uentry_getSref (u)))
- {
- stateClauseList clauses = uentry_getStateClauseList (u);
- sRef res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
-
- DPRINTF (("Returned: %s", sRef_unparseFull (res)));
- sRef_setAllocated (res, g_currentloc);
-
- DPRINTF (("ensures clause: %s / %s", uentry_unparse (u),
- stateClauseList_unparse (clauses)));
-
- /*
- ** This should be in exprNode_reflectEnsuresClause
- */
-
- stateClauseList_postElements (clauses, cl)
- {
- if (!stateClause_isGlobal (cl))
- {
- sRefSet refs = stateClause_getRefs (cl);
- sRefMod modf = stateClause_getEffectFunction (cl);
-
- sRefSet_elements (refs, el)
- {
- sRef base = sRef_getRootBase (el);
-
- if (sRef_isResult (base))
- {
- if (modf != NULL)
- {
- sRef sr = sRef_fixBase (el, res);
- modf (sr, g_currentloc);
- }
- }
- else
- {
- ;
- }
- } end_sRefSet_elements ;
- }
- } end_stateClauseList_postElements ;
-
- return res;
- }
- else
- {
- uentryList params;
- alkind ak;
- sRefSet prefs = sRefSet_new ();
- sRef res = sRef_undefined;
- sRef tcref = sRef_undefined;
- sRef tref = sRef_undefined;
- int paramno = 0;
-
- params = uentry_getParams (u);
-
- /*
- ** Setting up aliases has to happen *after* setting null state!
- */
-
- uentryList_elements (params, current)
- {
- if (uentry_isReturned (current))
- {
- if (exprNodeList_size (args) >= paramno)
- {
- exprNode ecur = exprNodeList_nth (args, paramno);
- tref = exprNode_getSref (ecur);
-
- DPRINTF (("Returned reference: %s", sRef_unparseFull (tref)));
-
- if (sRef_isValid (tref))
- {
- tcref = sRef_copy (tref);
-
- if (sRef_isDead (tcref))
- {
- sRef_setDefined (tcref, g_currentloc);
- sRef_setOnly (tcref, g_currentloc);
- }
-
- if (sRef_isRefCounted (tcref))
- {
- /* could be a new ref now (but only if its returned) */
- sRef_setAliasKindComplete (tcref, AK_ERROR, g_currentloc);
- }
-
- sRef_makeSafe (tcref);
- prefs = sRefSet_insert (prefs, tcref);
- }
- }
- }
-
- paramno++;
- } end_uentryList_elements ;
-
- if (sRefSet_size (prefs) > 0)
- {
- nstate n = sRef_getNullState (u->sref);
-
- if (sRefSet_size (prefs) == 1)
- {
- sRef rref = sRefSet_choose (prefs);
- tref = rref;
- res = sRef_makeType (sRef_getType (rref));
- sRef_copyState (res, tref);
- }
- else
- {
- /* should this ever happen? */ /*@i534 evans 2001-05-27 */
- res = sRefSet_mergeIntoOne (prefs);
- }
-
- if (nstate_isKnown (n))
- {
- sRef_setNullState (res, n, g_currentloc);
- DPRINTF (("Setting null: %s", sRef_unparseFull (res)));
- }
- }
- else
- {
- if (ctype_isFunction (u->utype))
- {
- DPRINTF (("Making new from %s -->", uentry_unparseFull (u)));
- res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
- }
- else
- {
- DPRINTF (("Making new from %s -->", uentry_unparseFull (u)));
- res = sRef_makeNew (ctype_unknown, u->sref, u->uname);
- }
-
- if (sRef_isRefCounted (res))
- {
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
- }
- }
-
- if (sRef_getNullState (res) == NS_ABSNULL)
- {
- ctype ct = ctype_realType (u->utype);
-
- if (ctype_isAbstract (ct))
- {
- sRef_setNotNull (res, g_currentloc);
- }
- else
- {
- if (ctype_isUser (ct))
- {
- sRef_setStateFromUentry (res, usymtab_getTypeEntry (ctype_typeId (ct)));
- }
- else
- {
- sRef_setNotNull (res, g_currentloc);
- }
- }
- }
-
- if (sRef_isRefCounted (res))
- {
- sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
- }
- else if (sRef_isKillRef (res))
- {
- sRef_setAliasKind (res, AK_REFCOUNTED, g_currentloc);
- }
- else
- {
- ;
- }
-
- ak = sRef_getAliasKind (res);
-
- if (alkind_isImplicit (ak))
- {
- sRef_setAliasKind (res, alkind_fixImplicit (ak), g_currentloc);
- }
-
-# if 0
- DPRINTF (("Aliasing: %s / %s", sRef_unparseFull (res), sRef_unparseFull (tref)));
- usymtab_addReallyForceMustAlias (tref, res); /* evans 2001-05-27 */
-
- /* evans 2002-03-03 - need to be symettric explicitly, since its not a local now */
- usymtab_addReallyForceMustAlias (res, tref);
-# endif
-
- sRefSet_free (prefs);
-
- DPRINTF (("Returns ref: %s", sRef_unparseFull (res)));
- return res;
- }
-}
-# endif
-
/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args, fileloc loc)
{
llassert (uentry_isRealFunction (u));
}
else
{
- /* should this ever happen? */ /*@i534 evans 2001-05-27 */
+ /* should this ever happen? */
res = sRefSet_mergeIntoOne (prefs);
}
return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
}
+
+bool uentry_hasBufStateInfo (uentry ue)
+{
+ llassert (uentry_isValid (ue));
+ return (ue->info->var->bufinfo != NULL);
+}
+
+bool uentry_isNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return ue->info->var->bufinfo->bufstate == BB_NULLTERMINATED;
+}
+
+bool uentry_isPossiblyNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return (ue->info->var->bufinfo->bufstate == BB_POSSIBLYNULLTERMINATED);
+}
+
+bool uentry_isNotNullTerminated (uentry ue)
+{
+ llassert (uentry_hasBufStateInfo (ue));
+ llassert (ue->info->var->bufinfo != NULL);
+ return (ue->info->var->bufinfo->bufstate == BB_NOTNULLTERMINATED);
+}
+
# ifdef DEBUGSPLINT
/*
void
uentryList_free (uentryList s)
{
-
if (!uentryList_isUndefined (s))
{
int i;
}
}
+void
+uentryList_freeShallow (uentryList s)
+{
+ if (!uentryList_isUndefined (s))
+ {
+ /*@-mustfree@*/ /* free shallow does not free the element */
+ sfree (s->elements);
+ /*@=mustfree@*/
+ sfree (s);
+ }
+}
+
bool
uentryList_isVoid (uentryList cl)
{
cp1 = p1->elements[index];
cp2 = p2->elements[index];
- /*@i32*/
/*
** Should compare uentry's --- need to fix report errors too.
*/
usymtab_lookupQuietNoAlt (usymtab p_s, cstring p_k);
static void usymtab_printAllAux (usymtab p_s) /*@modifies g_warningstream@*/ ;
-static int usymtab_getIndex (/*@notnull@*/ usymtab p_s, cstring p_k);
-static /*@exposed@*/ uentry usymtab_fetchIndex (/*@notnull@*/ usymtab p_s, int p_i);
-static /*@exposed@*/ uentry
- usymtab_lookupAux (usymtab p_s, cstring p_k);
-static /*@exposed@*/ /*@dependent@*/ /*@notnull@*/ usymtab
- usymtab_getFileTab (void) /*@globals filetab@*/ ;
-static int refTable_lookup (/*@notnull@*/ usymtab p_ut, int p_level, int p_index);
+
+/*@function bool usymtab_indexFound (usymId) @*/
+# define usymtab_indexFound(u) ((u) != usymId_notfound)
+
+static usymId usymtab_getIndex (/*@notnull@*/ usymtab p_s, cstring p_k);
+static /*@exposed@*/ uentry usymtab_fetchIndex (/*@notnull@*/ usymtab p_s, usymId p_ui);
+static /*@exposed@*/ uentry usymtab_lookupAux (usymtab p_s, cstring p_k);
+
+static /*@exposed@*/ /*@dependent@*/ /*@notnull@*/
+ usymtab usymtab_getFileTab (void) /*@globals filetab@*/ ;
+
+static int refTable_lookup (/*@notnull@*/ usymtab p_ut, int p_level, usymId p_index);
static bool usymtab_mustBreak (usymtab p_s);
static bool usymtab_mustEscape (usymtab p_s);
}
else
{
- int thisentry = s->nentries;
+ usymId thisentry = usymId_fromInt (s->nentries);
if (uentry_isVar (e))
{
*/
uentry old;
- int thisentry = s->nentries;
+ usymId thisentry = usymId_fromInt (s->nentries);
if (uentry_isValid (old = usymtab_lookupQuiet (s, uentry_rawName (e))))
{
/*@globals globtab@*/
/*@modifies st, e@*/
{
- usymId thisentry = st->nentries;
+ usymId thisentry = usymId_fromInt (st->nentries);
llassert (!uentry_isElipsisMarker (e));
if (uentry_isDatatype (e))
{
-
- uentry_setDatatype (e, thisentry);
+ uentry_setDatatype (e, typeId_fromUsymId (thisentry));
}
if (uentry_isFunction (e))
{
cstring ename = uentry_rawName (e);
bool staticEntry = FALSE;
- int eindex;
+ usymId eindex;
DPRINTF (("Sup entry aux: %s", uentry_unparseFull (e)));
{
eindex = usymtab_getIndex (st, ename);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ce = st->entries[eindex];
uentry_showWhereLast (ce);
}
- if (eindex == st->nentries - 1)
+ if (eindex == usymId_fromInt (st->nentries - 1))
{
;
}
eindex = usymtab_getIndex (st, ename);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ce = st->entries[eindex];
if (uentry_isDatatype (e))
{
- uentry_setDatatype (e, eindex);
+ uentry_setDatatype (e, typeId_fromUsymId (eindex));
}
if (st == globtab && !uentry_isSpecified (e))
st->entries[eindex] = e;
ce = e;
- if (uentry_isDatatype (e)) uentry_setDatatype (e, eindex);
+ if (uentry_isDatatype (e)) uentry_setDatatype (e, typeId_fromUsymId (eindex));
}
else
{
if (uentry_isDatatype (e))
{
- uentry_setDatatype (e, eindex);
+ uentry_setDatatype (e, typeId_fromUsymId (eindex));
}
if (cstringTable_isDefined (st->htable))
eindex = usymtab_getIndex (filetab, ename);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ce = filetab->entries[eindex];
}
exitPoint:
- return (staticEntry ? USYMIDINVALID : eindex);
+ return (staticEntry ? usymId_invalid : eindex);
}
static void
/*@globals globtab@*/ /*@modifies st, e@*/
{
cstring ename = uentry_rawName (e);
- int eindex;
+ usymId eindex;
/* static tags in global scope */
eindex = usymtab_getIndex (st, ename);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ce = st->entries[eindex];
if (uentry_isAbstractDatatype (e))
{
- uid = usymtab_supAbstractTypeEntry (e, FALSE);
- ret = ctype_createAbstract (uid);
+ typeId tid = usymtab_supAbstractTypeEntry (e, FALSE);
+ ret = ctype_createAbstract (tid);
+ uid = typeId_toUsymId (tid);
}
else
{
uid = usymtab_supEntryAux (globtab, e, FALSE);
- ret = ctype_createUser (uid);
+ ret = ctype_createUser (typeId_fromUsymId (uid));
}
if (sRef_modInFunction ())
if (uentry_isAbstractDatatype (e))
{
- uid = usymtab_supAbstractTypeEntry (e, FALSE);
+ uid = typeId_toUsymId (usymtab_supAbstractTypeEntry (e, FALSE));
}
else if (uentry_isMaybeAbstract (e) && context_getFlag (FLG_IMPABSTRACT))
{
if (maybeabs)
{
uentry ux;
- uid = usymtab_supAbstractTypeEntry (e, FALSE);
- ux = usymtab_getTypeEntry (uid);
+ typeId tid = usymtab_supAbstractTypeEntry (e, FALSE);
+ ux = usymtab_getTypeEntry (tid);
uentry_setAbstract (ux);
+ uid = typeId_toUsymId (tid);
}
else
{
uid = usymtab_supEntryAux (globtab, e, FALSE);
- e = usymtab_getTypeEntry (uid);
+ e = usymtab_getTypeEntry (typeId_fromUsymId (uid));
if (uentry_isMaybeAbstract (e))
{
else
{
uid = usymtab_supEntryAux (globtab, e, FALSE);
- e = usymtab_getTypeEntry (uid);
+ e = usymtab_getTypeEntry (typeId_fromUsymId (uid));
/*? evans 2002-12-16 removed this? it doesn't make sense
if (uentry_isMaybeAbstract (e))
return (globtab->entries[uid]);
}
-usymId
+typeId
usymtab_supAbstractTypeEntry (/*@only@*/ uentry e, bool dodef)
/*@globals globtab, filetab@*/
/*@modifies globtab, e@*/
{
- usymId uid;
+ typeId uid;
uentry ue;
- uid = usymtab_supEntryAux (globtab, e, FALSE);
+ uid = typeId_fromUsymId (usymtab_supEntryAux (globtab, e, FALSE));
ue = usymtab_getTypeEntry (uid);
if (dodef)
return (uid);
}
-usymId
+typeId
usymtab_supExposedTypeEntry (/*@only@*/ uentry e, bool dodef)
/*@globals globtab, filetab@*/
/*@modifies globtab, e@*/
{
- usymId uid;
+ typeId uid;
- uid = usymtab_supEntryAux (globtab, e, FALSE);
+ uid = typeId_fromUsymId (usymtab_supEntryAux (globtab, e, FALSE));
if (dodef)
{
recordFunctionType (globtab->entries[uid]);
}
- return (uid);
+ return uid;
}
ctype
/*@globals globtab, filetab@*/
/*@modifies globtab, e@*/
{
- usymId uid = usymtab_supEntryAux (globtab, e, FALSE);
+ typeId uid = typeId_fromUsymId (usymtab_supEntryAux (globtab, e, FALSE));
uentry ue = usymtab_getTypeEntry (uid);
uentry_setDatatype (ue, uid);
return (utab->lexlevel > paramsScope);
}
-static int
+static usymId
usymtab_getIndex (/*@notnull@*/ usymtab s, cstring k)
{
int i;
if (cstringTable_isDefined (s->htable))
{
i = cstringTable_lookup (s->htable, k);
- return i;
+ return usymId_fromInt (i);
}
else
{
if (!uentry_isUndefined (current)
&& cstring_equal (uentry_rawName (current), k))
{
- return i;
+ return usymId_fromInt (i);
}
}
- return NOT_FOUND;
+ return usymId_notfound;
}
}
static uentry
-usymtab_fetchIndex (/*@notnull@*/ usymtab s, int i)
+usymtab_fetchIndex (/*@notnull@*/ usymtab s, usymId ui)
{
+ int i = usymId_toInt (ui);
llassert (i >= 0 && i < s->nentries);
return (s->entries[i]);
}
-usymId
+typeId
usymtab_getTypeId (cstring k) /*@globals globtab@*/
{
usymId uid = usymtab_getIndex (globtab, k);
- if (uid == NOT_FOUND) return USYMIDINVALID;
-
- if (!(uentry_isDatatype (usymtab_getTypeEntry (uid)))) {
- return USYMIDINVALID;
- }
-
- return uid;
+ if (!usymtab_indexFound (uid)
+ || !(uentry_isDatatype (usymtab_getTypeEntry (typeId_fromUsymId (uid)))))
+
+ {
+ return typeId_invalid;
+ }
+ else
+ {
+ return typeId_fromUsymId (uid);
+ }
}
/*@dependent@*/ uentry
usymId uid = usymtab_getIndex (globtab, k);
uentry ue;
- if (uid == NOT_FOUND)
+ if (!usymtab_indexFound (uid))
{
- return USYMIDINVALID;
+ return usymId_invalid;
}
ue = usymtab_getGlobalEntry (uid);
if (uentry_isPriv (ue))
{
- return USYMIDINVALID;
+ return usymId_invalid;
}
return uid;
static /*@exposed@*/ uentry
usymtab_getEntryAux (/*@notnull@*/ usymtab s, usymId uid)
{
- llassert (uid != USYMIDINVALID);
+ llassert (uid != usymId_invalid);
- if (uid < 0 || uid >= s->nentries)
+ if (uid < 0 || uid >= usymId_fromInt (s->nentries))
{
llcontbug (message ("usymtab_getEntry: out of range: level = %d [%d]",
s->lexlevel, uid));
}
}
-/*@dependent@*/ /*@exposed@*/ uentry
- usymtab_getTypeEntry (usymId uid)
+/*@dependent@*/ /*@exposed@*/ uentry usymtab_getTypeEntry (typeId uid)
/*@globals globtab@*/
{
if (dbgload)
{
- if (uid >= 0 && uid < globtab->nentries)
+ if (uid >= 0 && uid < typeId_fromInt (globtab->nentries))
{
return (globtab->entries[uid]);
}
}
else
{
- llassert (uid >= 0 && uid < globtab->nentries);
+ llassert (uid >= 0 && uid < typeId_fromInt (globtab->nentries));
return (globtab->entries[uid]);
}
}
** in load files
*/
-/*@dependent@*/ /*@exposed@*/ uentry
- usymtab_getTypeEntrySafe (usymId uid)
+/*@dependent@*/ /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId uid)
/*@globals globtab@*/
{
- if (uid < 0 || uid >= globtab->nentries)
+ if (uid < 0 || uid >= typeId_fromInt (globtab->nentries))
{
return uentry_undefined;
}
-
- return (globtab->entries[uid]);
+
+ return (globtab->entries[uid]);
}
-bool
- usymtab_isBoolType (usymId uid)
+bool usymtab_isBoolType (typeId uid)
/*@globals globtab@*/
{
- llassert (uid >= 0 && uid < globtab->nentries);
+ llassert (uid >= 0 && uid < typeId_fromInt (globtab->nentries));
return (cstring_equal (uentry_rawName (globtab->entries[uid]),
context_getBoolName ()));
}
-cstring
-usymtab_getTypeEntryName (usymId uid)
+cstring usymtab_getTypeEntryName (typeId uid)
/*@globals globtab@*/
{
uentry ue;
/*@-compdestroy@*/ sfree (s); /*@=compdestroy@*/
}
+usymId usymtab_convertTypeId (typeId uid)
+{
+ return usymtab_convertId (typeId_toUsymId (uid));
+}
+
/*
-** converts usymId from old table to sorted one
+** usymtab_convertId: converts usymId from old table to sorted one
*/
-usymId
- usymtab_convertId (usymId uid)
+usymId usymtab_convertId (usymId uid)
/*@globals oldtab, utab@*/
{
uentry ue;
uentry_unparse (ue), uid,
uentry_unparse (utab->entries[ret]), ret));
- llassertprint (ret != USYMIDINVALID, ("convertId: return is invalid"));
+ llassertprint (ret != usymId_invalid, ("convertId: return is invalid"));
return (ret);
}
if (sRef_isUndefGlob (el))
{
- int index = sRef_getScopeIndex (el);
+ usymId index = sRef_getScopeIndex (el);
sRef sr = sRef_updateSref (el);
fileloc loc = uentry_whereEarliest (fcn);
{
usymtab_entries (stab, current)
{
- if (usymtab_getIndex (ttab, uentry_rawName (current)) == NOT_FOUND)
+ if (!usymtab_indexFound (usymtab_getIndex (ttab, uentry_rawName (current))))
{
uentry old = /*@-compmempass@*/
usymtab_lookupAux (ltab, uentry_rawName (current));
{
uentry fthis = ftab->entries[i];
uentry old = usymtab_lookupAux (env, uentry_rawName (fthis));
- int tindex = usymtab_getIndex (ttab, uentry_rawName (fthis));
+ usymId tindex = usymtab_getIndex (ttab, uentry_rawName (fthis));
DPRINTF (("Entry: %s / %s", uentry_unparseFull (fthis), uentry_unparseFull (old)));
continue;
}
- if (tindex != NOT_FOUND)
+ if (usymtab_indexFound (tindex))
{
uentry tthis = ttab->entries[tindex];
void usymtab_checkFinalScope (bool isReturn)
/*@globals utab@*/
{
- bool mustFree = context_getFlag (FLG_MUSTFREEONLY) || context_getFlag (FLG_MUSTFREEFRESH); /*@i423 remove this mustFree */
bool mustDefine = context_getFlag (FLG_MUSTDEFINE);
- /* bool mustNotAlias = context_getFlag (FLG_MUSTNOTALIAS); */
sRefSet checked = sRefSet_new ();
usymtab stab = utab;
int i;
if (!uentry_sameObject (ce, oue))
{
- DPRINTF (("Skipping outer entry: %s / %s", uentry_unparseFull (ce),
- uentry_unparseFull (oue)));
- /*@i32 what if it is one an alternate branch? */
+ /* what if it is one an alternate branch? */
/*@innercontinue@*/ continue;
}
}
if (cstring_isDefined (msg))
{
- /*@i32 print extra info for assignments@*/
- DPRINTF (("From: %s", sRef_unparseFull (sr)));
- DPRINTF (("Null? %s / %s",
- bool_unparse (sRef_isDefinitelyNull (sr)),
- bool_unparse (usymtab_isGuarded (sr))));
-
if (optgenerror
(FLG_STATETRANSFER,
message
} end_valueTable_elements;
}
- DPRINTF (("Here 1"));
-
- if (mustFree)
+ DPRINTF (("Check mustfree entry: %s", uentry_unparseFull (ce)));
+
+ if (!sRefSet_member (checked, sr) && !sRef_isFileOrGlobalScope (rb))
{
- DPRINTF (("Check mustfree entry: %s", uentry_unparseFull (ce)));
-
- if (!sRefSet_member (checked, sr) && !sRef_isFileOrGlobalScope (rb))
+ if (ctype_isRealSU (uentry_getType (ce))
+ && !uentry_isAnyParam (ce)
+ && !uentry_isRefParam (ce)
+ && !uentry_isStatic (ce)
+ && !sRef_isDependent (sr)
+ && !sRef_isOwned (sr))
{
- if (ctype_isRealSU (uentry_getType (ce))
- && !uentry_isAnyParam (ce)
- && !uentry_isRefParam (ce)
- && !uentry_isStatic (ce)
- && !sRef_isDependent (sr)
- && !sRef_isOwned (sr))
+ sRefSet als = usymtab_allAliases (sr);
+
+ if (sRefSet_isEmpty (als))
{
- sRefSet als = usymtab_allAliases (sr);
-
- if (sRefSet_isEmpty (als))
- {
- transferChecks_localDestroyed (sr, g_currentloc);
- }
- else
+ transferChecks_localDestroyed (sr, g_currentloc);
+ }
+ else
+ {
+ /* aliased, no problem */ ;
+ }
+
+ sRefSet_free (als);
+ }
+ else if
+ (!uentry_isStatic (ce)
+ && ((sRef_isNewRef (sr))
+ || (((sRef_isOnly (sr) || sRef_isFresh (sr)
+ || sRef_isKeep (sr) || sRef_isOwned (sr))
+ && !sRef_isDead (sr))
+ && (!sRef_definitelyNull (sr))
+ && (!usymtab_isDefinitelyNull (sr)))))
+ {
+ bool hasError = TRUE;
+
+ DPRINTF (("Checking: %s", sRef_unparseFull (sr)));
+
+ /*
+ ** If its a scope exit, check if there is an alias.
+ ** If so, make it only. If not, there is an error.
+ */
+
+ if (!isReturn)
+ {
+ if (transferChecks_canLoseReference (sr, g_currentloc))
{
- /* aliased, no problem */ ;
+ DPRINTF (("Can lose!"));
+ hasError = FALSE;
}
-
- sRefSet_free (als);
}
- else if
- (!uentry_isStatic (ce)
- && ((sRef_isNewRef (sr))
- || (((sRef_isOnly (sr) || sRef_isFresh (sr)
- || sRef_isKeep (sr) || sRef_isOwned (sr))
- && !sRef_isDead (sr))
- && (!sRef_definitelyNull (sr))
- && (!usymtab_isDefinitelyNull (sr)))))
- {
- bool hasError = TRUE;
-
- DPRINTF (("Checking: %s", sRef_unparseFull (sr)));
-
- /*
- ** If its a scope exit, check if there is an alias.
- ** If so, make it only. If not, there is an error.
- */
-
- if (!isReturn)
- {
- if (transferChecks_canLoseReference (sr, g_currentloc))
- {
- DPRINTF (("Can lose!"));
- hasError = FALSE;
- }
- }
-
- if (hasError)
- {
- if (sRef_hasLastReference (sr))
- {
- sRef ar = sRef_getAliasInfoRef (sr);
-
- if (optgenerror
- (sRef_isFresh (ar) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
- message
- ("Last reference %q to %s storage %qnot %q before %q",
- sRef_unparse (sr),
- alkind_unparse (sRef_getAliasKind (sr)),
- sRef_unparseOpt (ar),
- cstring_makeLiteral (sRef_isKeep (sr)
- ? "transferred" : "released"),
- cstring_makeLiteral (isReturn
- ? "return" : "scope exit")),
- g_currentloc))
- {
- sRef_showRefLost (sr);
- }
- }
- else if (sRef_isNewRef (sr))
- {
- if (optgenerror
- (sRef_isFresh (sr) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
- message
- ("%q %q not released before %q",
- cstring_makeLiteral
- (alkind_isKillRef (sRef_getOrigAliasKind (sr))
- ? "Kill reference parameter" : "New reference"),
- uentry_getName (ce),
- cstring_makeLiteral (isReturn
- ? "return" : "scope exit")),
- g_currentloc))
- {
- sRef_showAliasInfo (sr);
- }
- }
- else
- {
- if (ctype_isRealSU (sRef_getType (sr)))
- {
- transferChecks_structDestroyed (sr, g_currentloc);
- }
- else
- {
- DPRINTF (("Here we are: %s", sRef_unparseFull (sr)));
-
- if (optgenerror
- (sRef_isFresh (sr) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
- message
- ("%s storage %q not %q before %q",
- alkind_capName (sRef_getAliasKind (sr)),
- uentry_getName (ce),
- cstring_makeLiteral (sRef_isKeep (sr)
- ? "transferred" : "released"),
- cstring_makeLiteral (isReturn
- ? "return" : "scope exit")),
- g_currentloc))
- {
- sRef_showAliasInfo (sr);
- DPRINTF (("Storage: %s", sRef_unparseFull (sr)));
- }
- }
- }
- }
- }
- else
+
+ if (hasError)
{
- ;
+ if (sRef_hasLastReference (sr))
+ {
+ sRef ar = sRef_getAliasInfoRef (sr);
+
+ if (optgenerror
+ (sRef_isFresh (ar) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
+ message
+ ("Last reference %q to %s storage %qnot %q before %q",
+ sRef_unparse (sr),
+ alkind_unparse (sRef_getAliasKind (sr)),
+ sRef_unparseOpt (ar),
+ cstring_makeLiteral (sRef_isKeep (sr)
+ ? "transferred" : "released"),
+ cstring_makeLiteral (isReturn
+ ? "return" : "scope exit")),
+ g_currentloc))
+ {
+ sRef_showRefLost (sr);
+ }
+ }
+ else if (sRef_isNewRef (sr))
+ {
+ if (optgenerror
+ (sRef_isFresh (sr) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
+ message
+ ("%q %q not released before %q",
+ cstring_makeLiteral
+ (alkind_isKillRef (sRef_getOrigAliasKind (sr))
+ ? "Kill reference parameter" : "New reference"),
+ uentry_getName (ce),
+ cstring_makeLiteral (isReturn
+ ? "return" : "scope exit")),
+ g_currentloc))
+ {
+ sRef_showAliasInfo (sr);
+ }
+ }
+ else
+ {
+ if (ctype_isRealSU (sRef_getType (sr)))
+ {
+ transferChecks_structDestroyed (sr, g_currentloc);
+ }
+ else
+ {
+ if (optgenerror
+ (sRef_isFresh (sr) ? FLG_MUSTFREEFRESH : FLG_MUSTFREEONLY,
+ message
+ ("%s storage %q not %q before %q",
+ alkind_capName (sRef_getAliasKind (sr)),
+ uentry_getName (ce),
+ cstring_makeLiteral (sRef_isKeep (sr)
+ ? "transferred" : "released"),
+ cstring_makeLiteral (isReturn
+ ? "return" : "scope exit")),
+ g_currentloc))
+ {
+ sRef_showAliasInfo (sr);
+ DPRINTF (("Storage: %s", sRef_unparseFull (sr)));
+ }
+ }
+ }
}
}
+ else
+ {
+ ;
+ }
}
if (mustDefine && uentry_isOut (ce))
if (sRef_isCvar (el))
{
uentry current;
- int index = sRef_getScopeIndex (el);
+ usymId index = sRef_getScopeIndex (el);
if (sRef_isFileStatic (el))
{
# ifdef DEBUGSPLINT
usymtab_checkAllValid ();
# endif
-/*@i523@*/ }
+}
/*@=globstate@*/
/*
** yikes! don't let the '170 kids see this one...
*/
-int
-uentry_directParamNo (uentry ue)
+usymId
+usymtab_directParamNo (uentry ue)
{
if (uentry_isVar (ue))
{
if (sRef_lexLevel (sr) == functionScope)
{
- int index = sRef_getScopeIndex (sr);
+ usymId index = sRef_getScopeIndex (sr);
- if (index < uentryList_size (context_getParams ()))
+ if (index < usymId_fromInt (uentryList_size (context_getParams ())))
{
return index;
}
}
}
- return -1;
+ return usymId_invalid;
}
/*@dependent@*/ /*@exposed@*/ uentry
s = usymtab_dropEnv (s);
}
- if (index >= s->nentries)
+ if (index >= usymId_fromInt (s->nentries))
{
return uentry_undefined;
}
while (usymtab_isBranch (s) && s->lexlevel == level)
{
int eindex = refTable_lookup (s, level, index);
-
if (eindex != NOT_FOUND)
{
s = usymtab_dropEnv (s);
}
- if (s->lexlevel == level && (index < s->nentries))
+ if (s->lexlevel == level && (index < usymId_fromInt (s->nentries)))
{
ue = s->entries[index];
}
- if (index >= s->nentries)
+ if (index >= usymId_fromInt (s->nentries))
{
return uentry_undefined;
}
*/
static
-int refTable_lookup (/*@notnull@*/ usymtab ut, int level, int index)
+int refTable_lookup (/*@notnull@*/ usymtab ut, int level, usymId index)
{
refTable rt = ut->reftable;
int i;
for (i = 0; i < ut->nentries; i++)
{
- if (rt[i]->level == level && rt[i]->index == index)
+ if (rt[i]->level == level && rt[i]->index == usymId_toInt (index))
{
return i;
}
static /*@dependent@*/ /*@exposed@*/ uentry
usymtab_addRefEntry (/*@notnull@*/ usymtab s, cstring k)
{
- int eindex;
usymtab ut = s;
if (ut->reftable == NULL)
while (s != GLOBAL_ENV)
{
- eindex = usymtab_getIndex (s, k);
+ usymId eindex = usymtab_getIndex (s, k);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry current = s->entries[eindex];
else
{
ut->reftable[ut->nentries - 1]
- = refentry_create (s->lexlevel, eindex);
+ = refentry_create (s->lexlevel, usymId_toInt (eindex));
}
return (ue);
while (s != GLOBAL_ENV)
{
- int eindex = usymtab_getIndex (s, k);
+ usymId eindex = usymtab_getIndex (s, k);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ret = s->entries[eindex];
# if 0
static /*@dependent@*/ /*@exposed@*/ uentry
usymtab_lookupQuietAux (usymtab s, cstring k, bool noalt)
{
- int eindex;
-
while (s != GLOBAL_ENV)
{
- eindex = usymtab_getIndex (s, k);
+ usymId eindex = usymtab_getIndex (s, k);
- if (eindex != NOT_FOUND)
+ if (usymtab_indexFound (eindex))
{
uentry ret = s->entries[eindex];
return (ret);
}
else
{
- llassert (s != NULL); /*@i523 should not need this? */
+ llassert (s != NULL);
s = s->env;
}
}
usymtab_lookupType (cstring k)
/*@globals globtab@*/
{
- usymId uid = usymtab_getTypeId (k);
+ typeId uid = usymtab_getTypeId (k);
- if (uid == USYMIDINVALID)
+ if (typeId_isInvalid (uid))
{
llcontbug (message ("usymtab_lookupType: not found: %s", k));
return ctype_unknown;
ctype
usymtab_lookupAbstractType (cstring k) /*@globals globtab@*/
{
- usymId uid = usymtab_getTypeId (k);
+ typeId uid = usymtab_getTypeId (k);
- if (uid == USYMIDINVALID)
+ if (typeId_isInvalid (uid))
{
llcontbug (message ("usymtab_lookupType: not found: %s", k));
return ctype_unknown;
}
sfree (u); /* evans 2002-07-12: was inside if */
- /*:!!mustfree@*/
-} /*!@=mustfree@*/
+}
static void
usymtab_freeAux (/*@only@*/ usymtab u)
dbgfree = TRUE;
usymtab_freeAux (utab);
utab = usymtab_undefined;
-/*@i523@*/ }
+ /*@-globstate@*/
+} /*@=globstate@*/ /* Splint cannot tell that utab is killed */
static int usymtab_lexicalLevel (void) /*@globals utab@*/
{
}
bool
-usymtab_matchForwardStruct (usymId u1, usymId u2)
+usymtab_matchForwardStruct (typeId u1, typeId u2)
/*@globals globtab@*/
{
uentry ue1 = usymtab_getTypeEntry (u1);
if (u2 == rtuid) return TRUE;
- if (usymId_isValid (rtuid))
+ if (typeId_isValid (rtuid))
{
- reptype = uentry_getType (usymtab_getTypeEntry (rtuid));
-
+ reptype = uentry_getType (usymtab_getTypeEntry (rtuid));
return (ctype_isUA (reptype) && (u2 == (ctype_typeId (reptype))));
}
}
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
# include "gram.h"
# include "lclscan.h"
# include "lclsyntable.h"
cstring tn;
fileloc loc;
uentry ue;
- usymId uid;
+ typeId uid;
abstBodyNode ab;
if (n == (abstractNode) 0)
}
}
-static void
- declareExposedType (exposedNode n, bool priv)
+static void declareExposedType (exposedNode n, bool priv)
{
- usymId uid;
qtype c;
cstring s;
uentry_setDefined (ue, loc);
}
- uid = usymtab_supExposedTypeEntry (ue, context_inLCLLib () && !priv);
+ (void) usymtab_supExposedTypeEntry (ue, context_inLCLLib () && !priv);
} end_declaratorInvNodeList_elements;
qtype_free (c);
}
}
- if (usymId_isInvalid (tn))
+ if (typeId_isInvalid (tn))
{
acct = context_fileAccessTypes ();
}
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
varDeclarationNodeList varDeclarationNodeList_new ()
{
*/
# include "splintMacros.nf"
-# include "llbasic.h"
+# include "basic.h"
varNodeList varNodeList_new ()
{
andersk / splint.git / commitdiff
