From: evans1629 Date: Mon, 14 Apr 2003 04:12:55 +0000 (+0000) Subject: Fixed all /*@i...@*/ tags (except 1). X-Git-Tag: splint-3_1_0~16 X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/b73d1009d4a3494951c129e49f50f8b4c795deb1 Fixed all /*@i...@*/ tags (except 1). --- diff --git a/doc/manual.doc b/doc/manual.doc index 4b1b134..8b4b3b1 100644 Binary files a/doc/manual.doc and b/doc/manual.doc differ diff --git a/src/.splintrc b/src/.splintrc index e7af515..10e3bd2 100644 --- a/src/.splintrc +++ b/src/.splintrc @@ -76,6 +76,9 @@ -boolfalse FALSE +numliteral ++numabstractindex ++numabstractlit +-numabstractprint -indentspaces 3 diff --git a/src/Headers/basic.h b/src/Headers/basic.h index 1578c3f..8cc45a4 100644 --- a/src/Headers/basic.h +++ b/src/Headers/basic.h @@ -68,6 +68,8 @@ # include "varKinds.h" # include "sRefSet.h" # include "ekind.h" +# include "usymId.h" +# include "typeId.h" # include "usymIdSet.h" # include "sRefList.h" # include "uentryList.h" @@ -109,9 +111,9 @@ # include "mtincludes.h" # include "functionConstraint.h" # include "fileIdList.h" - # include "context.h" # include "constants.h" +# include "llglobals.h" # else # error "Multiple include" diff --git a/src/Headers/cstringList.h b/src/Headers/cstringList.h index f96818e..d27873d 100644 --- a/src/Headers/cstringList.h +++ b/src/Headers/cstringList.h @@ -27,7 +27,7 @@ extern /*@unused@*/ /*@falsewhennull@*/ bool cstringList_empty (/*@sef@*/ cstrin 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) /*@*/ ; diff --git a/src/Headers/fileLib.h b/src/Headers/fileLib.h index cf0462a..5168718 100644 --- a/src/Headers/fileLib.h +++ b/src/Headers/fileLib.h @@ -19,7 +19,7 @@ extern cstring fileLib_withoutExtension (cstring p_s, cstring p_suffix) /*@*/ ; 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 diff --git a/src/Headers/flags.h b/src/Headers/flags.h index e81b563..dcf4e26 100644 --- a/src/Headers/flags.h +++ b/src/Headers/flags.h @@ -114,7 +114,8 @@ flags_processFlags (bool p_inCommandLine, 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 */ ; diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h index 1d515de..a0b0ca2 100644 --- a/src/Headers/functionClauseList.h +++ b/src/Headers/functionClauseList.h @@ -41,8 +41,8 @@ extern /*@unused@*/ functionClauseList 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) ; diff --git a/src/Headers/llbasic.h b/src/Headers/llbasic.h deleted file mode 100644 index 4c2e4af..0000000 --- a/src/Headers/llbasic.h +++ /dev/null @@ -1,20 +0,0 @@ -/* -** 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 - - - - - diff --git a/src/Headers/llerror.h b/src/Headers/llerror.h index 2e3a6c8..99b39e5 100644 --- a/src/Headers/llerror.h +++ b/src/Headers/llerror.h @@ -422,7 +422,6 @@ extern void llgenindentmsgnoloc (/*@only@*/ cstring p_s); extern /*@observer@*/ cstring lldecodeerror (int) /*@*/ ; -/*@i523@*/ /* ** should be static, but used in cpperror (which shouldn't exist) */ diff --git a/src/Headers/misc.h b/src/Headers/misc.h index 35244e4..3afd2b4 100644 --- a/src/Headers/misc.h +++ b/src/Headers/misc.h @@ -35,7 +35,6 @@ extern long unsigned longUnsigned_fromInt (int p_x) /*@*/ /*@ensures result == # 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)) diff --git a/src/Headers/mtAnnotationList.h b/src/Headers/mtAnnotationList.h index b02c6e7..0e18e97 100644 --- a/src/Headers/mtAnnotationList.h +++ b/src/Headers/mtAnnotationList.h @@ -6,11 +6,13 @@ # 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;@*/ @@ -29,14 +31,14 @@ extern cstring mtAnnotationList_unparseSep (mtAnnotationList p_s, cstring p_sep) 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) ; diff --git a/src/Headers/mtDefaultsDeclList.h b/src/Headers/mtDefaultsDeclList.h index 2be663f..a4d7a75 100644 --- a/src/Headers/mtDefaultsDeclList.h +++ b/src/Headers/mtDefaultsDeclList.h @@ -39,7 +39,7 @@ extern mtDefaultsDeclList /*@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 diff --git a/src/Headers/mtLoseReferenceList.h b/src/Headers/mtLoseReferenceList.h index 8d881a9..d051bf6 100644 --- a/src/Headers/mtLoseReferenceList.h +++ b/src/Headers/mtLoseReferenceList.h @@ -32,14 +32,14 @@ extern cstring mtLoseReferenceList_unparseSep (mtLoseReferenceList p_s, 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) ; diff --git a/src/Headers/mtMergeClauseList.h b/src/Headers/mtMergeClauseList.h index 082c216..65587b1 100644 --- a/src/Headers/mtMergeClauseList.h +++ b/src/Headers/mtMergeClauseList.h @@ -39,7 +39,7 @@ extern /*@unused@*/ mtMergeClauseList /*@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) ; diff --git a/src/Headers/mtTransferClauseList.h b/src/Headers/mtTransferClauseList.h index a2ae122..16ef039 100644 --- a/src/Headers/mtTransferClauseList.h +++ b/src/Headers/mtTransferClauseList.h @@ -32,14 +32,14 @@ extern cstring mtTransferClauseList_unparseSep (mtTransferClauseList p_s, cstrin 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) ; diff --git a/src/Headers/mtValuesNode.h b/src/Headers/mtValuesNode.h index ce89d39..92250f1 100644 --- a/src/Headers/mtValuesNode.h +++ b/src/Headers/mtValuesNode.h @@ -19,7 +19,6 @@ extern void mtValuesNode_free (/*@only@*/ mtValuesNode) ; 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) diff --git a/src/Headers/nameChecks.h b/src/Headers/nameChecks.h index b356b43..a08f107 100644 --- a/src/Headers/nameChecks.h +++ b/src/Headers/nameChecks.h @@ -14,7 +14,6 @@ extern void checkFileScopeName (uentry p_ue) /*@modifies g_warningstream, p_ue@* 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" diff --git a/src/Headers/splintMacros.nf b/src/Headers/splintMacros.nf index 265edf6..1d5a738 100644 --- a/src/Headers/splintMacros.nf +++ b/src/Headers/splintMacros.nf @@ -111,7 +111,6 @@ /*@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@*/ diff --git a/src/Headers/stateCombinationTable.h b/src/Headers/stateCombinationTable.h index 7564661..c21339c 100644 --- a/src/Headers/stateCombinationTable.h +++ b/src/Headers/stateCombinationTable.h @@ -20,22 +20,20 @@ typedef struct { 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); @@ -52,7 +50,7 @@ extern void stateCombinationTable_update (stateCombinationTable p_h, 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, diff --git a/src/Headers/typeId.h b/src/Headers/typeId.h new file mode 100644 index 0000000..6ffbe4d --- /dev/null +++ b/src/Headers/typeId.h @@ -0,0 +1,35 @@ +# 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 diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index 314f009..d60d77f 100644 --- a/src/Headers/uentry.h +++ b/src/Headers/uentry.h @@ -354,6 +354,8 @@ extern /*@exposed@*/ sRef uentry_getSref (/*@temp@*/ uentry p_e) /*@*/ ; 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) /*@*/ ; @@ -483,7 +485,7 @@ extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn) 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@*/ @@ -608,41 +610,23 @@ extern bool uentry_hasAccessType (uentry p_e); /*@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 { diff --git a/src/Headers/uentryList.h b/src/Headers/uentryList.h index 50d01d2..bcee1ae 100644 --- a/src/Headers/uentryList.h +++ b/src/Headers/uentryList.h @@ -58,6 +58,7 @@ extern cstring uentryList_unparseAbbrev (uentryList p_p) /*@*/ ; 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@*/ ; diff --git a/src/Headers/usymId.h b/src/Headers/usymId.h index cdd6a37..65dd6c3 100644 --- a/src/Headers/usymId.h +++ b/src/Headers/usymId.h @@ -1,18 +1,28 @@ # 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" diff --git a/src/Headers/usymIdSet.h b/src/Headers/usymIdSet.h index 57dc116..61b60b5 100644 --- a/src/Headers/usymIdSet.h +++ b/src/Headers/usymIdSet.h @@ -11,8 +11,6 @@ # ifndef USYMIDSET_H # define USYMIDSET_H -# include "usymId.h" - abst_typedef /*@null@*/ struct { int entries; diff --git a/src/Headers/usymtab.h b/src/Headers/usymtab.h index 44fb5e1..89d8118 100644 --- a/src/Headers/usymtab.h +++ b/src/Headers/usymtab.h @@ -150,7 +150,7 @@ extern bool usymtab_existsTypeEither (cstring p_k) /*@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@*/ ; @@ -177,7 +177,7 @@ extern usymId usymtab_addEntry (/*@only@*/ uentry 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) @@ -187,27 +187,6 @@ extern bool usymtab_existsUnionTag (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; \ @@ -245,6 +224,7 @@ extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k) /*@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@*/ ; @@ -315,7 +295,7 @@ extern /*@exposed@*/ uentry 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) diff --git a/src/Makefile.am b/src/Makefile.am index 024c878..aa76a9e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -211,11 +211,11 @@ HEADERSRC = Headers/abstBodyNode.h Headers/ltokenList.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 \ diff --git a/src/Makefile.in b/src/Makefile.in index 65226c0..d501c7f 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -307,11 +307,11 @@ HEADERSRC = Headers/abstBodyNode.h Headers/ltokenList.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 \ diff --git a/src/abstract.c b/src/abstract.c index 3e95eae..5138b56 100644 --- a/src/abstract.c +++ b/src/abstract.c @@ -35,7 +35,7 @@ */ # 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" @@ -2523,8 +2523,12 @@ typeExpr makeArrayNode (/*@returned@*/ typeExpr x, ** 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 { diff --git a/src/checking.c b/src/checking.c index 7e11ce8..c574aee 100644 --- a/src/checking.c +++ b/src/checking.c @@ -32,7 +32,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "llgrammar.h" # include "checking.h" # include "lclscan.h" diff --git a/src/clabstract.c b/src/clabstract.c index f1da5b0..f8bf35b 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -29,7 +29,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "cgrammar.h" # include "usymtab_interface.h" @@ -961,7 +961,7 @@ checkTypeDecl (uentry e, ctype rep) 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 ())); diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 3dfcf90..5e6c84f 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -794,7 +794,7 @@ static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt /*@-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@*/ diff --git a/src/constraintList.c b/src/constraintList.c index 24654bc..ba719e9 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -31,7 +31,7 @@ */ # 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) \ diff --git a/src/context.c b/src/context.c index bb24cab..e0755e4 100644 --- a/src/context.c +++ b/src/context.c @@ -34,7 +34,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "usymtab_interface.h" # include "exprChecks.h" @@ -143,7 +143,7 @@ static struct 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. */ @@ -831,10 +831,9 @@ context_resetAllFlags (void) ** 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; @@ -842,6 +841,7 @@ context_resetAllFlags (void) 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; @@ -1116,7 +1116,7 @@ context_setModeAux (cstring s, bool warn) { 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, @@ -1171,6 +1171,7 @@ context_setModeAux (cstring s, bool warn) FLG_SPECUNDEF, FLG_IMPCHECKMODINTERNALS, FLG_DECLUNDEF, FLG_INCONDEFS, FLG_INCONDEFSLIB, FLG_MISPLACEDSHAREQUAL, FLG_REDUNDANTSHAREQUAL, + FLG_NUMABSTRACTPRINT, FLG_MATCHFIELDS, FLG_MACROPARAMS, FLG_MACROASSIGN, @@ -1252,6 +1253,7 @@ context_setModeAux (cstring s, bool warn) FLG_MODFILESYSTEM, FLG_MACROMATCHNAME, FLG_FORMATCONST, + FLG_NUMABSTRACTPRINT, FLG_STRINGLITNOROOM, FLG_STRINGLITNOROOMFINALNULL, FLG_STRINGLITSMALLER, @@ -2298,8 +2300,7 @@ static 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); } @@ -3023,8 +3024,10 @@ context_setString (flagcode flag, cstring val) { ; /* 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) == '\"') { @@ -4856,7 +4859,7 @@ valueTable context_createValueTable (sRef s, stateInfo sinfo) 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) @@ -4897,11 +4900,11 @@ valueTable context_createGlobalMarkerValueTable (stateInfo sinfo) 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))); diff --git a/src/cpperror.c b/src/cpperror.c index 137ef16..70ac876 100644 --- a/src/cpperror.c +++ b/src/cpperror.c @@ -84,7 +84,7 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # define FATAL_EXIT_CODE EXIT_FAILURE # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "cpplib.h" # include "cpperror.h" diff --git a/src/cppexp.c b/src/cppexp.c index 8182205..60f16b0 100644 --- a/src/cppexp.c +++ b/src/cppexp.c @@ -57,7 +57,7 @@ Written by Per Bothner 1994. */ # include # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "cpplib.h" # include "cpphash.h" # include "cppexp.h" @@ -366,7 +366,6 @@ cppReader_parseNumber (cppReader *pfile, char *start, int olen) /*@requires maxR if (overflow) { - /*@i23 add flags for all these...*/ cppReader_pedwarnLit (pfile, cstring_makeLiteralTemp ("Integer constant out of range")); diff --git a/src/cpphash.c b/src/cpphash.c index 937af05..3716c2a 100644 --- a/src/cpphash.c +++ b/src/cpphash.c @@ -52,7 +52,7 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. what you give them. Help stamp out software-hoarding! */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include # include "cpplib.h" # include "cpphash.h" diff --git a/src/cpplib.c b/src/cpplib.c index 340f34b..82bbdd6 100644 --- a/src/cpplib.c +++ b/src/cpplib.c @@ -93,7 +93,7 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # include # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lcllib.h" # include "cpplib.h" # include "cpperror.h" @@ -2756,15 +2756,17 @@ compare_defs (DEFINITION *d1, DEFINITION *d2) 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) { @@ -2790,12 +2792,14 @@ 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) @@ -2803,20 +2807,14 @@ do_defineAux (cppReader *pfile, struct directive *keyword, 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; @@ -2833,7 +2831,7 @@ do_defineAux (cppReader *pfile, struct directive *keyword, else { BADBRANCH; } - /*@i2@*/ + /* Print the warning if it's not ok. */ if (!ok) { @@ -2849,7 +2847,7 @@ do_defineAux (cppReader *pfile, struct directive *keyword, } cpp_setLocation (pfile); - /*@i2@*/ + if (hp->type == T_MACRO) { if (hp->value.defn->noExpand) @@ -2874,7 +2872,6 @@ do_defineAux (cppReader *pfile, struct directive *keyword, message ("Macro %q already defined", cstring_copyLength (mdef.symnam, mdef.symlen))); - /*@i2@*/ } } @@ -2890,7 +2887,7 @@ do_defineAux (cppReader *pfile, struct directive *keyword, */ hashNode hn; - /*@i2@*/ + if (CPPOPTIONS (pfile)->debug_output && (keyword != NULL)) { pass_thru_directive (buf, limit, pfile, keyword); @@ -2904,9 +2901,8 @@ do_defineAux (cppReader *pfile, struct directive *keyword, } /*@=branchstate@*/ return 0; - /*@i2@*/ + nope: - /*@i2@*/ return 1; } @@ -2917,21 +2913,23 @@ do_define (cppReader *pfile, struct directive *keyword, 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; @@ -2944,11 +2942,13 @@ struct argdata { 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) { @@ -2990,7 +2990,7 @@ cppReader_pushBuffer (cppReader *pfile, char *buffer, size_t length) return buf; } - /*@i2@*/ + cppBuffer * cppReader_popBuffer (cppReader *pfile) { @@ -3002,9 +3002,11 @@ 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) { @@ -3027,7 +3029,6 @@ cppReader_scanBuffer (cppReader *pfile) } } } - /*@i2@*/ /* * Rescan a string (which may have escape marks) into pfile's buffer. @@ -4209,9 +4210,8 @@ cpplib_macroExpand (cppReader *pfile, /*@dependent@*/ hashNode hp) } 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 @@ -4219,7 +4219,7 @@ cpplib_macroExpand (cppReader *pfile, /*@dependent@*/ hashNode hp) /* 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) { @@ -4866,7 +4866,7 @@ do_include (cppReader *pfile, struct directive *keyword, 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) @@ -7615,11 +7615,13 @@ void cpplib_initializeReader (cppReader *pfile) /* Must be done after library is 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); } } @@ -7630,11 +7632,14 @@ void cpplib_initializeReader (cppReader *pfile) /* Must be done after library is 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; diff --git a/src/cppmain.c b/src/cppmain.c index 7cd4a0a..61bca21 100644 --- a/src/cppmain.c +++ b/src/cppmain.c @@ -47,7 +47,7 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. 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" diff --git a/src/cscannerHelp.c b/src/cscannerHelp.c index d3379ae..ece76d9 100644 --- a/src/cscannerHelp.c +++ b/src/cscannerHelp.c @@ -405,7 +405,8 @@ static char macro_nextChar (void) } else /* if (c == '@') */ { - llassert (FALSE); /*@i23@*/ + llassert (FALSE); + if (cscannerHelp_handleLlSpecial () != BADTOK) { llerrorlit (FLG_SYNTAX, "Macro cannot use special syntax"); @@ -935,7 +936,9 @@ int cscannerHelp_handleLlSpecial (void) s = mstring_append (s, c); charsread++; } - /*@i888@*/ } + /*@-branchstate@*/ + } /* spurious (?) warnings about s */ + /*@=branchstate@*/ DPRINTF (("Read: %s / %s", s, fileloc_unparse (g_currentloc))); @@ -1163,7 +1166,7 @@ int cscannerHelp_handleLlSpecial (void) 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); @@ -1433,7 +1436,9 @@ int cscannerHelp_handleLlSpecial (void) message ("Semantic comment unrecognized: %s", cstring_fromChars (os)), loc); - /*@i888@*/ } + /*@-branchstate@*/ + } /* spurious (?) warning about t */ + /*@=branchstate@*/ sfree (t); } @@ -1575,7 +1580,7 @@ int cscannerHelp_processIdentifier (cstring id) if (annotationInfo_isDefined (ainfo)) { DPRINTF (("Found annotation: %s", annotationInfo_unparse (ainfo))); - /*@i324@*/ yylval.annotation = ainfo; + yylval.annotation = ainfo; return CANNOTATION; } else @@ -1774,12 +1779,12 @@ int cscannerHelp_processIdentifier (cstring id) 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)) @@ -1805,7 +1810,7 @@ int cscannerHelp_processIdentifier (cstring id) } else { - /*@i32@*/ yylval.entry = le; + yylval.entry = le; return (IDENTIFIER); } } @@ -1827,7 +1832,7 @@ int cscannerHelp_processIdentifier (cstring id) } else { - /*@i32@*/ yylval.entry = le; + yylval.entry = le; return (IDENTIFIER); } @@ -2144,7 +2149,6 @@ bool cscannerHelp_isConstraintToken (int tok) { return (tok == QMAXSET || tok == QMAXREAD); /* || tok == QMINREAD || tok == QMINSET */ - /*@i4523@*/ /* uncomment the additional if statement tests when minSet and minRead are supported */ } diff --git a/src/cstringList.c b/src/cstringList.c index 5ab4995..ac2ec0e 100644 --- a/src/cstringList.c +++ b/src/cstringList.c @@ -349,12 +349,14 @@ cstringList_get (cstringList s, int index) 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 { diff --git a/src/cstringTable.c b/src/cstringTable.c index 5eeb122..61be3f7 100644 --- a/src/cstringTable.c +++ b/src/cstringTable.c @@ -55,8 +55,7 @@ static hentry hentry_create (/*@only@*/ cstring key, int val) h->key = key; h->val = val; - llassert (val != HBUCKET_DNE); /*@i523 way bogus! */ - + llassert (val != HBUCKET_DNE); return (h); } @@ -116,12 +115,13 @@ hbucket_grow (/*@notnull@*/ hbucket 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); diff --git a/src/ctbase.i b/src/ctbase.i index 2b30048..49f3e25 100644 --- a/src/ctbase.i +++ b/src/ctbase.i @@ -34,7 +34,7 @@ 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) @@ -1024,12 +1024,11 @@ ctbase_dump (ctbase c) 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: @@ -1173,7 +1172,8 @@ ctbase_free (/*@only@*/ ctbase c) 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: @@ -2382,13 +2382,13 @@ ctbase_compare (ctbase c1, ctbase c2, bool strict) 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: diff --git a/src/cttable.i b/src/cttable.i index 585daf8..7613cb6 100644 --- a/src/cttable.i +++ b/src/cttable.i @@ -541,7 +541,7 @@ cttable_addComplex (/*@only@*/ ctbase cnew) ctb = ctype_getCtbase (i); - /*@i32 is this optimization really worthwhile??? */ + /* is this optimization really worthwhile? */ if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb)) { diff --git a/src/ctype.c b/src/ctype.c index 1ea98e0..8ed249f 100644 --- a/src/ctype.c +++ b/src/ctype.c @@ -1954,8 +1954,7 @@ ctype_dump (ctype c) 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 ())) { @@ -2296,7 +2295,10 @@ bool ctype_isRefCounted (ctype t) bool ctype_isVisiblySharable (ctype t) { - if (ctype_isUnknown (t)) return TRUE; + if (ctype_isUnknown (t)) + { + return TRUE; + } if (ctype_isConj (t)) { @@ -2312,7 +2314,14 @@ bool ctype_isVisiblySharable (ctype t) if (rt == t) { - return TRUE; + if (ctype_isNumAbstract (t)) + { + return FALSE; + } + else + { + return TRUE; + } } else { diff --git a/src/declaratorInvNodeList.c b/src/declaratorInvNodeList.c index c0784f5..a36c8ab 100644 --- a/src/declaratorInvNodeList.c +++ b/src/declaratorInvNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" declaratorInvNodeList declaratorInvNodeList_new () diff --git a/src/declaratorNodeList.c b/src/declaratorNodeList.c index ad36481..3bfa3db 100644 --- a/src/declaratorNodeList.c +++ b/src/declaratorNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" declaratorNodeList declaratorNodeList_new () diff --git a/src/exprChecks.c b/src/exprChecks.c index 5a8f624..9bc78f2 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -264,13 +264,13 @@ checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e, 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) @@ -319,7 +319,7 @@ checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e, 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)) { diff --git a/src/exprNode.c b/src/exprNode.c index 403dbab..9df0718 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -1330,6 +1330,15 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) 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 @@ -1623,11 +1632,9 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, 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 */ @@ -2236,7 +2243,7 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, codetext, expecttype, a->typ, exprNode_unparse (a)), a->loc)) - { + { if (fileloc_isDefined (formatloc) && context_getFlag (FLG_SHOWCOL)) { @@ -3126,7 +3133,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, 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, @@ -3701,7 +3708,7 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args) if (sRef_isResult (sRef_getRootBase (sel))) { - ; /*@i423 what do we do about results */ + ; /* what do we do about results? */ } else { @@ -6465,8 +6472,8 @@ exprNode_vaArg (/*@only@*/ lltok tok, /*@only@*/ exprNode arg, /*@only@*/ qtype */ 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, @@ -6777,8 +6784,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) 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; @@ -6991,7 +6997,6 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause) exprNode_loc (pred)); } - /*! exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); */ /*@i523@*/ exprNode_checkUse (pred, pred->sref, pred->loc); if (!exprNode_isError (tclause)) @@ -7120,9 +7125,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred, exprNode_loc (pred)); } - /*@i3423 exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);*/ exprNode_checkUse (ret, pred->sref, pred->loc); - exprNode_mergeCondUSs (ret, tclause, eclause); } @@ -8496,37 +8499,6 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t) { 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 { @@ -8535,9 +8507,6 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t) 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); /* @@ -11107,6 +11076,7 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) 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 */ diff --git a/src/fcnNodeList.c b/src/fcnNodeList.c index 19bb191..2325202 100644 --- a/src/fcnNodeList.c +++ b/src/fcnNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" fcnNodeList fcnNodeList_new () diff --git a/src/fileLib.c b/src/fileLib.c index ea08927..ec108b0 100644 --- a/src/fileLib.c +++ b/src/fileLib.c @@ -220,8 +220,10 @@ cstring fileLib_cleanName (cstring s) { 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; } diff --git a/src/fileTable.c b/src/fileTable.c index dee235e..0fe22bf 100644 --- a/src/fileTable.c +++ b/src/fileTable.c @@ -48,7 +48,7 @@ # include # include # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "llmain.h" # include "portab.h" @@ -328,7 +328,6 @@ fileTable_addFilePrim (fileTable ft, /*@temp@*/ cstring name, 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) diff --git a/src/fileloc.c b/src/fileloc.c index c1f95dd..84d9e3b 100644 --- a/src/fileloc.c +++ b/src/fileloc.c @@ -34,7 +34,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "portab.h" @@ -794,7 +794,7 @@ fileloc_unparse (fileloc f) { 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; diff --git a/src/flags.c b/src/flags.c index b908b15..e8b3ceb 100644 --- a/src/flags.c +++ b/src/flags.c @@ -493,7 +493,6 @@ printAllFlags (bool desc, bool full) cstringSList_elements (fl, el) { - /*@i22@*/ /*find out why this is necessary*/ cstring tmp; tmp = cstring_copy(el); llmsg (message ("%q\n\n", describeFlag (tmp))); diff --git a/src/flags.def b/src/flags.def index 6c0d636..404b0c2 100644 --- a/src/flags.def +++ b/src/flags.def @@ -131,6 +131,16 @@ static flaglist flags = "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) @@ -502,7 +512,23 @@ static flaglist flags = "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 }, { diff --git a/src/functionClause.c b/src/functionClause.c index a127ed4..27f862c 100644 --- a/src/functionClause.c +++ b/src/functionClause.c @@ -28,7 +28,7 @@ # 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)); diff --git a/src/functionClauseList.c b/src/functionClauseList.c index 665605c..a78acf3 100644 --- a/src/functionClauseList.c +++ b/src/functionClauseList.c @@ -94,10 +94,10 @@ functionClauseList functionClauseList_add (functionClauseList s, /*@keep@*/ func } 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) @@ -106,7 +106,7 @@ functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ if (!functionClauseList_isDefined (s)) { - /*@i32@*/ return functionClauseList_single (el); + return functionClauseList_single (el); } if (s->nspace <= 0) @@ -121,10 +121,10 @@ functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - - /*@i32@*/ return s; + + return s; } cstring @@ -217,7 +217,6 @@ functionClauseList_setImplictConstraints (/*@returned@*/ functionClauseList s) else { llassert (FALSE); - /*@i2523 fix this */ } } } diff --git a/src/functionConstraint.c b/src/functionConstraint.c index 96bfff8..4bed9ac 100644 --- a/src/functionConstraint.c +++ b/src/functionConstraint.c @@ -28,7 +28,7 @@ # 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)); @@ -91,7 +91,7 @@ extern constraintList functionConstraint_getBufferConstraints (functionConstrain { 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)); } diff --git a/src/genericTable.c b/src/genericTable.c index 4ba7a09..5e1b2a3 100644 --- a/src/genericTable.c +++ b/src/genericTable.c @@ -53,6 +53,15 @@ ghentry_create (/*@keep@*/ cstring key, /*@keep@*/ void *val) 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) { @@ -95,7 +104,7 @@ static ghbucket ghbucket_single (/*@keep@*/ ghentry e) 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); } @@ -116,9 +125,10 @@ ghbucket_grow (/*@notnull@*/ ghbucket 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); @@ -143,7 +153,7 @@ ghbucket_add (/*@notnull@*/ ghbucket h, /*@only@*/ ghentry e) h->entries[h->size] = e; h->size++; h->nspace--; -/*@i23@*/ } +} static int ghbucket_ncollisions (ghbucket h) @@ -178,7 +188,14 @@ void ghbucket_free (/*@only@*/ 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); } } @@ -323,7 +340,7 @@ genericTable_stats (genericTable 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); /* @@ -340,8 +357,8 @@ genericTable_addEntry (/*@notnull@*/ genericTable h, /*@keep@*/ ghentry e) } else { - /*@i23@*/ ghbucket_add (h->buckets[hindex], e); - /*@i23@*/ } + ghbucket_add (h->buckets[hindex], e); + } } void @@ -407,13 +424,13 @@ genericTable_insert (genericTable h, cstring key, void *value) 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) diff --git a/src/globalsClause.c b/src/globalsClause.c index 59fef94..a0c9fca 100644 --- a/src/globalsClause.c +++ b/src/globalsClause.c @@ -34,7 +34,8 @@ globalsClause_create (lltok tok, globSet gl) 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) @@ -53,7 +54,7 @@ extern void globalsClause_free (globalsClause gclause) { if (gclause == NULL) { - return; /*@i435 shouldn't ever need this? */ + return; /* shouldn't ever need this? */ } globSet_free (gclause->globs); diff --git a/src/help.c b/src/help.c index 53163fd..eee5ffb 100644 --- a/src/help.c +++ b/src/help.c @@ -78,7 +78,7 @@ describeVars (void) 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)); diff --git a/src/idDecl.c b/src/idDecl.c index 4c0429c..d60e65e 100644 --- a/src/idDecl.c +++ b/src/idDecl.c @@ -51,7 +51,7 @@ idDecl_free (idDecl t) { 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); diff --git a/src/importNodeList.c b/src/importNodeList.c index 597516b..6abfca3 100644 --- a/src/importNodeList.c +++ b/src/importNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ importNodeList importNodeList_new () diff --git a/src/imports.c b/src/imports.c index bc91fe9..c6c4441 100644 --- a/src/imports.c +++ b/src/imports.c @@ -32,7 +32,7 @@ */ # 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" diff --git a/src/initDeclNodeList.c b/src/initDeclNodeList.c index 74669d4..1edf677 100644 --- a/src/initDeclNodeList.c +++ b/src/initDeclNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ initDeclNodeList initDeclNodeList_new () diff --git a/src/inputStream.c b/src/inputStream.c index 95c1323..70931d0 100644 --- a/src/inputStream.c +++ b/src/inputStream.c @@ -45,7 +45,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "portab.h" @@ -80,14 +80,12 @@ inputStream_create (cstring name, cstring suffix, bool echo) { 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) @@ -101,9 +99,7 @@ inputStream_create (cstring name, cstring suffix, bool echo) 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; @@ -114,7 +110,7 @@ inputStream_create (cstring name, cstring suffix, bool echo) s->stringSourceTail = NULL; s->buffer[0] = '\0'; - /*@i523@*/ return s; + return s; } extern /*@only@*/ inputStream diff --git a/src/interfaceNodeList.c b/src/interfaceNodeList.c index 3c4bdff..a0b9e18 100644 --- a/src/interfaceNodeList.c +++ b/src/interfaceNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ interfaceNodeList interfaceNodeList_new () diff --git a/src/lclctypes.c b/src/lclctypes.c index 48535eb..b9164a0 100644 --- a/src/lclctypes.c +++ b/src/lclctypes.c @@ -38,7 +38,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" typedef struct { diff --git a/src/lclinit.c b/src/lclinit.c index 4743994..94b590a 100644 --- a/src/lclinit.c +++ b/src/lclinit.c @@ -28,7 +28,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "gram.h" # include "lclscan.h" # include "scanline.h" diff --git a/src/lcllib.c b/src/lcllib.c index 6fecc48..1cfe85f 100644 --- a/src/lcllib.c +++ b/src/lcllib.c @@ -37,7 +37,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "version.h" @@ -227,11 +227,10 @@ lcllib_isSkipHeader (cstring sname) /*@-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 */ } } @@ -256,7 +255,7 @@ lcllib_isSkipHeader (cstring sname) cstring_free (xname); /*@noaccess cstring@*/ - /*@-nullstate@*/ /*@i233@*/ /* same problem as above */ + /*@-nullstate@*/ /* same problem as above */ return FALSE; /*@=nullstate@*/ } diff --git a/src/lclscan.c b/src/lclscan.c index 20b6dee..bf968b6 100644 --- a/src/lclscan.c +++ b/src/lclscan.c @@ -43,7 +43,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@-redecl@*/ /* from llgrammar.y */ extern bool g_inTypeDef; diff --git a/src/lclscanline.c b/src/lclscanline.c index 622a1ac..59bbd8f 100644 --- a/src/lclscanline.c +++ b/src/lclscanline.c @@ -50,7 +50,7 @@ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "gram.h" # include "lclscan.h" # include "scanline.h" diff --git a/src/lcltokentable.c b/src/lcltokentable.c index e6b5e83..3c2ab73 100644 --- a/src/lcltokentable.c +++ b/src/lcltokentable.c @@ -29,7 +29,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lcltokentable.h" static long unsigned MaxToken; diff --git a/src/letDeclNodeList.c b/src/letDeclNodeList.c index 6a23885..ec20039 100644 --- a/src/letDeclNodeList.c +++ b/src/letDeclNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ letDeclNodeList letDeclNodeList_new () diff --git a/src/lh.c b/src/lh.c index 05930e8..30fed49 100644 --- a/src/lh.c +++ b/src/lh.c @@ -40,7 +40,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "lh.h" # include "llmain.h" @@ -276,7 +276,6 @@ lhCleanup (void) 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 diff --git a/src/llerror.c b/src/llerror.c index 0560920..4f108c4 100644 --- a/src/llerror.c +++ b/src/llerror.c @@ -30,7 +30,7 @@ # include "splintMacros.nf" # include # include -# 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! */ @@ -928,7 +928,22 @@ xllgenformattypeerror (char *srcFile, int srcLine, { 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 { diff --git a/src/llgrammar.c.der b/src/llgrammar.c.der index 2ce2282..3d837ac 100644 --- a/src/llgrammar.c.der +++ b/src/llgrammar.c.der @@ -204,7 +204,7 @@ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lclscan.h" # include "checking.h" # include "lslparse.h" diff --git a/src/llgrammar.y b/src/llgrammar.y index ab30d80..6bebe40 100644 --- a/src/llgrammar.y +++ b/src/llgrammar.y @@ -27,7 +27,7 @@ %{ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lclscan.h" # include "checking.h" # include "lslparse.h" diff --git a/src/llmain.c b/src/llmain.c index ad07b72..5a38916 100644 --- a/src/llmain.c +++ b/src/llmain.c @@ -49,7 +49,7 @@ # endif # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "help.h" diff --git a/src/lslOpList.c b/src/lslOpList.c index fde38b8..54dcd5d 100644 --- a/src/lslOpList.c +++ b/src/lslOpList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ lslOpList lslOpList_new () diff --git a/src/lslOpSet.c b/src/lslOpSet.c index cba843e..2f1155b 100644 --- a/src/lslOpSet.c +++ b/src/lslOpSet.c @@ -31,7 +31,7 @@ */ # 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); diff --git a/src/lslinit.c b/src/lslinit.c index d80d761..83de1cf 100644 --- a/src/lslinit.c +++ b/src/lslinit.c @@ -28,7 +28,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "signature.h" # include "signature2.h" # include "scan.h" diff --git a/src/lslparse.c b/src/lslparse.c index 30efe8a..6f14644 100644 --- a/src/lslparse.c +++ b/src/lslparse.c @@ -32,7 +32,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lclscan.h" # include "signature.h" # include "signature2.h" diff --git a/src/lsymbolList.c b/src/lsymbolList.c index 6a42ebd..0e720f9 100644 --- a/src/lsymbolList.c +++ b/src/lsymbolList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ lsymbolList lsymbolList_new () diff --git a/src/lsymbolSet.c b/src/lsymbolSet.c index 7020918..e5491db 100644 --- a/src/lsymbolSet.c +++ b/src/lsymbolSet.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" lsymbolSet lsymbolSet_new () { diff --git a/src/ltoken.c b/src/ltoken.c index cc6e383..5b3a699 100644 --- a/src/ltoken.c +++ b/src/ltoken.c @@ -26,7 +26,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "llgrammar.h" # include "scanline.h" # include "lclscanline.h" diff --git a/src/ltokenList.c b/src/ltokenList.c index 96dae70..617319b 100644 --- a/src/ltokenList.c +++ b/src/ltokenList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@notnull@*/ /*@only@*/ ltokenList ltokenList_new () diff --git a/src/macrocache.c b/src/macrocache.c index 881b094..0db6792 100644 --- a/src/macrocache.c +++ b/src/macrocache.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "llmain.h" /*@constant int MCEBASESIZE;@*/ diff --git a/src/mapping.c b/src/mapping.c index 881a260..ef35daa 100644 --- a/src/mapping.c +++ b/src/mapping.c @@ -32,7 +32,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@constant int MAPPING_SIZE; @*/ # define MAPPING_SIZE 127 diff --git a/src/mtAnnotationList.c b/src/mtAnnotationList.c index b2afaea..977d7b2 100644 --- a/src/mtAnnotationList.c +++ b/src/mtAnnotationList.c @@ -74,14 +74,14 @@ mtAnnotationList_grow (/*@notnull@*/ mtAnnotationList s) 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)) { @@ -94,19 +94,19 @@ mtAnnotationList mtAnnotationList_add (mtAnnotationList s, /*@keep@*/ mtAnnotati } 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) @@ -121,10 +121,10 @@ mtAnnotationList mtAnnotationList_prepend (mtAnnotationList s, /*@keep@*/ mtAnno s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - /*@i32@*/ return s; + return s; } cstring diff --git a/src/mtDeclarationNode.c b/src/mtDeclarationNode.c index e9cecbf..a90270b 100644 --- a/src/mtDeclarationNode.c +++ b/src/mtDeclarationNode.c @@ -86,7 +86,7 @@ extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal) mvals = mtValuesNode_getValues (mtv); } - /*@-usedef@*/ /*@i34 splint should figure this out... */ + /*@-usedef@*/ /* splint should figure this out... */ nvalues = cstringList_size (mvals); /*@=usedef@*/ @@ -492,7 +492,7 @@ extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal) { for (j = low2index; j <= high2index; j++) { - /*@i32 check for multiple definitions! */ + /* Need to add checks for multiple definitions! */ if (mtTransferAction_isError (taction)) { diff --git a/src/mtDeclarationPiece.c b/src/mtDeclarationPiece.c index fa104ab..3f2da7f 100644 --- a/src/mtDeclarationPiece.c +++ b/src/mtDeclarationPiece.c @@ -36,7 +36,7 @@ mtDeclarationPiece_create (mtPieceKind kind, /*@null@*/ /*@only@*/ void *node) res->kind = kind; res->node = node; - /*@i32@*/ return res; + return res; } extern mtDeclarationPiece mtDeclarationPiece_createContext (mtContextNode node) /*@*/ diff --git a/src/mtDeclarationPieces.c b/src/mtDeclarationPieces.c index 694a0f8..6f20a5e 100644 --- a/src/mtDeclarationPieces.c +++ b/src/mtDeclarationPieces.c @@ -87,7 +87,7 @@ mtDeclarationPieces_findPiece (mtDeclarationPieces pieces, mtPieceKind kind) 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 { diff --git a/src/mtDefaultsDeclList.c b/src/mtDefaultsDeclList.c index db657d7..ba66fb7 100644 --- a/src/mtDefaultsDeclList.c +++ b/src/mtDefaultsDeclList.c @@ -94,10 +94,10 @@ mtDefaultsDeclList mtDefaultsDeclList_add (mtDefaultsDeclList s, /*@keep@*/ mtDe } 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) @@ -106,7 +106,7 @@ mtDefaultsDeclList mtDefaultsDeclList_prepend (mtDefaultsDeclList s, /*@keep@*/ if (!mtDefaultsDeclList_isDefined (s)) { - /*@i32@*/ return mtDefaultsDeclList_single (el); + return mtDefaultsDeclList_single (el); } if (s->nspace <= 0) @@ -121,10 +121,10 @@ mtDefaultsDeclList mtDefaultsDeclList_prepend (mtDefaultsDeclList s, /*@keep@*/ s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - /*@i32@*/ return s; + return s; } cstring diff --git a/src/mtLoseReferenceList.c b/src/mtLoseReferenceList.c index 20bb914..ff756e4 100644 --- a/src/mtLoseReferenceList.c +++ b/src/mtLoseReferenceList.c @@ -74,7 +74,7 @@ mtLoseReferenceList_grow (/*@notnull@*/ mtLoseReferenceList s) s->elements = newelements; } -mtLoseReferenceList mtLoseReferenceList_single (/*@keep@*/ mtLoseReference el) +mtLoseReferenceList mtLoseReferenceList_single (mtLoseReference el) { mtLoseReferenceList s = mtLoseReferenceList_new (); s = mtLoseReferenceList_add (s, el); @@ -94,19 +94,19 @@ mtLoseReferenceList mtLoseReferenceList_add (mtLoseReferenceList s, /*@keep@*/ m } 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) @@ -121,10 +121,10 @@ mtLoseReferenceList mtLoseReferenceList_prepend (mtLoseReferenceList s, /*@keep@ s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - /*@i32@*/ return s; + return s; } cstring diff --git a/src/mtMergeClauseList.c b/src/mtMergeClauseList.c index faf249b..9504902 100644 --- a/src/mtMergeClauseList.c +++ b/src/mtMergeClauseList.c @@ -94,10 +94,10 @@ mtMergeClauseList mtMergeClauseList_add (mtMergeClauseList s, /*@keep@*/ mtMerge } 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) @@ -106,7 +106,7 @@ mtMergeClauseList mtMergeClauseList_prepend (mtMergeClauseList s, /*@keep@*/ mtM if (!mtMergeClauseList_isDefined (s)) { - /*@i32@*/ return mtMergeClauseList_single (el); + return mtMergeClauseList_single (el); } if (s->nspace <= 0) @@ -121,10 +121,10 @@ mtMergeClauseList mtMergeClauseList_prepend (mtMergeClauseList s, /*@keep@*/ mtM s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - /*@i32@*/ return s; + return s; } cstring diff --git a/src/mtTransferClauseList.c b/src/mtTransferClauseList.c index 62b26d7..afbbe4d 100644 --- a/src/mtTransferClauseList.c +++ b/src/mtTransferClauseList.c @@ -74,7 +74,7 @@ mtTransferClauseList_grow (/*@notnull@*/ mtTransferClauseList s) s->elements = newelements; } -mtTransferClauseList mtTransferClauseList_single (/*@keep@*/ mtTransferClause el) +mtTransferClauseList mtTransferClauseList_single (mtTransferClause el) { mtTransferClauseList s = mtTransferClauseList_new (); s = mtTransferClauseList_add (s, el); @@ -94,19 +94,19 @@ mtTransferClauseList mtTransferClauseList_add (mtTransferClauseList s, /*@keep@* } 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) @@ -121,10 +121,10 @@ mtTransferClauseList mtTransferClauseList_prepend (mtTransferClauseList s, /*@ke s->elements[i] = s->elements [i - 1]; } - /*@i32@*/ s->elements[0] = el; + s->elements[0] = el; s->nelements++; - /*@i32@*/ return s; + return s; } cstring diff --git a/src/mtgrammar.c b/src/mtgrammar.c index 6f61067..67c2e99 100644 --- a/src/mtgrammar.c +++ b/src/mtgrammar.c @@ -118,7 +118,7 @@ # 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@*/ ; diff --git a/src/mtgrammar.c.der b/src/mtgrammar.c.der index 6f61067..67c2e99 100644 --- a/src/mtgrammar.c.der +++ b/src/mtgrammar.c.der @@ -118,7 +118,7 @@ # 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@*/ ; diff --git a/src/mtgrammar.y b/src/mtgrammar.y index bf4e435..591158a 100644 --- a/src/mtgrammar.y +++ b/src/mtgrammar.y @@ -31,7 +31,7 @@ # 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@*/ ; diff --git a/src/mtreader.c b/src/mtreader.c index 3eaf42d..c4b09d0 100644 --- a/src/mtreader.c +++ b/src/mtreader.c @@ -28,7 +28,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "mtgrammar.h" # include "mtscanner.h" diff --git a/src/mtscanner.c b/src/mtscanner.c index b13a09a..b350281 100644 --- a/src/mtscanner.c +++ b/src/mtscanner.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "mtgrammar.h" # include "mtscanner.h" diff --git a/src/nameChecks.c b/src/nameChecks.c index adbb2b0..20e8fa5 100644 --- a/src/nameChecks.c +++ b/src/nameChecks.c @@ -1124,7 +1124,7 @@ checkFileScopeName (/*@unused@*/ uentry ue) ** No file scope checks (yet) */ - /*@i423 add a file scope naming convention policy? */ + /* add a file scope naming convention policy? */ return; } @@ -1555,4 +1555,4 @@ void checkParamNames (uentry ue) } } -/*@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 */ diff --git a/src/osd.c b/src/osd.c index 71b5de4..4e72f78 100644 --- a/src/osd.c +++ b/src/osd.c @@ -1037,7 +1037,6 @@ cstring osd_absolutePath (cstring cwd, cstring filename) 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; @@ -1078,7 +1077,6 @@ cstring osd_outputPath (cstring filename) } else { - /*@i324 ! splint didn't report an errors for: return ++path_p; */ cstring_free (rel_buffer); return cstring_fromCharsNew (path_p + 1); } @@ -1166,7 +1164,7 @@ cstring osd_outputPath (cstring filename) 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))) diff --git a/src/pairNodeList.c b/src/pairNodeList.c index c390407..1f9dac1 100644 --- a/src/pairNodeList.c +++ b/src/pairNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ pairNodeList pairNodeList_new () diff --git a/src/paramNodeList.c b/src/paramNodeList.c index 6516fd2..cf1093f 100644 --- a/src/paramNodeList.c +++ b/src/paramNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ paramNodeList paramNodeList_new () diff --git a/src/programNodeList.c b/src/programNodeList.c index b5617f8..b184e43 100644 --- a/src/programNodeList.c +++ b/src/programNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ programNodeList programNodeList_new () diff --git a/src/quantifierNodeList.c b/src/quantifierNodeList.c index 9289dc8..41b6ff8 100644 --- a/src/quantifierNodeList.c +++ b/src/quantifierNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ quantifierNodeList quantifierNodeList_new () diff --git a/src/rcfiles.c b/src/rcfiles.c index aff1aaa..2bc9a1e 100644 --- a/src/rcfiles.c +++ b/src/rcfiles.c @@ -195,7 +195,10 @@ static void rcfiles_loadFile (/*:open:*/ FILE *rcfile, cstringList *passThroughA 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)); } diff --git a/src/replaceNodeList.c b/src/replaceNodeList.c index ee16481..f7490f7 100644 --- a/src/replaceNodeList.c +++ b/src/replaceNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ replaceNodeList replaceNodeList_new () diff --git a/src/sRef.c b/src/sRef.c index 1dae1a9..7eb9d63 100644 --- a/src/sRef.c +++ b/src/sRef.c @@ -343,7 +343,7 @@ static void sRef_checkValidAux (sRef s, sRefSet checkedsofar) 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: @@ -438,8 +438,8 @@ static /*@dependent@*/ /*@notnull@*/ /*@special@*/ sRef /* 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; @@ -890,7 +890,7 @@ sRef_getBaseUentry (sRef s) 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: @@ -1053,7 +1053,7 @@ sRef_getUentry (sRef s) 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: @@ -1076,13 +1076,13 @@ sRef_getUentry (sRef s) } } -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 @@ -2295,14 +2295,15 @@ sRef_closeEnough (sRef s1, sRef s2) 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: { @@ -3547,7 +3548,7 @@ static int sRef_depth (sRef s) 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)); @@ -3570,7 +3571,7 @@ sRef sRef_makeExternal (sRef t) 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; @@ -3584,7 +3585,7 @@ sRef sRef_makeExternal (sRef t) 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)); @@ -4042,8 +4043,6 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other, ** Merge value table states */ - - /*@i3245@*/ # if 0 /* ** This doesn't do anything. And its broken too... @@ -4407,8 +4406,8 @@ sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef a, /*@exposed@*/ sRef b) 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); @@ -6029,7 +6028,7 @@ bool sRef_isDirectParam (sRef s) 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) @@ -6113,7 +6112,7 @@ void sRef_free (/*@only@*/ sRef s) s->definfo = stateInfo_undefined; s->nullinfo = stateInfo_undefined; - /*@i32@*/ sfree (s); + sfree (s); } } @@ -6290,7 +6289,7 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f) 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)) @@ -6654,7 +6653,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s, 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); @@ -6721,7 +6720,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s, 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; @@ -6930,7 +6929,7 @@ sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef t) 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)) { @@ -7253,10 +7252,8 @@ sRef_copyState (sRef s1, sRef s2) 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; } } @@ -9205,13 +9202,13 @@ static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef s) 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; @@ -9431,7 +9428,7 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s) 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: @@ -10013,7 +10010,7 @@ bool sRef_makeStateSpecial (sRef s) ** 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) { diff --git a/src/scan.c b/src/scan.c index ebbbf3d..8c38a02 100644 --- a/src/scan.c +++ b/src/scan.c @@ -43,7 +43,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "signature.h" # include "signature2.h" # include "scan.h" diff --git a/src/scanline.c b/src/scanline.c index 392a4e1..1c539b1 100644 --- a/src/scanline.c +++ b/src/scanline.c @@ -40,7 +40,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "signature.h" # include "signature2.h" # include "scan.h" diff --git a/src/shift.c b/src/shift.c index ba3202e..d423aa2 100644 --- a/src/shift.c +++ b/src/shift.c @@ -35,7 +35,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "shift.h" /*@constant static int SHIFTMAX=200;@*/ diff --git a/src/sigNodeSet.c b/src/sigNodeSet.c index e7f55d7..26d27fe 100644 --- a/src/sigNodeSet.c +++ b/src/sigNodeSet.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "intSet.h" static bool sigNodeSet_member (sigNodeSet p_s, sigNode p_el); diff --git a/src/signature.c.der b/src/signature.c.der index 12cb56b..2df1fc4 100644 --- a/src/signature.c.der +++ b/src/signature.c.der @@ -116,7 +116,7 @@ # include # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lslparse.h" # include "signature.h" diff --git a/src/signature.y b/src/signature.y index 107e6b3..b52657d 100644 --- a/src/signature.y +++ b/src/signature.y @@ -33,7 +33,7 @@ # include # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "lslparse.h" # include "signature.h" diff --git a/src/sort.c b/src/sort.c index e8266ed..d631770 100644 --- a/src/sort.c +++ b/src/sort.c @@ -36,7 +36,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "llgrammar.h" # include "lclscan.h" diff --git a/src/sortList.c b/src/sortList.c index 8b196b4..5b5511c 100644 --- a/src/sortList.c +++ b/src/sortList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ sortList sortList_new () diff --git a/src/sortSet.c b/src/sortSet.c index 95ad972..46006ec 100644 --- a/src/sortSet.c +++ b/src/sortSet.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" sortSet sortSet_new () { diff --git a/src/sortSetList.c b/src/sortSetList.c index 76536d6..ef614bf 100644 --- a/src/sortSetList.c +++ b/src/sortSetList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ sortSetList sortSetList_new () diff --git a/src/stDeclNodeList.c b/src/stDeclNodeList.c index 2b7ebd3..7a6fd75 100644 --- a/src/stDeclNodeList.c +++ b/src/stDeclNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ stDeclNodeList stDeclNodeList_new () diff --git a/src/stateClause.c b/src/stateClause.c index 249e34e..cf2faf0 100644 --- a/src/stateClause.c +++ b/src/stateClause.c @@ -759,7 +759,7 @@ static sRefModVal stateClause_getStateFunction (stateClause cl) } else if (qual_isAliasQual (sq)) { - return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/ + return (sRefModVal) sRef_setAliasKind; } else { @@ -777,9 +777,12 @@ int stateClause_getStateParameter (stateClause cl) 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)) { diff --git a/src/stateClauseList.c b/src/stateClauseList.c index 1c01941..d51c24c 100644 --- a/src/stateClauseList.c +++ b/src/stateClauseList.c @@ -252,7 +252,7 @@ void stateClauseList_checkAll (uentry ue) if (stateClause_isGlobal (cl)) { - /*@i232@*/ + ; } else { @@ -396,7 +396,7 @@ void stateClauseList_checkAll (uentry ue) { 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", @@ -451,7 +451,7 @@ void stateClauseList_checkEqual (uentry old, uentry unew) { if (stateClause_isGlobal (cl)) { - ; /*@i32@*/ + ; /* Don't handle globals for now */ } else { diff --git a/src/stateCombinationTable.c b/src/stateCombinationTable.c index c116129..149e9e9 100644 --- a/src/stateCombinationTable.c +++ b/src/stateCombinationTable.c @@ -28,7 +28,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /* ** (key, value, value) => value @@ -82,13 +82,15 @@ stateCombinationTable stateCombinationTable_create (int size) 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) @@ -130,9 +132,10 @@ static void stateRow_free (/*@only@*/ stateRow r) { 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); @@ -143,7 +146,7 @@ void stateCombinationTable_free (/*@only@*/ stateCombinationTable t) int i; for (i = 0; i < t->size; i++) { - /*@i32@*/ stateRow_free (t->rows[i]); + stateRow_free (t->rows[i]); } sfree (t->rows); @@ -198,7 +201,7 @@ void stateCombinationTable_update (stateCombinationTable h, 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); @@ -207,10 +210,7 @@ int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, 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; } diff --git a/src/stateInfo.c b/src/stateInfo.c index b2fad5c..79e0049 100644 --- a/src/stateInfo.c +++ b/src/stateInfo.c @@ -97,9 +97,9 @@ static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo sinfo) 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 { @@ -116,18 +116,24 @@ static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo sinfo) 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@*/ } } } diff --git a/src/stateValue.c b/src/stateValue.c index 9c357d8..873ba4b 100644 --- a/src/stateValue.c +++ b/src/stateValue.c @@ -26,7 +26,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" extern /*@notnull@*/ stateValue stateValue_create (int value, stateInfo info) { diff --git a/src/storeRefNodeList.c b/src/storeRefNodeList.c index 1fce313..a21c547 100644 --- a/src/storeRefNodeList.c +++ b/src/storeRefNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ storeRefNodeList storeRefNodeList_new () diff --git a/src/symtable.c b/src/symtable.c index 7f026fd..b00dbb8 100644 --- a/src/symtable.c +++ b/src/symtable.c @@ -41,7 +41,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "gram.h" # include "lclscan.h" # include "lclsyntable.h" diff --git a/src/termNodeList.c b/src/termNodeList.c index b7c4ca2..35a49d7 100644 --- a/src/termNodeList.c +++ b/src/termNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" termNodeList termNodeList_new () { diff --git a/src/tokentable.c b/src/tokentable.c index ecc2e19..6b0e891 100644 --- a/src/tokentable.c +++ b/src/tokentable.c @@ -26,7 +26,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "osd.h" # include "tokentable.h" diff --git a/src/traitRefNodeList.c b/src/traitRefNodeList.c index 88a8bdd..5e49bcb 100644 --- a/src/traitRefNodeList.c +++ b/src/traitRefNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" /*@only@*/ traitRefNodeList traitRefNodeList_new () diff --git a/src/transferChecks.c b/src/transferChecks.c index bc4c8c9..d77e7c3 100644 --- a/src/transferChecks.c +++ b/src/transferChecks.c @@ -1657,7 +1657,7 @@ transferChecks_return (exprNode fexp, uentry rval) { if (stateClause_isGlobal (cl)) { - ; /*@i32@*/ + ; } else if (stateClause_setsMetaState (cl)) { @@ -1695,7 +1695,6 @@ transferChecks_return (exprNode fexp, uentry rval) exprNode_loc (fexp))) { sRef_showAliasInfo (sr); - /*@i32@*/ } } } @@ -2535,7 +2534,7 @@ checkTransferNullAux (sRef fref, exprNode fexp, /*@unused@*/ bool ffix, 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), @@ -4139,7 +4138,7 @@ checkMetaStateConsistent (/*@exposed@*/ sRef fref, sRef 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); @@ -4237,8 +4236,6 @@ checkMetaStateTransfer (exprNode fexp, sRef fref, exprNode texp, sRef tref, { if (nval == stateValue_error) { - /*@i32 print extra info for assignments@*/ - if (optgenerror (FLG_STATETRANSFER, message diff --git a/src/typeIdSet.c b/src/typeIdSet.c index ce35afd..0bfb036 100644 --- a/src/typeIdSet.c +++ b/src/typeIdSet.c @@ -119,8 +119,6 @@ void typeIdSet_loadTable (FILE *fin) tistable_addDirectEntry (u); s = reader_readLine (fin, os, MAX_DUMP_LINE_LENGTH); } - - /*@i32 free os? @*/ } static void tistable_grow (void) @@ -201,8 +199,7 @@ typeIdSet typeIdSet_emptySet (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) @@ -212,14 +209,14 @@ 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 { @@ -231,19 +228,19 @@ typeIdSet typeIdSet_insert (typeIdSet t, typeId el) { 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) diff --git a/src/typeNameNodeList.c b/src/typeNameNodeList.c index 42b11d4..d983d33 100644 --- a/src/typeNameNodeList.c +++ b/src/typeNameNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" typeNameNodeList typeNameNodeList_new () { diff --git a/src/uentry.c b/src/uentry.c index 5077faf..6d364fb 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -108,7 +108,7 @@ static void uentry_convertVarFunction (uentry ue) /*@modifies ue@*/ static /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/ { uentry ue = (uentry) dmalloc (sizeof (*ue)); - ue->warn = warnClause_undefined; /*@i32@*/ + ue->warn = warnClause_undefined; nuentries++; totuentries++; @@ -895,7 +895,8 @@ static void reflectImplicitFunctionQualifiers (/*@notnull@*/ uentry ue, bool spe } 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. */ } @@ -926,9 +927,7 @@ uentry_makeFunctionAux (cstring n, ctype t, 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)) { @@ -1104,7 +1103,7 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses) ** */ - uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); /*@i32@*/ + uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); } else { @@ -1313,7 +1312,7 @@ static void uentry_implicitParamAnnots (/*@notnull@*/ uentry e) 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; @@ -1474,8 +1473,7 @@ uentry_fixupSref (uentry ue) 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); } @@ -1485,7 +1483,7 @@ static void uentry_addStateClause (/*@notnull@*/ uentry ue, stateClause sc) { /* ** Okay to allow multiple clauses of the same kind. - */ /*@i834 is this true?@*/ + */ ue->info->fcn->specclauses = stateClauseList_add (ue->info->fcn->specclauses, sc); @@ -3154,7 +3152,7 @@ uentry uentry_makeConstantAux (cstring n, ctype t, 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); @@ -3315,7 +3313,7 @@ uentry uentry_makeVariableAux (cstring n, ctype 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; @@ -3330,7 +3328,7 @@ uentry uentry_makeVariableAux (cstring n, ctype t, 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))); @@ -3359,7 +3357,7 @@ uentry uentry_makeVariableAux (cstring n, ctype t, 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); } @@ -3676,7 +3674,7 @@ void uentry_addAccessType (uentry ue, typeId tid) /*@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)), @@ -3801,7 +3799,7 @@ uentry_makeUnspecFunction (cstring n, ctype t, uentry_setSpecDef (e, f); - e->warn = warnClause_undefined; /*@i634@*/ + e->warn = warnClause_undefined; e->uses = filelocList_new (); e->isPrivate = priv; e->hasNameError = FALSE; @@ -3865,7 +3863,7 @@ static /*@only@*/ /*@notnull@*/ uentry uentry_setSpecDef (e, f); - e->warn = warnClause_undefined; /*@i452@*/ + e->warn = warnClause_undefined; e->uses = filelocList_new (); e->isPrivate = FALSE; e->hasNameError = FALSE; @@ -3910,8 +3908,8 @@ uentry_makeEndIterAux (cstring n, typeIdSet access, /*@only@*/ fileloc f) 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); } @@ -3958,7 +3956,7 @@ static /*@only@*/ /*@notnull@*/ uentry 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)) { @@ -4312,12 +4310,12 @@ static uentry 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); @@ -4360,7 +4358,7 @@ static /*@only@*/ uentry 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)); @@ -4445,9 +4443,7 @@ uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, qual abstract, 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 (); @@ -4653,7 +4649,7 @@ static /*@only@*/ uentry 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)); @@ -4698,7 +4694,7 @@ static uentry 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)); @@ -4742,7 +4738,7 @@ static uentry 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)); @@ -5526,10 +5522,19 @@ uentry_isMaybeAbstract (uentry e) 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 @@ -6233,7 +6238,8 @@ sRef uentry_getSref (uentry e) 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)) @@ -6433,7 +6439,7 @@ uentry_getAbstractType (uentry e) ctype uentry_getRealType (uentry e) { ctype ct; - typeId uid = USYMIDINVALID; + typeId uid = typeId_invalid; if (uentry_isInvalid (e)) { @@ -6475,9 +6481,9 @@ ctype uentry_getRealType (uentry 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))); @@ -6506,7 +6512,7 @@ ctype uentry_getRealType (uentry e) ctype uentry_getForceRealType (uentry e) { ctype ct; - typeId uid = USYMIDINVALID; + typeId uid = typeId_invalid; if (uentry_isInvalid (e)) { @@ -6540,9 +6546,9 @@ ctype uentry_getForceRealType (uentry 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))); @@ -6588,7 +6594,7 @@ uentry uentry_nameCopy (cstring name, uentry e) } void -uentry_setDatatype (uentry e, usymId uid) +uentry_setDatatype (uentry e, typeId uid) { llassert (uentry_isDatatype (e)); @@ -8643,13 +8649,12 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, } */ - /*@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); @@ -8657,7 +8662,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, /*@-branchstate@*/ } } - /*@=branchstate@*/ /*@i23 shouldn't need this@*/ + /*@=branchstate@*/ /* shouldn't need this */ if (fileloc_isUndefined (old->whereDeclared)) { @@ -8671,7 +8676,8 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, { /* no change */ } -/*@i523 @*/ } + /*@-compmempass@*/ +} /*@=compmempass@*/ /* I think this is a spurious warning */ void uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m) @@ -9897,7 +9903,7 @@ static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old) } else { - fileloc_free (unew->whereSpecified); /*@i523 why no error without this? */ + fileloc_free (unew->whereSpecified); unew->whereSpecified = fileloc_copy (old->whereSpecified); } @@ -9908,7 +9914,7 @@ static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old) } else { - fileloc_free (unew->whereDefined); /*@i523 why no error without this? */ + fileloc_free (unew->whereDefined); unew->whereDefined = fileloc_copy (old->whereDefined); } @@ -9919,7 +9925,7 @@ static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old) } else { - fileloc_free (unew->whereDeclared); /*@i523 why no error without this? */ + fileloc_free (unew->whereDeclared); unew->whereDeclared = fileloc_copy (old->whereDeclared); } @@ -10454,8 +10460,6 @@ uentry_mergeValueStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other, if (nval == stateValue_error) { - /*@i32 print extra info for assignments@*/ - if (uentry_isGlobalMarker (res)) { if (optgenerror @@ -10635,8 +10639,6 @@ void uentry_setUsed (uentry e, fileloc loc) if (uentry_isValid (e)) { - int dp; - if (warnClause_isDefined (e->warn)) { flagSpec flg = warnClause_getFlag (e->warn); @@ -10695,9 +10697,9 @@ void uentry_setUsed (uentry e, fileloc loc) } } - 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; @@ -10736,207 +10738,6 @@ bool uentry_isReturned (uentry u) || 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)); @@ -11049,7 +10850,7 @@ bool uentry_isReturned (uentry u) } else { - /* should this ever happen? */ /*@i534 evans 2001-05-27 */ + /* should this ever happen? */ res = sRefSet_mergeIntoOne (prefs); } @@ -11552,6 +11353,34 @@ metaStateConstraintList uentry_getMetaStateEnsures (uentry e) 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 /* diff --git a/src/uentryList.c b/src/uentryList.c index 975f2a0..eca84f0 100644 --- a/src/uentryList.c +++ b/src/uentryList.c @@ -327,7 +327,6 @@ uentryList uentryList_copy (uentryList s) void uentryList_free (uentryList s) { - if (!uentryList_isUndefined (s)) { int i; @@ -342,6 +341,18 @@ uentryList_free (uentryList s) } } +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) { @@ -873,7 +884,6 @@ uentryList_matchFields (uentryList p1, uentryList p2) cp1 = p1->elements[index]; cp2 = p2->elements[index]; - /*@i32*/ /* ** Should compare uentry's --- need to fix report errors too. */ diff --git a/src/usymtab.c b/src/usymtab.c index 58174be..bdb71f9 100644 --- a/src/usymtab.c +++ b/src/usymtab.c @@ -153,13 +153,18 @@ static /*@exposed@*/ /*@dependent@*/ uentry 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); @@ -525,7 +530,7 @@ usymtab_addEntryBase (/*@notnull@*/ usymtab s, /*@only@*/ uentry e) } else { - int thisentry = s->nentries; + usymId thisentry = usymId_fromInt (s->nentries); if (uentry_isVar (e)) { @@ -552,7 +557,7 @@ usymtab_addEntryAlways (/*@notnull@*/ usymtab s, /*@only@*/ uentry e) */ uentry old; - int thisentry = s->nentries; + usymId thisentry = usymId_fromInt (s->nentries); if (uentry_isValid (old = usymtab_lookupQuiet (s, uentry_rawName (e)))) { @@ -585,7 +590,7 @@ usymtab_addEntryAux (/*@notnull@*/ usymtab st, /*@keep@*/ uentry e, bool isSref) /*@globals globtab@*/ /*@modifies st, e@*/ { - usymId thisentry = st->nentries; + usymId thisentry = usymId_fromInt (st->nentries); llassert (!uentry_isElipsisMarker (e)); @@ -635,8 +640,7 @@ usymtab_addEntryAux (/*@notnull@*/ usymtab st, /*@keep@*/ uentry e, bool isSref) if (uentry_isDatatype (e)) { - - uentry_setDatatype (e, thisentry); + uentry_setDatatype (e, typeId_fromUsymId (thisentry)); } if (uentry_isFunction (e)) @@ -713,7 +717,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, { cstring ename = uentry_rawName (e); bool staticEntry = FALSE; - int eindex; + usymId eindex; DPRINTF (("Sup entry aux: %s", uentry_unparseFull (e))); @@ -723,7 +727,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, { eindex = usymtab_getIndex (st, ename); - if (eindex != NOT_FOUND) + if (usymtab_indexFound (eindex)) { uentry ce = st->entries[eindex]; @@ -737,7 +741,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, uentry_showWhereLast (ce); } - if (eindex == st->nentries - 1) + if (eindex == usymId_fromInt (st->nentries - 1)) { ; } @@ -780,7 +784,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, eindex = usymtab_getIndex (st, ename); - if (eindex != NOT_FOUND) + if (usymtab_indexFound (eindex)) { uentry ce = st->entries[eindex]; @@ -807,7 +811,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, if (uentry_isDatatype (e)) { - uentry_setDatatype (e, eindex); + uentry_setDatatype (e, typeId_fromUsymId (eindex)); } if (st == globtab && !uentry_isSpecified (e)) @@ -843,7 +847,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, 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 { @@ -860,7 +864,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, if (uentry_isDatatype (e)) { - uentry_setDatatype (e, eindex); + uentry_setDatatype (e, typeId_fromUsymId (eindex)); } if (cstringTable_isDefined (st->htable)) @@ -970,7 +974,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, eindex = usymtab_getIndex (filetab, ename); - if (eindex != NOT_FOUND) + if (usymtab_indexFound (eindex)) { uentry ce = filetab->entries[eindex]; @@ -1036,7 +1040,7 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st, } exitPoint: - return (staticEntry ? USYMIDINVALID : eindex); + return (staticEntry ? usymId_invalid : eindex); } static void @@ -1044,12 +1048,12 @@ usymtab_replaceEntryAux (/*@notnull@*/ usymtab st, /*@only@*/ uentry e) /*@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]; @@ -1160,13 +1164,14 @@ usymtab_supTypeEntry (/*@only@*/ uentry e) 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 ()) @@ -1188,7 +1193,7 @@ usymtab_supReturnTypeEntry (/*@only@*/ uentry e) 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)) { @@ -1221,14 +1226,15 @@ usymtab_supReturnTypeEntry (/*@only@*/ uentry e) 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)) { @@ -1239,7 +1245,7 @@ usymtab_supReturnTypeEntry (/*@only@*/ uentry 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)) @@ -1257,15 +1263,15 @@ usymtab_supReturnTypeEntry (/*@only@*/ uentry 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) @@ -1286,14 +1292,14 @@ usymtab_supAbstractTypeEntry (/*@only@*/ uentry e, bool 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) { @@ -1307,7 +1313,7 @@ usymtab_supExposedTypeEntry (/*@only@*/ uentry e, bool dodef) recordFunctionType (globtab->entries[uid]); } - return (uid); + return uid; } ctype @@ -1315,7 +1321,7 @@ usymtab_supForwardTypeEntry (/*@only@*/ uentry e) /*@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); @@ -1395,7 +1401,7 @@ usymtab_inDeepScope () /*@globals utab@*/ return (utab->lexlevel > paramsScope); } -static int +static usymId usymtab_getIndex (/*@notnull@*/ usymtab s, cstring k) { int i; @@ -1405,7 +1411,7 @@ usymtab_getIndex (/*@notnull@*/ usymtab s, cstring k) if (cstringTable_isDefined (s->htable)) { i = cstringTable_lookup (s->htable, k); - return i; + return usymId_fromInt (i); } else { @@ -1418,33 +1424,37 @@ usymtab_getIndex (/*@notnull@*/ usymtab s, cstring k) 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 @@ -1483,16 +1493,16 @@ usymtab_getId (cstring k) /*@globals globtab@*/ 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; @@ -1501,9 +1511,9 @@ usymtab_getId (cstring k) /*@globals globtab@*/ 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)); @@ -1533,13 +1543,12 @@ usymtab_getEntryAux (/*@notnull@*/ usymtab s, usymId 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]); } @@ -1550,7 +1559,7 @@ usymtab_getEntryAux (/*@notnull@*/ usymtab s, usymId uid) } else { - llassert (uid >= 0 && uid < globtab->nentries); + llassert (uid >= 0 && uid < typeId_fromInt (globtab->nentries)); return (globtab->entries[uid]); } } @@ -1559,30 +1568,27 @@ usymtab_getEntryAux (/*@notnull@*/ usymtab s, usymId 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; @@ -1653,12 +1659,16 @@ usymtab_shallowFree (/*@only@*/ /*@notnull@*/ usymtab s) /*@-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; @@ -1679,7 +1689,7 @@ usymId 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); } @@ -2400,7 +2410,7 @@ usymtab_enterFunctionScope (uentry fcn) if (sRef_isUndefGlob (el)) { - int index = sRef_getScopeIndex (el); + usymId index = sRef_getScopeIndex (el); sRef sr = sRef_updateSref (el); fileloc loc = uentry_whereEarliest (fcn); @@ -2845,7 +2855,7 @@ usymtab_exitSwitch (/*@unused@*/ exprNode sw, bool allpaths) { 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)); @@ -3065,7 +3075,7 @@ usymtab_popBranches (exprNode pred, exprNode tbranch, exprNode fbranch, { 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))); @@ -3076,7 +3086,7 @@ usymtab_popBranches (exprNode pred, exprNode tbranch, exprNode fbranch, continue; } - if (tindex != NOT_FOUND) + if (usymtab_indexFound (tindex)) { uentry tthis = ttab->entries[tindex]; @@ -3836,9 +3846,7 @@ checkGlobalReturn (uentry glob, sRef orig) 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; @@ -3866,9 +3874,7 @@ void usymtab_checkFinalScope (bool isReturn) 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; } } @@ -3930,12 +3936,6 @@ void usymtab_checkFinalScope (bool isReturn) 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 @@ -3957,134 +3957,127 @@ void usymtab_checkFinalScope (bool isReturn) } 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)) @@ -4526,7 +4519,7 @@ void usymtab_exitScope (exprNode expr) if (sRef_isCvar (el)) { uentry current; - int index = sRef_getScopeIndex (el); + usymId index = sRef_getScopeIndex (el); if (sRef_isFileStatic (el)) { @@ -4567,15 +4560,15 @@ void usymtab_exitScope (exprNode expr) # 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)) { @@ -4583,15 +4576,15 @@ uentry_directParamNo (uentry 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 @@ -4727,7 +4720,7 @@ static /*@dependent@*/ /*@exposed@*/ usymtab s = usymtab_dropEnv (s); } - if (index >= s->nentries) + if (index >= usymId_fromInt (s->nentries)) { return uentry_undefined; } @@ -4785,7 +4778,6 @@ usymtab_getRefNoisy (/*@notnull@*/ usymtab s, int level, usymId index) while (usymtab_isBranch (s) && s->lexlevel == level) { int eindex = refTable_lookup (s, level, index); - if (eindex != NOT_FOUND) { @@ -4812,7 +4804,7 @@ usymtab_getRefNoisy (/*@notnull@*/ usymtab s, int level, usymId index) s = usymtab_dropEnv (s); } - if (s->lexlevel == level && (index < s->nentries)) + if (s->lexlevel == level && (index < usymId_fromInt (s->nentries))) { ue = s->entries[index]; @@ -4841,7 +4833,7 @@ usymtab_getRefNoisy (/*@notnull@*/ usymtab s, int level, usymId index) } - if (index >= s->nentries) + if (index >= usymId_fromInt (s->nentries)) { return uentry_undefined; } @@ -4859,7 +4851,7 @@ usymtab_getRefNoisy (/*@notnull@*/ usymtab s, int level, usymId index) */ 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; @@ -4868,7 +4860,7 @@ int refTable_lookup (/*@notnull@*/ usymtab ut, int level, int index) 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; } @@ -4891,7 +4883,6 @@ static static /*@dependent@*/ /*@exposed@*/ uentry usymtab_addRefEntry (/*@notnull@*/ usymtab s, cstring k) { - int eindex; usymtab ut = s; if (ut->reftable == NULL) @@ -4904,9 +4895,9 @@ usymtab_addRefEntry (/*@notnull@*/ usymtab s, cstring k) 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]; @@ -4938,7 +4929,7 @@ usymtab_addRefEntry (/*@notnull@*/ usymtab s, cstring k) else { ut->reftable[ut->nentries - 1] - = refentry_create (s->lexlevel, eindex); + = refentry_create (s->lexlevel, usymId_toInt (eindex)); } return (ue); @@ -4961,9 +4952,9 @@ static uentry usymtab_lookupAux (usymtab s, cstring k) 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 @@ -5004,13 +4995,11 @@ static uentry usymtab_lookupAux (usymtab s, cstring k) 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); @@ -5022,7 +5011,7 @@ usymtab_lookupQuietAux (usymtab s, cstring k, bool noalt) } else { - llassert (s != NULL); /*@i523 should not need this? */ + llassert (s != NULL); s = s->env; } } @@ -5114,9 +5103,9 @@ ctype 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; @@ -5128,9 +5117,9 @@ usymtab_lookupType (cstring k) 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; @@ -5393,8 +5382,7 @@ usymtab_freeLevel (/*@notnull@*/ /*@only@*/ usymtab u) } sfree (u); /* evans 2002-07-12: was inside if */ - /*:!!mustfree@*/ -} /*!@=mustfree@*/ +} static void usymtab_freeAux (/*@only@*/ usymtab u) @@ -5418,7 +5406,8 @@ void usymtab_free () 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@*/ { @@ -5449,7 +5438,7 @@ usymtab_replaceEntry (uentry s) } bool -usymtab_matchForwardStruct (usymId u1, usymId u2) +usymtab_matchForwardStruct (typeId u1, typeId u2) /*@globals globtab@*/ { uentry ue1 = usymtab_getTypeEntry (u1); @@ -5469,10 +5458,9 @@ usymtab_matchForwardStruct (usymId u1, usymId u2) 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)))); } } diff --git a/src/usymtab_interface.c b/src/usymtab_interface.c index 9509586..f55a388 100644 --- a/src/usymtab_interface.c +++ b/src/usymtab_interface.c @@ -32,7 +32,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "gram.h" # include "lclscan.h" # include "lclsyntable.h" @@ -863,7 +863,7 @@ declareAbstractType (abstractNode n, bool priv) cstring tn; fileloc loc; uentry ue; - usymId uid; + typeId uid; abstBodyNode ab; if (n == (abstractNode) 0) @@ -949,10 +949,8 @@ declareAbstractType (abstractNode n, bool priv) } } -static void - declareExposedType (exposedNode n, bool priv) +static void declareExposedType (exposedNode n, bool priv) { - usymId uid; qtype c; cstring s; @@ -982,7 +980,7 @@ static void uentry_setDefined (ue, loc); } - uid = usymtab_supExposedTypeEntry (ue, context_inLCLLib () && !priv); + (void) usymtab_supExposedTypeEntry (ue, context_inLCLLib () && !priv); } end_declaratorInvNodeList_elements; qtype_free (c); @@ -1120,7 +1118,7 @@ declareFcnAux (fcnNode f, /*@only@*/ qtype qt, ctype ct, } } - if (usymId_isInvalid (tn)) + if (typeId_isInvalid (tn)) { acct = context_fileAccessTypes (); } diff --git a/src/varDeclarationNodeList.c b/src/varDeclarationNodeList.c index b81d433..e0bfc0e 100644 --- a/src/varDeclarationNodeList.c +++ b/src/varDeclarationNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" varDeclarationNodeList varDeclarationNodeList_new () { diff --git a/src/varNodeList.c b/src/varNodeList.c index d7c21e9..44171a1 100644 --- a/src/varNodeList.c +++ b/src/varNodeList.c @@ -30,7 +30,7 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" varNodeList varNodeList_new () {