From 483f85218f7c0bee824fc41f6456d0643a9e4fe5 Mon Sep 17 00:00:00 2001 From: Mihail Groza Date: Wed, 25 Jan 2017 21:45:28 +0000 Subject: [PATCH] Various minor fixes for compiler/linter (other then splint itself) warnings. Mostly these are adding preprocessor guards to avoid building of unused routines, or to make some routines static. Most of the 'removed' routines are those that print the content of different data types. What is interesting (and a bit worysome) is the fact that some of the routines are memory deallocation routines, letting us assume that at least in some places compound structures are not correctly freed (and memory is lost). Unneeded header inclusion was also handled. Files sRefList.{c,h} are removed, as they weren't used. --- src/Headers/abstBodyNode.h | 2 - src/Headers/abstract.h | 4 - src/Headers/abstractNode.h | 1 - src/Headers/annotationInfo.h | 5 -- src/Headers/annotationTable.h | 18 ----- src/Headers/basic.h | 4 +- src/Headers/clabstract.h | 14 ---- src/Headers/claimNode.h | 1 - src/Headers/constDeclarationNode.h | 2 - src/Headers/constraint.h | 34 +------- src/Headers/constraintExpr.h | 4 - src/Headers/constraintList.h | 7 -- src/Headers/constraintResolve.h | 12 +-- src/Headers/constraintTerm.h | 9 +-- src/Headers/context.h | 25 ------ src/Headers/cpperror.h | 3 - src/Headers/cpplib.h | 40 +--------- src/Headers/cscannerHelp.h | 6 -- src/Headers/cstring.h | 11 +-- src/Headers/cstringHash.h | 2 +- src/Headers/cstringList.h | 10 --- src/Headers/cstringSList.h | 9 --- src/Headers/cstringTable.h | 17 ---- src/Headers/ctypeList.h | 7 -- src/Headers/declaratorInvNode.h | 1 - src/Headers/declaratorInvNodeList.h | 7 -- src/Headers/enumNameList.h | 13 +--- src/Headers/enumSpecNode.h | 3 - src/Headers/exportNode.h | 2 - src/Headers/exposedNode.h | 2 - src/Headers/exprData.h | 19 ++--- src/Headers/exprNode.h | 6 -- src/Headers/exprNodeList.h | 8 +- src/Headers/exprNodeSList.h | 12 +-- src/Headers/fcnNode.h | 9 ++- src/Headers/fcnNodeList.h | 11 +-- src/Headers/fileIdList.h | 5 -- src/Headers/fileLib.h | 1 - src/Headers/fileTable.h | 1 - src/Headers/fileloc.h | 6 -- src/Headers/filelocList.h | 15 +--- src/Headers/filelocStack.h | 7 -- src/Headers/flagMarkerList.h | 8 -- src/Headers/forwardTypes.h | 1 - src/Headers/functionClause.h | 3 - src/Headers/functionClauseList.h | 14 ---- src/Headers/genericTable.h | 17 ---- src/Headers/globSet.h | 2 - src/Headers/globalList.h | 2 - src/Headers/globalsClause.h | 1 - src/Headers/idDecl.h | 5 -- src/Headers/idDeclList.h | 7 -- src/Headers/importNodeList.h | 7 -- src/Headers/initDeclNodeList.h | 7 -- src/Headers/intSet.h | 7 -- src/Headers/interfaceNode.h | 2 - src/Headers/iterNode.h | 2 - src/Headers/lctype.h | 7 +- src/Headers/letDeclNodeList.h | 7 -- src/Headers/lh.h | 1 - src/Headers/llerror.h | 11 --- src/Headers/lslOpList.h | 6 -- src/Headers/lslOpSet.h | 4 - src/Headers/lsymbol.h | 2 - src/Headers/lsymbolSet.h | 4 - src/Headers/macrocache.h | 1 - src/Headers/messageLog.h | 7 -- src/Headers/metaStateConstraintList.h | 11 --- src/Headers/metaStateInfo.h | 14 ---- src/Headers/metaStateTable.h | 6 -- src/Headers/misc.h | 3 - src/Headers/modifiesClause.h | 1 - src/Headers/modifyNode.h | 12 --- src/Headers/mtContextNode.h | 3 - src/Headers/mtDeclarationPiece.h | 2 - src/Headers/mttok.h | 1 - src/Headers/multiVal.h | 1 - src/Headers/opFormNode.h | 2 - src/Headers/osd.h | 2 - src/Headers/privateNode.h | 1 - src/Headers/programNode.h | 1 - src/Headers/qual.h | 5 -- src/Headers/qualList.h | 16 ---- src/Headers/quantifierNode.h | 1 - src/Headers/quantifierNodeList.h | 7 -- src/Headers/reader.h | 2 +- src/Headers/renamingNode.h | 1 - src/Headers/replaceNode.h | 1 - src/Headers/replaceNodeList.h | 7 -- src/Headers/sRef.h | 14 +--- src/Headers/sRefList.h | 63 --------------- src/Headers/sRefSet.h | 8 +- src/Headers/sRefTable.h | 6 -- src/Headers/shift.h | 2 - src/Headers/sigNodeSet.h | 5 +- src/Headers/sort.h | 3 - src/Headers/sortSet.h | 4 - src/Headers/sortSetList.h | 7 -- src/Headers/splintMacros.nf | 19 +---- src/Headers/stateClause.h | 8 -- src/Headers/stateClauseList.h | 6 -- src/Headers/stateInfo.h | 3 - src/Headers/stateValue.h | 6 -- src/Headers/stmtNode.h | 1 - src/Headers/strOrUnionNode.h | 3 - src/Headers/symtable.h | 2 - src/Headers/taggedUnionNode.h | 2 - src/Headers/traitRefNodeList.h | 7 -- src/Headers/typeExpr.h | 6 -- src/Headers/typeNameNodeList.h | 7 -- src/Headers/typeNode.h | 3 - src/Headers/uentry.h | 12 +-- src/Headers/usymtab.h | 7 +- src/Headers/valueTable.h | 6 -- src/Headers/varDeclarationNode.h | 2 - src/Headers/varDeclarationNodeList.h | 7 -- src/Headers/varNode.h | 1 - src/Headers/varNodeList.h | 7 -- src/Makefile.am | 2 - src/abstract.c | 59 +++++++++++--- src/aliasTable.c | 6 +- src/annotationInfo.c | 2 + src/cgrammar.y | 7 +- src/checking.c | 1 - src/clabstract.c | 56 +++---------- src/clause.c | 2 +- src/constraint.c | 88 ++++++++++----------- src/constraintExpr.c | 28 ++----- src/constraintExprData.c | 3 - src/constraintGeneration.c | 31 ++++---- src/constraintList.c | 3 + src/constraintResolve.c | 44 ++++++----- src/constraintTerm.c | 8 +- src/context.c | 16 ++-- src/cpperror.c | 7 +- src/cppexp.c | 5 +- src/cpphash.c | 1 - src/cpplib.c | 61 ++++++++++----- src/cppmain.c | 5 +- src/cscannerHelp.c | 26 +++---- src/cstring.c | 29 +++---- src/cstringList.c | 4 + src/cstringSList.c | 18 +++-- src/cstringTable.c | 10 +++ src/ctbase.i | 12 +-- src/cttable.i | 2 + src/ctype.c | 11 ++- src/ctypeList.c | 8 +- src/declaratorInvNodeList.c | 6 ++ src/enumNameList.c | 6 ++ src/exprChecks.c | 7 +- src/exprData.c | 6 +- src/exprNode.c | 70 +++-------------- src/exprNodeList.c | 3 + src/exprNodeSList.c | 7 +- src/fcnNodeList.c | 5 ++ src/fileLib.c | 7 +- src/fileTable.c | 5 +- src/fileloc.c | 2 + src/filelocList.c | 6 +- src/filelocStack.c | 10 +-- src/flagMarkerList.c | 6 +- src/functionClause.c | 6 ++ src/functionClauseList.c | 34 ++++---- src/genericTable.c | 13 ++++ src/globSet.c | 4 + src/globalsClause.c | 2 + src/help.c | 1 - src/idDecl.c | 2 +- src/idDeclList.c | 5 ++ src/importNodeList.c | 5 ++ src/imports.c | 6 -- src/initDeclNodeList.c | 5 ++ src/intSet.c | 7 ++ src/lclinit.c | 2 - src/lcllib.c | 5 +- src/lclscanline.c | 3 +- src/letDeclNodeList.c | 5 ++ src/lh.c | 10 --- src/llerror.c | 10 ++- src/llmain.c | 7 +- src/loopHeuristics.c | 4 - src/lslOpList.c | 5 ++ src/lslOpSet.c | 6 +- src/lslinit.c | 2 - src/lslparse.c | 5 -- src/lsltokentable.c | 1 - src/lsymbol.c | 2 + src/lsymbolSet.c | 5 ++ src/macrocache.c | 3 +- src/messageLog.c | 5 ++ src/metaStateConstraintList.c | 16 ++-- src/metaStateInfo.c | 4 + src/misc.c | 4 + src/modifiesClause.c | 2 + src/mtContextNode.c | 6 +- src/mtDeclarationNode.c | 3 + src/mtDeclarationPiece.c | 4 + src/mttok.c | 2 + src/multiVal.c | 2 + src/nameChecks.c | 6 +- src/osd.c | 3 +- src/programNodeList.c | 2 + src/qual.c | 2 + src/qualList.c | 6 +- src/quantifierNodeList.c | 6 ++ src/reader.c | 2 +- src/replaceNodeList.c | 5 ++ src/sRef.c | 54 +++++++------ src/sRefList.c | 143 ---------------------------------- src/sRefSet.c | 7 ++ src/sRefTable.c | 5 ++ src/shift.c | 8 -- src/sigNodeSet.c | 5 ++ src/sort.c | 12 +-- src/sortSet.c | 5 ++ src/sortSetList.c | 5 ++ src/stateClause.c | 20 ++--- src/stateClauseList.c | 7 +- src/stateInfo.c | 33 +++----- src/stateValue.c | 8 +- src/symtable.c | 7 +- src/traitRefNodeList.c | 5 ++ src/typeNameNodeList.c | 5 ++ src/uentry.c | 21 +++-- src/usymtab.c | 12 ++- src/usymtab_interface.c | 3 - src/varDeclarationNodeList.c | 5 ++ src/varNodeList.c | 5 ++ 229 files changed, 710 insertions(+), 1448 deletions(-) delete mode 100644 src/Headers/sRefList.h delete mode 100644 src/sRefList.c diff --git a/src/Headers/abstBodyNode.h b/src/Headers/abstBodyNode.h index 1c80c19..d1cec26 100644 --- a/src/Headers/abstBodyNode.h +++ b/src/Headers/abstBodyNode.h @@ -10,5 +10,3 @@ struct s_abstBodyNode { fcnNodeList fcns; /* only for abstBody, not for optExposedBody */ } ; -extern /*@unused@*/ /*@only@*/ cstring abstBodyNode_unparse (abstBodyNode p_n); - diff --git a/src/Headers/abstract.h b/src/Headers/abstract.h index 55052dd..c26f6f4 100644 --- a/src/Headers/abstract.h +++ b/src/Headers/abstract.h @@ -164,8 +164,6 @@ extern /*@only@*/ lslOp makelslOpNode (/*@only@*/ /*@null@*/ nameNode p_name, /*@dependent@*/ sigNode p_s); -extern /*@only@*/ cstring lslOp_unparse (lslOp p_x); - /*@notfunction@*/ # define MASH(x,y) \ (/*@+enumint@*/ (((unsigned) ((x)+1) << 1) + (y)) & HT_MAXINDEX /*@=enumint@*/) @@ -293,8 +291,6 @@ extern /*@only@*/ abstractNode bool p_isMutable, bool p_isRefCounted, /*@only@*/ abstBodyNode p_a); -extern /*@unused@*/ /*@only@*/ cstring abstBodyNode_unparseExposed (abstBodyNode p_n); - extern /*@only@*/ exposedNode makeExposedNode (/*@only@*/ ltoken p_t, /*@only@*/ lclTypeSpecNode p_s, /*@only@*/ declaratorInvNodeList p_d); diff --git a/src/Headers/abstractNode.h b/src/Headers/abstractNode.h index 88a69bf..3a9daa7 100644 --- a/src/Headers/abstractNode.h +++ b/src/Headers/abstractNode.h @@ -13,4 +13,3 @@ typedef struct { abstBodyNode body; } *abstractNode; -extern /*@unused@*/ /*@only@*/ cstring abstractNode_unparse(abstractNode p_n); diff --git a/src/Headers/annotationInfo.h b/src/Headers/annotationInfo.h index d88066c..be497e6 100644 --- a/src/Headers/annotationInfo.h +++ b/src/Headers/annotationInfo.h @@ -56,12 +56,7 @@ extern void annotationInfo_free (/*@only@*/ annotationInfo) ; extern /*@observer@*/ cstring annotationInfo_dump (annotationInfo) ; extern /*@observer@*/ annotationInfo annotationInfo_undump (char **p_s) /*@modifies *p_s@*/ ; -extern void annotationInfo_showContextRefError (annotationInfo, sRef) /*@*/ ; - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/annotationTable.h b/src/Headers/annotationTable.h index 96c2f26..63fae87 100644 --- a/src/Headers/annotationTable.h +++ b/src/Headers/annotationTable.h @@ -18,15 +18,6 @@ # ifndef ANNOTTABLE_H # define ANNOTTABLE_H -/*@constant null annotationTable annotationTable_undefined; @*/ -# define annotationTable_undefined genericTable_undefined - -extern /*@falsewhennull@*/ bool annotationTable_isDefined(annotationTable) /*@*/ ; -# define annotationTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) - -extern /*@nullwhentrue@*/ bool annotationTable_isUndefined(annotationTable) /*@*/ ; -# define annotationTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) - /*@constant int DEFAULT_ANNOTTABLE_SIZE@*/ # define DEFAULT_ANNOTTABLE_SIZE 32 @@ -46,9 +37,6 @@ extern bool annotationTable_contains (annotationTable p_h, cstring p_key) /*@*/ # define annotationTable_contains(p_h,p_key) \ (genericTable_contains ((genericTable) (p_h), p_key)) -extern /*@unused@*/ /*@only@*/ cstring annotationTable_stats(annotationTable p_h); -# define annotationTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) - extern /*@only@*/ cstring annotationTable_unparse (annotationTable p_h); extern void annotationTable_free (/*@only@*/ annotationTable p_h); @@ -62,13 +50,7 @@ extern void annotationTable_free (/*@only@*/ annotationTable p_h); genericTable_elements((genericTable) (p_g), m_key, m_el) # define end_annotationTable_elements end_genericTable_elements -extern int annotationTable_size (annotationTable p_h); -# define annotationTable_size(p_h) (genericTable_size(p_h)) - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/basic.h b/src/Headers/basic.h index 12fe587..77584d2 100644 --- a/src/Headers/basic.h +++ b/src/Headers/basic.h @@ -40,7 +40,6 @@ # include "flag_codes.h" # include "flags.h" # include "flagSpec.h" -# include "cpp.h" # include "qual.h" # include "lltok.h" # include "clause.h" @@ -76,7 +75,6 @@ # include "usymId.h" # include "typeId.h" # include "usymIdSet.h" -# include "sRefList.h" # include "uentryList.h" # include "globSet.h" # include "ctypeList.h" @@ -99,6 +97,8 @@ # include "constraintExprData.h" # include "constraintExpr.h" # include "constraint.h" +# include "constraintResolve.h" +# include "constraintOutput.h" # include "constraintList.h" # include "exprNode.h" # include "exprData.h" diff --git a/src/Headers/clabstract.h b/src/Headers/clabstract.h index afa1455..5911836 100644 --- a/src/Headers/clabstract.h +++ b/src/Headers/clabstract.h @@ -59,8 +59,6 @@ extern void setProcessingIterVars (uentry p_iter); extern void setProcessingTypedef (/*@only@*/ qtype p_q); extern void setProcessingVars (/*@only@*/ qtype p_q); extern void setStorageClass (storageClassCode p_sc); -extern void storeLoc (void); -extern void unsetProcessingTypedef (void); extern void unsetProcessingVars (void); extern /*@only@*/ uentry makeCurrentParam (idDecl p_t); @@ -78,11 +76,6 @@ extern void checkDoneParams (void); extern void exitParamsTemp (void); extern void enterParamsTemp (void); -extern void clearProcessingGlobMods (void); -extern bool isProcessingGlobMods (void); -extern void setProcessingGlobMods (void); - -extern void setFunctionNoGlobals (void); extern int iterParamNo (void); extern void nextIterParam (void); extern void declareCIter (cstring p_name, /*@owned@*/ uentryList p_params); @@ -116,10 +109,3 @@ extern void clabstract_initMod (void) /*@modifies internalState@*/ ; # error "Multiple include" # endif - - - - - - - diff --git a/src/Headers/claimNode.h b/src/Headers/claimNode.h index f3bb375..0395d46 100644 --- a/src/Headers/claimNode.h +++ b/src/Headers/claimNode.h @@ -14,4 +14,3 @@ typedef struct { /*@null@*/ lclPredicateNode ensures; } *claimNode; -extern /*@unused@*/ /*@only@*/ cstring claimNode_unparse (claimNode p_c); diff --git a/src/Headers/constDeclarationNode.h b/src/Headers/constDeclarationNode.h index bee1b27..47db0aa 100644 --- a/src/Headers/constDeclarationNode.h +++ b/src/Headers/constDeclarationNode.h @@ -9,5 +9,3 @@ typedef struct { initDeclNodeList decls; } *constDeclarationNode; -extern /*@unused@*/ /*@only@*/ cstring - constDeclarationNode_unparse (/*@null@*/ constDeclarationNode p_x); diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 269aefc..5964d65 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -1,6 +1,5 @@ -#ifndef __constraint_h__ - -#define __constraint_h__ +#ifndef CONSTRAINT_H +#define CONSTRAINT_H typedef enum { @@ -50,15 +49,8 @@ extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@observer@*/ exprNode p_t1, /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint); -extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) - /*@modifies p_c1 @*/; - extern /*@only@*/ constraint constraint_copy (/*@temp@*/ constraint p_c); -extern bool fileloc_closer (/*@observer@*/ fileloc p_loc1, - /*@observer@*/ fileloc p_loc2, - /*@observer@*/ fileloc p_loc3) /*@*/; - extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/; extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c); @@ -77,8 +69,6 @@ extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@obse extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint); extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/; -extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition, - exprNodeList p_arglist); extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); @@ -110,25 +100,14 @@ extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, / extern bool constraint_hasMaxSet(constraint p_c); -/*from constraintGenreation.c*/ -extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint); - -extern /*@only@*/ constraintList -exprNode_traverseRequiresConstraints (exprNode p_e); - -extern /*@only@*/ constraintList -exprNode_traverseEnsuresConstraints (exprNode p_e); - extern constraint constraint_togglePost (/*@returned@*/ constraint p_c); extern bool constraint_same (constraint p_c1, constraint p_c2) ; extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ; -extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/ - extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ; extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ; -extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ; +extern void exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ; constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c); bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c); @@ -155,17 +134,10 @@ void exprNode_findValue( exprNode p_e); /*drl added 12/30/01 */ /* extern / *@only@* / constraint constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */ -/*drl added 12/19 */ -bool constraint_isConstantOnly (constraint p_c); /*@=czechfcns*/ /* drl possible problem : warning take this out */ -#include "constraintResolve.h" -#include "constraintOutput.h" - #else - #error Multiple include - #endif diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h index a3d262f..140530f 100644 --- a/src/Headers/constraintExpr.h +++ b/src/Headers/constraintExpr.h @@ -78,8 +78,6 @@ bool constraintExpr_search (/*@observer@*/ /*@temp@*/ constraintExpr p_c, /*@obs /*@only@*/ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef p_s); -constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr p_expr, exprNodeList p_arglist); - /*@only@*/ constraintExpr constraintExpr_makeExprNode (/*@dependent@*/ exprNode p_e); /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr p_expr, /*@observer@*/ exprNode p_fcnCall); @@ -111,8 +109,6 @@ extern void constraintExpr_dump (/*@observer@*/ /*@temp@*/ constraintExpr p_exp extern /*@only@*/ constraintExpr constraintExpr_undump (FILE *p_f); -extern /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode p_e) ; - /* drl added 8/8/001*/ bool constraintExpr_isTerm (/*@observer@*/ /*@temp@*/ constraintExpr p_c); diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index 5c826c9..bf7b71d 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -68,14 +68,10 @@ extern constraintList constraintList_preserveOrig (/*@returned@*/ constraintList # define constraintListBASESIZE SMALLBASESIZE -extern /*@only@*/ constraintList constraintList_doSRefFixBaseParam ( constraintList p_preconditions, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_preconditions@*/; - extern constraintList constraintList_togglePost (/*@returned@*/ constraintList p_c) /*@modifies p_c@*/; extern /*@only@*/ constraintList constraintList_doSRefFixConstraintParam ( /*@only@*/ constraintList p_preconditions, /*@observer@*/ /*@temp@*/ exprNodeList p_arglist) /*@modifies p_preconditions@*/; -extern constraintList exprNode_getPostConditions (/*@dependent@*/ /*@observer@*/ exprNode p_fcn, exprNodeList p_arglist, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall) /*@*/; - /*@only@*/ constraintList constraintList_doFixResult ( /*@only@*/ constraintList p_postconditions, /*@observer@*/ /*@dependent@*/ exprNode p_fcnCall) /*@modifies p_postconditions@*/; extern constraintList constraintList_addGeneratingExpr (/*@returned@*/ constraintList p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) /*@modifies p_c@*/; @@ -99,6 +95,3 @@ extern void constraintList_dump (/*@observer@*/ constraintList p_c, FILE * p_f) # error "Multiple include" # endif - - - diff --git a/src/Headers/constraintResolve.h b/src/Headers/constraintResolve.h index 5a28ef9..9e81dc7 100644 --- a/src/Headers/constraintResolve.h +++ b/src/Headers/constraintResolve.h @@ -1,3 +1,5 @@ +# ifndef CONSTRAINT_RESOLVE_H +# define CONSTRAINT_RESOLVE_H extern /*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ /*@temp@*/ constraintList p_pre2, /*@observer@*/ /*@temp@*/ constraintList p_post1); @@ -13,10 +15,6 @@ extern bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint p_c, / extern constraint constraint_simplify ( /*@returned@*/ constraint p_c); -extern /*@only@*/ constraintList constraintList_fixConflicts (constraintList p_list1, constraintList p_list2); - -extern constraintList constraintList_subsumeEnsures (constraintList p_list1, constraintList p_list2); - extern constraintList constraintList_mergeEnsures (/*observer@*/ /*@temp@*/ constraintList p_list1, /*@observer@*/ /*@temp@*/ constraintList p_list2); /*@only@*/ constraintList constraintList_mergeEnsuresFreeFirst (/*@only@*/ constraintList p_list1, /*@observer@*/ /*@temp@*/ constraintList p_list2); @@ -32,9 +30,11 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint p_c); constraintList constraintList_reflectChangesOr (constraintList p_pre2, constraintList p_post1); -/*@only@*/ constraintList constraintList_substitute (constraintList p_target, /*2observer@*/ constraintList p_subList); - /*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList p_target, /*@observer@*/ /*@temp@*/ constraintList p_subList); extern void exprNode_mergeResolve (exprNode p_parent, exprNode p_child1, exprNode p_child2); +# else +# error "Multiple include" +# endif + diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h index 1ecd622..fa47a02 100644 --- a/src/Headers/constraintTerm.h +++ b/src/Headers/constraintTerm.h @@ -1,6 +1,5 @@ -#ifndef __constraintTerm_h__ - -#define __constraintTerm_h__ +#ifndef CONSTRAINT_TERM_H +#define CONSTRAINT_TERM_H typedef union { @@ -51,8 +50,6 @@ extern bool constraintTerm_isIntLiteral (constraintTerm p_term) /*@*/; extern constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef p_s) /*@*/; -/*@unused@*/ bool constraintTerm_probSame (constraintTerm p_term1, constraintTerm p_term2) /*@*/; - constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm p_term, fileloc p_loc) /*@modifies p_term@*/; constraintTerm constraintTerm_makeIntLiteral (long p_i) /*@*/; @@ -61,8 +58,6 @@ bool constraintTerm_isStringLiteral (constraintTerm p_c) /*@*/; cstring constraintTerm_getStringLiteral (constraintTerm p_c) /*@*/; -constraintTerm constraintTerm_doSRefFixBaseParam (/*@returned@*/ constraintTerm p_term, exprNodeList p_arglist) /*@modifies p_term@*/; - extern cstring constraintTerm_unparse (constraintTerm) /*@*/ ; extern void constraintTerm_dump ( /*@observer@*/ constraintTerm p_t, FILE * p_f); diff --git a/src/Headers/context.h b/src/Headers/context.h index 546ee56..6a06ad3 100644 --- a/src/Headers/context.h +++ b/src/Headers/context.h @@ -18,8 +18,6 @@ extern bool context_doDump (void); extern void context_resetAllFlags (void); -extern /*@unused@*/ cstring context_unparseFlagMarkers (void) /*@*/ ; - extern void context_enterDoWhileClause (void) /*@modifies internalState@*/ ; extern bool context_hasMods (void); @@ -89,9 +87,6 @@ extern bool context_inProtectVars (void); extern bool context_hasFileAccess (typeId p_t); -extern void context_hideShowscan (void); -extern void context_unhideShowscan (void); - extern void context_setMode (cstring p_s); extern void context_setModeNoWarn (cstring p_s); extern void context_exitAllClauses (void); @@ -145,8 +140,6 @@ extern /*@only@*/ cstring context_unparse (void) /*@*/ ; extern void context_setFunctionDefined (fileloc p_loc); extern void context_setFlagTemp (flagcode p_f, bool p_b); -extern /*@unused@*/ void context_showFilelocStack (void) ; - extern bool context_getFlag (flagcode p_d) /*@*/ ; extern bool context_flagOn (flagcode p_f, fileloc p_loc) /*@*/ ; @@ -163,12 +156,6 @@ extern int context_getValue (flagcode p_flag) /*@*/ ; extern void context_setValueAndFlag (flagcode p_flag, int p_val) /*@modifies internalState@*/ ; -extern /*@unused@*/ int context_getCounter (flagcode p_flag) /*@*/ ; -extern /*@unused@*/ void context_incCounter (flagcode p_flag) - /*@modifies internalState@*/ ; -extern /*@unused@*/ void context_decCounter (flagcode p_flag) - /*@modifies internalState@*/ ; - extern bool context_maybeSet (flagcode p_d) /*@*/ ; extern /*@observer@*/ cstring context_getString (flagcode p_flag) /*@*/ ; @@ -203,7 +190,6 @@ extern void context_setFilename(fileId p_fid, int p_lineno) extern void context_fileSetFlag (flagcode p_f, ynm p_set, fileloc p_loc); -extern /*@unused@*/ /*@only@*/ cstring context_unparseAccess (void) /*@*/ ; extern bool context_inFunction(void) /*@*/ ; extern bool context_inFunctionLike (void) /*@*/ ; @@ -315,7 +301,6 @@ extern bool context_inFunctionHeader (void) /*@globals internalState@*/ ; extern void context_enterFunctionHeader (void) /*@modifies internalState@*/ ; extern void context_exitFunctionHeader (void) /*@modifies internalState@*/ ; -extern bool context_inFunctionDeclaration (void) /*@globals internalState@*/ ; extern void context_enterFunctionDeclaration (/*@exposed@*/ uentry) /*@modifies internalState@*/ ; extern void context_exitFunctionDeclaration (void) /*@modifies internalState@*/ ; extern void context_enterOldStyleScope (void) /*@modifies internalState@*/ ; @@ -325,9 +310,6 @@ extern ctype context_boolImplementationType (void) /*@*/ ; extern /*@observer@*/ /*@null@*/ annotationInfo context_lookupAnnotation (cstring p_annot) /*@*/ ; -extern /*@observer@*/ metaStateTable context_getMetaStateTable (void) - /*@globals internalState@*/ ; - extern /*@observer@*/ metaStateInfo context_lookupMetaStateInfo (cstring p_key) /*@globals internalState@*/ ; @@ -360,10 +342,3 @@ extern void context_leaveSizeof (void); # error "Multiple include" # endif - - - - - - - diff --git a/src/Headers/cpperror.h b/src/Headers/cpperror.h index caa2ab1..2af9326 100644 --- a/src/Headers/cpperror.h +++ b/src/Headers/cpperror.h @@ -4,9 +4,6 @@ /* doesn't exit! */ extern void cppReader_fatalError (cppReader *p_pfile, /*@only@*/ cstring p_str); -extern /*@noreturn@*/ void cppReader_pfatalWithName (cppReader *p_pfile, - cstring p_name); - extern void cppReader_errorLit (cppReader *p_pfile, /*@observer@*/ cstring p_msg); extern void diff --git a/src/Headers/cpplib.h b/src/Headers/cpplib.h index 783d2a2..5bf594f 100644 --- a/src/Headers/cpplib.h +++ b/src/Headers/cpplib.h @@ -23,10 +23,6 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # ifndef CPPLIB_H # define CPPLIB_H -#ifdef __cplusplus -extern "C" { -#endif - typedef struct cppReader cppReader; typedef struct cppBuffer cppBuffer; typedef struct cppOptions cppOptions; @@ -236,11 +232,6 @@ extern bool cpplib_fatalErrors (cppReader *) /*@*/ ; extern int cpplib_bufPeek (cppBuffer *) /*@*/ ; -/* Macros for manipulating the token_buffer. */ - -/*@notfunction@*/ -#define CPP_OUT_BUFFER(PFILE) ((PFILE)->token_buffer) - /* Number of characters currently in PFILE's output buffer. */ extern size_t cpplib_getWritten (/*@sef@*/ cppReader *) /*@*/ ; @@ -250,26 +241,12 @@ extern size_t cpplib_getWritten (/*@sef@*/ cppReader *) /*@*/ ; extern /*@exposed@*/ char *cpplib_getPWritten (cppReader *) /*@*/ ; # define cpplib_getPWritten(PFILE) ((PFILE)->limit) +# if 0 extern /*@null@*/ macroDef cpplib_createDefinition (/*@dependent@*/ cstring p_def, fileloc p_loc, bool p_predefinition, bool p_noExpand) ; +# endif -/* Make sure PFILE->token_buffer has space for at least N more characters. */ - -extern void cpplib_reserve (/*@sef@*/ cppReader *, /*@sef@*/ size_t); -#define cpplib_reserve(PFILE, N) \ - (((cpplib_getWritten (PFILE) + (N) > (PFILE)->token_buffer_size)) ? cppReader_growBuffer (PFILE, (N)) : (void) 0) - -/* Append string STR (of length N) to PFILE's output buffer. - Assume there is enough space. */ - -extern void cppReader_putStrN (/*@sef@*/ cppReader *p_file, - /*@unique@*/ char *p_str, /*@sef@*/ size_t p_n) - /*@modifies *p_file; @*/; - -#define cppReader_putStrN(PFILE, STR, N) \ - (memcpy ((PFILE)->limit, STR, (N)), (PFILE)->limit += (N)) - extern void cppReader_setWritten (/*@sef@*/ /*@special@*/ cppReader *p_file, size_t) /*@uses p_file, *p_file, p_file->token_buffer;@*/ /*@sets p_file->limit;@*/ @@ -546,7 +523,6 @@ extern void cppBuffer_getLineAndColumn (/*@null@*/ cppBuffer *, /*@out@*/ int *, /*@out@*/ /*@null@*/ int *); extern /*@exposed@*/ /*@null@*/ cppBuffer *cppReader_fileBuffer (cppReader *); -extern void cppReader_growBuffer (cppReader *, size_t); extern int cppReader_parseEscape (cppReader *, char **); extern /*@exposed@*/ cppBuffer *cppReader_popBuffer (cppReader *p_pfile) @@ -570,25 +546,13 @@ struct file_name_list bool got_name_map; }; -extern void cppReader_define (cppReader *p_pfile, char *p_str); extern void cppReader_finish (cppReader *p_pfile); -extern void cpplib_init (/*@out@*/ cppReader *p_pfile) ; -extern void cppOptions_init (/*@out@*/ cppOptions *p_opts); extern void cpplib_initializeReader (cppReader *p_pfile, cstringList *cmdArgs) /*@modifies p_pfile@*/ ; extern int cppReader_startProcess (cppReader *p_pfile, cstring p_fname); extern bool isIdentifierChar (char) /*@*/ ; - -extern size_t cppReader_checkMacroName (cppReader *p_pfile, char *p_symname, - cstring p_usage); - -extern struct operation cppReader_parseNumber (cppReader * p_pfile, char * p_start, int p_olen) /*@requires maxRead(p_start) >= (p_olen - 1) @*/; -#ifdef __cplusplus -} -#endif - # else # error "Multiple include" # endif diff --git a/src/Headers/cscannerHelp.h b/src/Headers/cscannerHelp.h index 1431a12..d47ceac 100644 --- a/src/Headers/cscannerHelp.h +++ b/src/Headers/cscannerHelp.h @@ -44,19 +44,15 @@ extern int cscannerHelp_returnExpr (/*@only@*/ exprNode p_e) extern void cscannerHelp_setTokLength (int) /*@modifies g_currentloc, internalState@*/ ; extern void cscannerHelp_setTokLengthT (size_t) /*@modifies g_currentloc, internalState@*/ ; -extern void cscannerHelp_advanceLine (void) /*@modifies g_currentloc, internalState@*/ ; extern /*@observer@*/ cstring cscannerHelp_observeLastIdentifier (void) ; extern int cscannerHelp_handleLlSpecial (void) /*@modifies g_currentloc, internalState@*/ ; extern bool cscannerHelp_handleSpecial (char *) /*@modifies g_currentloc, internalState@*/ ; extern /*@only@*/ cstring cscannerHelp_makeIdentifier (char *); -extern bool cscannerHelp_isConstraintToken (int p_tok) /*@*/ ; - extern int cscannerHelp_handleNewLine (void) /*@modifies g_currentloc, internalState@*/ ; extern int cscannerHelp_processTextIdentifier (char *) /*@modifies internalState@*/ ; -extern int cscannerHelp_processIdentifier (/*@only@*/ cstring) /*@modifies internalState@*/ ; extern bool cscannerHelp_processHashIdentifier (/*@only@*/ cstring) /*@modifies internalState@*/ ; extern int cscannerHelp_processSpec (int p_tok) /*@modifies internalState@*/ ; @@ -79,7 +75,6 @@ extern /*@observer@*/ uentry cscannerHelp_coerceIterId (cstring p_cn); extern void cscannerHelp_setExpectingTypeName (void) /*@modifies internalState@*/ ; extern void cscannerHelp_clearExpectingTypeName (void) /*@modifies internalState@*/ ; -extern bool cscannerHelp_isExpectingTypeName (void) /*@globals internalState@*/ ; extern int cscannerHelp_ninput (void) /*@modifies internalState, g_currentloc@*/; @@ -87,4 +82,3 @@ extern int cscannerHelp_ninput (void) /*@modifies internalState, g_currentloc@*/ # error "Multiple include." # endif - diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h index 173546b..a31227e 100644 --- a/src/Headers/cstring.h +++ b/src/Headers/cstring.h @@ -44,7 +44,7 @@ extern cmpcode cstring_genericEqual (cstring p_s, cstring p_t, /* evans 2001-09-09 - removed conditional compilation on this (for WIN32, OS2) */ extern void cstring_replaceAll (cstring p_s, char p_old, char p_snew) /*@modifies p_s@*/ ; -extern void cstring_replaceLit (/*@unique@*/ cstring p_s, char *p_old, char *p_snew) +extern void cstring_replaceLit (/*@unique@*/ cstring p_s, const char *p_old, const char *p_snew) /*@modifies p_s@*/ /*@requires maxRead(p_snew) >= 0 /\ maxRead(p_old) >= 0 /\ maxRead(p_old) >= maxRead(p_snew) @*/; @@ -76,8 +76,6 @@ extern bool cstring_equalLit (cstring p_c1, char *p_c2) /*@*/ ; extern int cstring_compare (cstring p_c1, cstring p_c2) /*@*/ ; extern int cstring_xcompare (cstring *p_c1, cstring *p_c2) /*@*/ ; -extern bool cstring_hasNonAlphaNumBar (cstring p_s) /*@*/ ; - extern cstring cstring_elide (cstring p_s, size_t p_len) /*@*/ ; extern cstring cstring_clip (/*@returned@*/ cstring p_s, size_t p_len) @@ -85,10 +83,7 @@ extern cstring cstring_clip (/*@returned@*/ cstring p_s, size_t p_len) extern void cstring_stripChars (cstring p_s, const char *p_clist) /*@modifies p_s@*/ ; -extern /*@dependent@*/ cstring - cstring_bsearch (cstring p_key, - char **p_table, - int p_nentries); +extern bool cstring_bsearch (cstring p_key, const char **p_table, int p_nentries); extern bool cstring_lessthan (cstring p_s1, cstring p_s2) /*@*/ ; # define cstring_lessthan(s1, s2) (cstring_compare (s1, s2) < 0) @@ -221,5 +216,3 @@ cstring cstring_replaceChar(/*@returned@*/ cstring p_c, char p_oldChar, char p_n # error "Multiple include" # endif - - diff --git a/src/Headers/cstringHash.h b/src/Headers/cstringHash.h index fa4be32..4e4c3ae 100644 --- a/src/Headers/cstringHash.h +++ b/src/Headers/cstringHash.h @@ -6,7 +6,7 @@ # ifndef CSTRINGHASH_H # define CSTRINGHASH_H -unsigned int cstring_hashValue (cstring key); +extern unsigned int cstring_hashValue (cstring key); # else # error "Multiple include" diff --git a/src/Headers/cstringList.h b/src/Headers/cstringList.h index d27873d..63b559b 100644 --- a/src/Headers/cstringList.h +++ b/src/Headers/cstringList.h @@ -22,9 +22,6 @@ extern /*@falsewhennull@*/ bool cstringList_isDefined (cstringList p_s) /*@*/ ; extern int cstringList_size (/*@sef@*/ cstringList) /*@*/ ; # define cstringList_size(s) (cstringList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsewhennull@*/ bool cstringList_empty (/*@sef@*/ cstringList) /*@*/ ; -# define cstringList_empty(s) (cstringList_size(s) == 0) - extern cstring cstringList_unparseSep (cstringList p_s, cstring p_sep) /*@*/ ; extern /*@exposed@*/ /*@null@*/ ob_cstring *cstringList_getElements (cstringList) /*@*/ ; @@ -46,13 +43,9 @@ extern bool cstringList_contains (cstringList p_s, cstring p_key) /*@*/ ; extern int cstringList_getIndex (cstringList p_s, cstring p_key) /*@*/ ; extern /*@observer@*/ cstring cstringList_get (cstringList p_s, int p_index) /*@*/ ; -extern /*@unused@*/ void cstringList_alphabetize (cstringList p_s); -extern /*@unused@*/ /*@only@*/ cstring cstringList_unparseAbbrev (cstringList p_s) /*@*/ ; extern /*@unused@*/ /*@only@*/ cstring cstringList_unparse (cstringList p_s) ; extern void cstringList_free (/*@only@*/ cstringList p_s) ; -extern /*@unused@*/ void cstringList_printSpaced (cstringList p_s, size_t p_indent, size_t p_gap, int p_linelen); - extern /*@only@*/ cstringList cstringList_copy (cstringList p_s) /*@*/ ; /*@constant int cstringListBASESIZE;@*/ @@ -71,6 +64,3 @@ extern /*@only@*/ cstringList cstringList_copy (cstringList p_s) /*@*/ ; # error "Multiple include" # endif - - - diff --git a/src/Headers/cstringSList.h b/src/Headers/cstringSList.h index c8f75a2..8986f48 100644 --- a/src/Headers/cstringSList.h +++ b/src/Headers/cstringSList.h @@ -27,20 +27,14 @@ extern int cstringSList_size (/*@sef@*/ cstringSList) /*@*/ ; extern /*@falsewhennull@*/ bool cstringSList_empty (/*@sef@*/ cstringSList) /*@*/ ; # define cstringSList_empty(s) (cstringSList_size(s) == 0) -extern /*@unused@*/ cstring cstringSList_unparseSep (cstringSList p_s, cstring p_sep) /*@*/ ; - extern /*@only@*/ cstringSList cstringSList_new (void) /*@*/ ; -extern /*@unused@*/ /*@only@*/ cstringSList cstringSList_single (/*@exposed@*/ cstring p_el) /*@*/ ; - extern cstringSList cstringSList_add (/*@returned@*/ cstringSList p_s, /*@exposed@*/ cstring p_el) /*@modifies p_s@*/ ; extern void cstringSList_alphabetize (cstringSList p_s); -extern /*@observer@*/ cstring cstringSList_get (cstringSList p_s, int p_index) /*@*/ ; - extern /*@only@*/ cstring cstringSList_unparseAbbrev (cstringSList p_s) /*@*/ ; extern /*@unused@*/ /*@only@*/ cstring cstringSList_unparse (cstringSList p_s) /*@*/ ; extern void cstringSList_free (/*@only@*/ cstringSList p_s) ; @@ -63,6 +57,3 @@ extern void cstringSList_printSpaced (cstringSList p_s, size_t p_indent, size_t # error "Multiple include" # endif - - - diff --git a/src/Headers/cstringTable.h b/src/Headers/cstringTable.h index a08f4c9..638e1be 100644 --- a/src/Headers/cstringTable.h +++ b/src/Headers/cstringTable.h @@ -60,14 +60,9 @@ extern void cstringTable_insert (cstringTable p_h, int p_value) /*@modifies p_h@*/ ; extern int cstringTable_lookup (cstringTable p_h, cstring p_key); -extern /*@unused@*/ /*@only@*/ cstring cstringTable_stats(cstringTable p_h); extern void cstringTable_free (/*@only@*/ cstringTable p_h); extern void cstringTable_remove (cstringTable p_h, cstring p_key) /*@modifies p_h@*/ ; -extern /*@unused@*/ cstring cstringTable_unparse (cstringTable) /*@*/ ; - -extern /*@unused@*/ void cstringTable_update (cstringTable p_h, cstring p_key, int p_newval) /*@modifies p_h@*/ ; - extern void cstringTable_replaceKey (cstringTable p_h, cstring p_oldkey, /*@only@*/ cstring p_newkey); @@ -76,15 +71,3 @@ extern void # error "Multiple include" # endif - - - - - - - - - - - - diff --git a/src/Headers/ctypeList.h b/src/Headers/ctypeList.h index d7e66ec..643b882 100644 --- a/src/Headers/ctypeList.h +++ b/src/Headers/ctypeList.h @@ -26,13 +26,6 @@ extern int ctypeList_size (/*@sef@*/ ctypeList p_s) /*@*/ ; extern /*@only@*/ ctypeList ctypeList_new(void); extern void ctypeList_addh (ctypeList p_s, ctype p_el) /*@modifies p_s@*/; -extern /*@only@*/ ctypeList - ctypeList_append (/*@returned@*/ /*@only@*/ ctypeList p_s1, - ctypeList p_s2) /*@modifies p_s1@*/ ; - -extern ctypeList ctypeList_add (/*@only@*/ ctypeList p_s, ctype p_el) /*@modifies p_s@*/; - -extern /*@unused@*/ /*@only@*/ cstring ctypeList_unparse (ctypeList) /*@*/ ; extern void ctypeList_free (/*@only@*/ /*@only@*/ ctypeList p_s) /*@modifies p_s@*/; extern /*@falsewhennull@*/ bool ctypeList_isDefined (/*@null@*/ ctypeList p_ct) /*@*/ ; diff --git a/src/Headers/declaratorInvNode.h b/src/Headers/declaratorInvNode.h index c913139..bb694ef 100644 --- a/src/Headers/declaratorInvNode.h +++ b/src/Headers/declaratorInvNode.h @@ -13,5 +13,4 @@ typedef struct { } *declaratorInvNode; extern void declaratorInvNode_free (/*@only@*/ /*@null@*/ declaratorInvNode p_x); -extern /*@only@*/ cstring declaratorInvNode_unparse (declaratorInvNode p_d); diff --git a/src/Headers/declaratorInvNodeList.h b/src/Headers/declaratorInvNodeList.h index 2678f65..6bea952 100644 --- a/src/Headers/declaratorInvNodeList.h +++ b/src/Headers/declaratorInvNodeList.h @@ -32,16 +32,9 @@ extern declaratorInvNodeList declaratorInvNodeList_add (/*@returned@*/ declaratorInvNodeList p_s, /*@only@*/ declaratorInvNode p_el); -extern /*@only@*/ cstring declaratorInvNodeList_unparse (declaratorInvNodeList p_s) ; extern void declaratorInvNodeList_free (/*@only@*/ declaratorInvNodeList p_s) ; -/*@constant int declaratorInvNodeListBASESIZE;@*/ -# define declaratorInvNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/enumNameList.h b/src/Headers/enumNameList.h index b9d5883..598d8d7 100644 --- a/src/Headers/enumNameList.h +++ b/src/Headers/enumNameList.h @@ -11,13 +11,11 @@ typedef cstring enumName ; extern /*@only@*/ enumName enumName_create (/*@only@*/ cstring p_s) /*@*/ ; # define enumName_create(s) (s) -typedef /*@only@*/ enumName o_enumName; - abst_typedef struct { int nelements; int nspace; - /*@reldef@*/ /*@relnull@*/ o_enumName *elements; + /*@reldef@*/ /*@relnull@*/ /*@only@*/ enumName *elements; } *enumNameList ; /*@iter enumNameList_elements (sef enumNameList x, yield exposed enumName el); @*/ @@ -29,7 +27,6 @@ abst_typedef struct # define end_enumNameList_elements }} extern int enumNameList_size (enumNameList); - # define enumNameList_size(s) ((s)->nelements) extern /*@only@*/ enumNameList enumNameList_new(void); @@ -45,18 +42,14 @@ extern bool enumNameList_match (enumNameList p_e1, enumNameList p_e2) /*@*/ ; extern /*@only@*/ enumNameList enumNameList_single (/*@keep@*/ enumName p_t) /*@*/ ; extern /*@only@*/ enumNameList enumNameList_subtract (enumNameList p_source, enumNameList p_del) /*@*/ ; +# ifdef DEADCODE extern /*@only@*/ enumNameList enumNameList_copy (enumNameList p_s) /*@*/ ; +# endif extern /*@only@*/ enumNameList enumNameList_undump(char **p_s); extern /*@only@*/ cstring enumNameList_dump (enumNameList p_s); extern /*@only@*/ cstring enumNameList_unparseBrief (enumNameList p_s); -/*@constant int enumNameListBASESIZE;@*/ -# define enumNameListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/enumSpecNode.h b/src/Headers/enumSpecNode.h index 4027e09..183a35f 100644 --- a/src/Headers/enumSpecNode.h +++ b/src/Headers/enumSpecNode.h @@ -11,6 +11,3 @@ typedef struct { sort sort; } *enumSpecNode; -extern /*@unused@*/ /*@only@*/ - cstring enumSpecNode_unparse(/*@null@*/ enumSpecNode p_n) /*@*/ ; - diff --git a/src/Headers/exportNode.h b/src/Headers/exportNode.h index d8580a6..ec7e077 100644 --- a/src/Headers/exportNode.h +++ b/src/Headers/exportNode.h @@ -22,5 +22,3 @@ typedef struct { } content; } *exportNode; -extern /*@unused@*/ /*@only@*/ cstring exportNode_unparse (exportNode p_n); - diff --git a/src/Headers/exposedNode.h b/src/Headers/exposedNode.h index 699462e..ab3459e 100644 --- a/src/Headers/exposedNode.h +++ b/src/Headers/exposedNode.h @@ -10,5 +10,3 @@ typedef struct { declaratorInvNodeList decls; } *exposedNode; -extern /*@unused@*/ /*@only@*/ cstring exposedNode_unparse (exposedNode p_n); - diff --git a/src/Headers/exprData.h b/src/Headers/exprData.h index a57b751..13e9008 100644 --- a/src/Headers/exprData.h +++ b/src/Headers/exprData.h @@ -1,10 +1,11 @@ -/* ;-*-C-*-; */ - /* ** freeShallow: free exprData created from exprNode_effect calls. ** All but the innermost storage is free'd. */ +# ifndef EXPRDATA_H +# define EXPRDATA_H + /*@only@*/ exprData exprData_makeLiteral (/*@only@*/ cstring p_s); /*@only@*/ exprData exprData_makeId (/*@temp@*/ uentry p_id); @@ -101,10 +102,6 @@ exprData_makeOp (/*@keep@*/ exprNode p_a, /*@keep@*/ exprNode p_b, /*@keep@*/ ll exprData_makeIter (/*@exposed@*/ uentry p_sname, /*@keep@*/ exprNodeList p_args, /*@keep@*/ exprNode p_body, /*@exposed@*/ uentry p_ename); -/*static*/ /*@only@*/ exprData exprData_makeTriple (/*@keep@*/ exprNode p_pred, - /*@keep@*/ exprNode p_tbranch, - /*@keep@*/ exprNode p_fbranch); - /*static*/ /*@only@*/ exprData exprData_makeCall (/*@keep@*/ exprNode p_fcn, /*@keep@*/ exprNodeList p_args); @@ -136,13 +133,9 @@ exprData_makeIter (/*@exposed@*/ uentry p_sname, /*@keep@*/ exprNodeList p_args, /*@keep@*/ exprNode p_pred, /*@keep@*/ exprNode p_inc); - /*@=declundef*/ - - - - - - +# else +# error "Multiple include" +# endif diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h index 40975bf..68a63b9 100644 --- a/src/Headers/exprNode.h +++ b/src/Headers/exprNode.h @@ -297,9 +297,6 @@ extern /*@only@*/ /*@notnull@*/ exprNode ** No surrounding quotes. */ -extern /*@notnull@*/ exprNode - exprNode_rawStringLiteral (/*@only@*/ cstring p_t, /*@only@*/ fileloc p_loc) /*@*/ ; - extern exprNode exprNode_comma (/*@only@*/ exprNode p_e1, /*@only@*/ exprNode p_e2) /*@*/ ; extern exprNode exprNode_labelMarker (/*@only@*/ cstring p_label); extern exprNode @@ -331,7 +328,6 @@ extern exprNode exprNode_return (/*@only@*/ exprNode p_e); extern /*@dependent@*/ /*@observer@*/ cstring exprNode_unparse (/*@temp@*/ exprNode p_e) /*@*/ ; -extern /*@falsewhennull@*/ bool exprNode_isBlock (exprNode p_e) /*@*/ ; extern /*@falsewhennull@*/ bool exprNode_isCharLiteral (exprNode p_e) /*@*/ ; extern /*@falsewhennull@*/ bool exprNode_isNumLiteral (exprNode p_e) /*@*/ ; @@ -383,9 +379,7 @@ extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ; extern /*@falsewhennull@*/ bool exprNode_isAssign (exprNode p_e) /*@*/ ; /*@-exportlocal@*/ -extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ; extern bool exprNode_isCaseMarker (exprNode p_e) /*@*/ ; -extern bool exprNode_isLabelMarker (exprNode p_e) /*@*/ ; /*@=exportlocal@*/ extern /*@only@*/ exprNode exprNode_combineLiterals (/*@only@*/ exprNode p_e, /*@only@*/ exprNode p_rest) ; diff --git a/src/Headers/exprNodeList.h b/src/Headers/exprNodeList.h index b22acf3..e2a6bbe 100644 --- a/src/Headers/exprNodeList.h +++ b/src/Headers/exprNodeList.h @@ -51,11 +51,7 @@ extern /*@observer@*/ exprNode exprNodeList_current (exprNodeList p_s) /*@*/ ; extern /*@exposed@*/ exprNode exprNodeList_getN (exprNodeList p_s, int p_n) /*@*/ ; -/*@constant int exprNodeListBASESIZE;@*/ -# define exprNodeListBASESIZE SMALLBASESIZE - +# else +# error "Multiple include" # endif - - - diff --git a/src/Headers/exprNodeSList.h b/src/Headers/exprNodeSList.h index c2fd5de..8c234ac 100644 --- a/src/Headers/exprNodeSList.h +++ b/src/Headers/exprNodeSList.h @@ -31,20 +31,12 @@ extern /*@only@*/ exprNodeSList exprNodeSList_new(void); extern /*@only@*/ exprNodeSList exprNodeSList_singleton (/*@exposed@*/ /*@dependent@*/ exprNode p_e) ; -extern /*@unused@*/ void - exprNodeSList_addh (exprNodeSList p_s, /*@exposed@*/ /*@dependent@*/ exprNode p_el); - -extern /*@only@*/ /*@unused@*/ cstring exprNodeSList_unparse (exprNodeSList p_s); extern void exprNodeSList_free (/*@only@*/ exprNodeSList p_s) ; extern exprNodeSList exprNodeSList_append (/*@returned@*/ exprNodeSList p_s1, /*@only@*/ exprNodeSList p_s2) ; -/*@constant int exprNodeSListBASESIZE;@*/ -# define exprNodeSListBASESIZE SMALLBASESIZE - +# else +# error "Multiple include" # endif - - - diff --git a/src/Headers/fcnNode.h b/src/Headers/fcnNode.h index 0e884af..08d702c 100644 --- a/src/Headers/fcnNode.h +++ b/src/Headers/fcnNode.h @@ -4,6 +4,9 @@ ** */ +# ifndef FCNNODE_H +# define FCNNODE_H + typedef struct { ltoken name; /*@null@*/ lclTypeSpecNode typespec; @@ -20,4 +23,8 @@ typedef struct { } *fcnNode; extern void fcnNode_free (/*@null@*/ /*@only@*/ fcnNode p_f); -extern /*@only@*/ cstring fcnNode_unparse (/*@null@*/ fcnNode p_f); + +# else +# error "Multiple include" +# endif + diff --git a/src/Headers/fcnNodeList.h b/src/Headers/fcnNodeList.h index 2dd178a..089bc70 100644 --- a/src/Headers/fcnNodeList.h +++ b/src/Headers/fcnNodeList.h @@ -36,25 +36,18 @@ extern /*@unused@*/ /*@nullwhentrue@*/ bool # define fcnNodeList_isUndefined(f) ((f) == fcnNodeList_undefined) extern int fcnNodeList_size (/*@sef@*/ fcnNodeList p_f); -extern bool fcnNodeList_isEmpty (/*@sef@*/ fcnNodeList p_f); - # define fcnNodeList_size(s) (fcnNodeList_isDefined(s) ? (s)->nelements : 0) + +extern bool fcnNodeList_isEmpty (/*@sef@*/ fcnNodeList p_f); # define fcnNodeList_isEmpty(s) (fcnNodeList_size(s) == 0) extern /*@only@*/ fcnNodeList fcnNodeList_new(void); extern fcnNodeList fcnNodeList_add (/*@returned@*/ fcnNodeList p_s, /*@keep@*/ fcnNode p_el) ; -extern /*@unused@*/ /*@only@*/ cstring fcnNodeList_unparse (fcnNodeList p_s) ; extern void fcnNodeList_free (/*@null@*/ /*@only@*/ fcnNodeList p_s) ; -/*@constant int fcnNodeListBASESIZE;@*/ -# define fcnNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/fileIdList.h b/src/Headers/fileIdList.h index 3f29ab1..dc061ae 100644 --- a/src/Headers/fileIdList.h +++ b/src/Headers/fileIdList.h @@ -37,10 +37,6 @@ extern fileIdList fileIdList_create (void); extern bool fileIdList_isEmpty (/*@sef@*/ fileIdList p_f) /*@*/ ; -extern fileIdList fileIdList_append (/*@only@*/ fileIdList p_f1, /*@temp@*/ fileIdList p_f2) - /*@modifies p_f1@*/ ; -# define fileIdList_append(f1,f2) ctypeList_append((ctypeList)(f1), (ctypeList)(f2)) - extern void fileIdList_add (fileIdList p_f, fileId p_fid) /*@modifies p_f@*/; # define fileIdList_add(f, el) ctypeList_addh((ctypeList)(f), (ctype)(el)) @@ -57,4 +53,3 @@ extern void fileIdList_free (/*@only@*/ fileIdList p_f) /*@modifies p_f@*/; # error "Multiple include" # endif - diff --git a/src/Headers/fileLib.h b/src/Headers/fileLib.h index 7e4a169..0fb74a5 100644 --- a/src/Headers/fileLib.h +++ b/src/Headers/fileLib.h @@ -22,7 +22,6 @@ 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 (/*@only@*/ cstring p_s) /*@*/ ; -extern bool fileLib_hasExtension (cstring p_s, cstring p_ext) /*@*/ ; extern /*@observer@*/ cstring fileLib_getExtension (/*@returned@*/ cstring p_s) /*@*/ ; diff --git a/src/Headers/fileTable.h b/src/Headers/fileTable.h index 1b76ac7..73433cf 100644 --- a/src/Headers/fileTable.h +++ b/src/Headers/fileTable.h @@ -89,7 +89,6 @@ extern bool fileTable_sameBase (fileTable p_ft, fileId p_f1, fileId p_f2); extern void fileTable_cleanup (fileTable p_ft) /*@modifies fileSystem@*/; extern fileId fileTable_lookupBase (fileTable p_ft, cstring p_base) /*@modifies p_ft@*/ ; extern void fileTable_printTemps (fileTable p_ft) /*@modifies g_warningstream@*/ ; -extern /*@unused@*/ /*@only@*/ cstring fileTable_unparse (fileTable p_ft) /*@*/ ; extern bool fileTable_exists (fileTable p_ft, cstring p_s) /*@*/ ; extern void fileTable_free (/*@only@*/ fileTable p_f); extern bool fileTable_isSpecialFile (fileTable p_ft, fileId p_fid) /*@*/ ; diff --git a/src/Headers/fileloc.h b/src/Headers/fileloc.h index 9eeb72f..1f4960f 100644 --- a/src/Headers/fileloc.h +++ b/src/Headers/fileloc.h @@ -67,7 +67,6 @@ extern bool fileloc_isHeader (fileloc p_f) /*@*/ ; extern bool fileloc_isSpec (fileloc p_f) /*@*/ ; extern bool fileloc_isRealSpec (fileloc p_f) /*@*/ ; extern fileloc fileloc_copy (fileloc p_f) /*@*/ ; -extern cstring fileloc_unparseDirect (fileloc p_fl) /*@*/ ; extern bool fileloc_notAfter (fileloc p_f1, fileloc p_f2) /*@*/ ; extern bool fileloc_almostSameFile (fileloc p_f1, fileloc p_f2) /*@*/ ; extern fileloc fileloc_noColumn (fileloc p_f) /*@*/ ; @@ -175,8 +174,3 @@ extern bool fileloc_storable (/*@sef@*/ fileloc p_f) /*@*/; # error "Multiple include" # endif - - - - - diff --git a/src/Headers/filelocList.h b/src/Headers/filelocList.h index c14eb65..a93fe68 100644 --- a/src/Headers/filelocList.h +++ b/src/Headers/filelocList.h @@ -12,13 +12,13 @@ abst_typedef /*@null@*/ struct /*@reldef@*/ /*@relnull@*/ o_fileloc *elements; } *filelocList ; -extern /*@unused@*/ /*@nullwhentrue@*/ bool - filelocList_isUndefined (filelocList p_f) /*@*/ ; -extern /*@falsewhennull@*/ bool filelocList_isDefined (filelocList p_f); - /*@constant null filelocList filelocList_undefined; @*/ # define filelocList_undefined (NULL) + +extern /*@falsewhennull@*/ bool filelocList_isDefined (filelocList p_f); # define filelocList_isDefined(f) ((f) != filelocList_undefined) + +extern /*@unused@*/ /*@nullwhentrue@*/ bool filelocList_isUndefined (filelocList p_f) /*@*/ ; # define filelocList_isUndefined(f) ((f) == filelocList_undefined) /*@iter filelocList_elements (sef filelocList x, yield exposed fileloc el); @*/ @@ -55,14 +55,7 @@ extern filelocList filelocList_addUndefined (/*@returned@*/ filelocList p_s) /*@modifies p_s@*/ ; extern /*@only@*/ cstring filelocList_unparseUses (filelocList p_s); -extern /*@unused@*/ /*@only@*/ cstring filelocList_unparse (filelocList p_s) ; extern void filelocList_free (/*@only@*/ filelocList p_s) ; -/*@constant int filelocListBASESIZE;@*/ -# define filelocListBASESIZE MIDBASESIZE - # endif - - - diff --git a/src/Headers/filelocStack.h b/src/Headers/filelocStack.h index 6014053..30a79a6 100644 --- a/src/Headers/filelocStack.h +++ b/src/Headers/filelocStack.h @@ -33,14 +33,7 @@ extern bool filelocStack_popPushFile (filelocStack p_s, /*@only@*/ fileloc p_el) /*@modifies p_s@*/ ; -extern /*@unused@*/ /*@only@*/ cstring filelocStack_unparse (filelocStack p_s) /*@*/ ; extern void filelocStack_free (/*@only@*/ filelocStack p_s) ; -/*@constant int filelocStackBASESIZE;@*/ -# define filelocStackBASESIZE MIDBASESIZE - # endif - - - diff --git a/src/Headers/flagMarkerList.h b/src/Headers/flagMarkerList.h index 4388f8d..c040829 100644 --- a/src/Headers/flagMarkerList.h +++ b/src/Headers/flagMarkerList.h @@ -21,8 +21,6 @@ abst_typedef struct extern /*@only@*/ flagMarkerList flagMarkerList_new (void) /*@*/ ; -extern /*@unused@*/ /*@only@*/ cstring - flagMarkerList_unparse (flagMarkerList p_s) /*@*/ ; extern void flagMarkerList_free (/*@only@*/ flagMarkerList p_s) ; extern bool flagMarkerList_add (flagMarkerList p_s, /*@only@*/ flagMarker p_fm) @@ -37,13 +35,7 @@ extern void flagMarkerList_checkSuppressCounts (flagMarkerList p_s) extern bool flagMarkerList_inIgnore (flagMarkerList p_s, fileloc p_loc) /*@*/ ; -/*@constant int flagMarkerListBASESIZE;@*/ -# define flagMarkerListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/forwardTypes.h b/src/Headers/forwardTypes.h index 5729157..b6ba731 100644 --- a/src/Headers/forwardTypes.h +++ b/src/Headers/forwardTypes.h @@ -12,7 +12,6 @@ abst_typedef /*@null@*/ struct s_usymtab *usymtab; abst_typedef /*@null@*/ struct s_exprNode *exprNode; abst_typedef /*@null@*/ struct s_guardSet *guardSet; abst_typedef /*@null@*/ struct s_sRefSet *sRefSet; -abst_typedef /*@null@*/ struct s_sRefList *sRefList ; abst_typedef /*@null@*/ struct s_aliasTable *aliasTable; abst_typedef /*@null@*/ struct s_fileloc *fileloc; abst_typedef /*@null@*/ struct s_cstringTable *cstringTable; diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h index 3b24bc7..39db8ed 100644 --- a/src/Headers/functionClause.h +++ b/src/Headers/functionClause.h @@ -71,9 +71,6 @@ extern functionClause functionClause_createRequires (/*@only@*/ functionConstrai extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ; extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ; -extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ; -extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ; -extern /*@exposed@*/ functionConstraint functionClause_getEnsures (functionClause) /*@*/ ; extern /*@exposed@*/ functionConstraint functionClause_getRequires (functionClause) /*@*/ ; extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ; diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h index 8860385..15e9ab0 100644 --- a/src/Headers/functionClauseList.h +++ b/src/Headers/functionClauseList.h @@ -31,16 +31,8 @@ extern int functionClauseList_size (/*@sef@*/ functionClauseList) /*@*/ ; extern /*@unused@*/ /*@falsewhennull@*/ bool functionClauseList_empty (/*@sef@*/ functionClauseList) /*@*/ ; # define functionClauseList_empty(s) (functionClauseList_size(s) == 0) -extern cstring functionClauseList_unparseSep (functionClauseList p_s, cstring p_sep) /*@*/ ; - extern /*@unused@*/ /*@only@*/ functionClauseList functionClauseList_new (void) /*@*/ ; -extern /*@only@*/ functionClauseList functionClauseList_single (/*@keep@*/ functionClause p_el) /*@*/ ; - -extern /*@unused@*/ functionClauseList - functionClauseList_add (/*@returned@*/ functionClauseList p_s, /*@keep@*/ functionClause p_el) - /*@modifies p_s@*/ ; - extern /*@only@*/ functionClauseList functionClauseList_prepend (/*@only@*/ functionClauseList p_s, /*@keep@*/ functionClause p_el) /*@modifies p_s@*/ ; @@ -50,9 +42,6 @@ extern void functionClauseList_free (/*@only@*/ functionClauseList p_s) ; functionClauseList functionClauseList_setImplicitConstraints (/*@returned@*/ functionClauseList p_s); - -/*@constant int functionClauseListBASESIZE;@*/ -# define functionClauseListBASESIZE MIDBASESIZE /*@iter functionClauseList_elements (sef functionClauseList x, yield exposed functionClause el); @*/ # define functionClauseList_elements(x, m_el) \ @@ -67,6 +56,3 @@ functionClauseList_setImplicitConstraints (/*@returned@*/ functionClauseList p_s # error "Multiple include" # endif - - - diff --git a/src/Headers/genericTable.h b/src/Headers/genericTable.h index 52b0722..c9bb9ef 100644 --- a/src/Headers/genericTable.h +++ b/src/Headers/genericTable.h @@ -10,9 +10,6 @@ # ifndef GHTABLE_H # define GHTABLE_H -/*@constant int GHBUCKET_BASESIZE; @*/ -# define GHBUCKET_BASESIZE 2 - /* in forwardTypes: abst_typedef null struct _genericTable *genericTable; */ @@ -60,9 +57,7 @@ extern /*@null@*/ /*@exposed@*/ void *genericTable_lookup (genericTable p_h, cst extern bool genericTable_contains (genericTable p_h, cstring p_key) /*@*/ ; -extern /*@unused@*/ /*@only@*/ cstring genericTable_stats (genericTable p_h); extern void genericTable_free (/*@only@*/ genericTable p_h); -extern void genericTable_remove (genericTable p_h, cstring p_key) /*@modifies p_h@*/ ; extern /*@unused@*/ void genericTable_update (genericTable p_h, cstring p_key, /*@only@*/ void *p_newval) /*@modifies p_h@*/ ; @@ -85,15 +80,3 @@ extern /*@unused@*/ void genericTable_update (genericTable p_h, cstring p_key, # error "Multiple include" # endif - - - - - - - - - - - - diff --git a/src/Headers/globSet.h b/src/Headers/globSet.h index df29829..5493c2d 100644 --- a/src/Headers/globSet.h +++ b/src/Headers/globSet.h @@ -46,9 +46,7 @@ extern globSet /*@modifies p_s1@*/ ; extern /*@only@*/ globSet globSet_newCopy (globSet p_s) /*@*/ ; -extern bool globSet_hasStatic (globSet p_s) /*@*/ ; -extern int globSet_compare (globSet p_l1, globSet p_l2); extern void globSet_clear (globSet p_g); /*@constant null globSet globSet_undefined;@*/ diff --git a/src/Headers/globalList.h b/src/Headers/globalList.h index eae7a70..64c77f8 100644 --- a/src/Headers/globalList.h +++ b/src/Headers/globalList.h @@ -5,8 +5,6 @@ */ typedef varDeclarationNodeList globalList ; -extern /*@unused@*/ cstring globalList_unparse (globalList p_s); extern void globalList_free (/*@only@*/ globalList p_s); # define globalList_free(s) (varDeclarationNodeList_free (s)) -# define globalList_unparse(s) (varDeclarationNodeList_unparse(s)) diff --git a/src/Headers/globalsClause.h b/src/Headers/globalsClause.h index 3d44feb..dbc54a8 100644 --- a/src/Headers/globalsClause.h +++ b/src/Headers/globalsClause.h @@ -16,7 +16,6 @@ struct s_globalsClause { } ; extern globalsClause globalsClause_create (/*@only@*/ lltok, /*@only@*/ globSet) /*@*/ ; -extern /*@observer@*/ globSet globalsClause_getGlobs (globalsClause) /*@*/ ; extern /*@only@*/ globSet globalsClause_takeGlobs (globalsClause p_gclause) /*@modifies p_gclause@*/ ; extern /*@observer@*/ fileloc globalsClause_getLoc (globalsClause) /*@*/ ; diff --git a/src/Headers/idDecl.h b/src/Headers/idDecl.h index 470a6ea..befe4eb 100644 --- a/src/Headers/idDecl.h +++ b/src/Headers/idDecl.h @@ -27,10 +27,6 @@ extern void idDecl_free (/*@only@*/ idDecl p_t); extern /*@only@*/ idDecl idDecl_create (/*@only@*/ cstring p_s, /*@only@*/ qtype p_t); -extern /*@only@*/ idDecl - idDecl_createClauses (/*@only@*/ cstring p_s, /*@only@*/ qtype p_t, - /*@only@*/ functionClauseList p_clauses); - extern /*@only@*/ cstring idDecl_unparse (idDecl p_d) /*@*/ ; extern /*@only@*/ cstring idDecl_unparseC (idDecl p_d) /*@*/ ; extern /*@exposed@*/ qtype idDecl_getTyp (idDecl p_d) /*@*/ ; @@ -57,4 +53,3 @@ extern void idDecl_addQual (idDecl p_d, qual p_q); # error "Multiple include" # endif - diff --git a/src/Headers/idDeclList.h b/src/Headers/idDeclList.h index 26aaf53..4d52c96 100644 --- a/src/Headers/idDeclList.h +++ b/src/Headers/idDeclList.h @@ -26,16 +26,9 @@ abst_typedef struct extern /*@only@*/ idDeclList idDeclList_singleton (/*@only@*/ idDecl p_e) ; extern idDeclList idDeclList_add (/*@returned@*/ idDeclList p_s, /*@only@*/ idDecl p_el) ; -extern /*@unused@*/ /*@only@*/ cstring idDeclList_unparse (idDeclList p_s) ; extern void idDeclList_free (/*@only@*/ idDeclList p_s) ; -/*@constant int idDeclListBASESIZE;@*/ -# define idDeclListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/importNodeList.h b/src/Headers/importNodeList.h index 119c607..992c787 100644 --- a/src/Headers/importNodeList.h +++ b/src/Headers/importNodeList.h @@ -27,16 +27,9 @@ extern /*@only@*/ importNodeList importNodeList_new (void); extern importNodeList importNodeList_add (/*@returned@*/ importNodeList p_s, /*@only@*/ importNode p_el) ; -extern /*@only@*/ cstring importNodeList_unparse (importNodeList p_s) ; extern void importNodeList_free (/*@only@*/ importNodeList p_s) ; -/*@constant int importNodeListBASESIZE;@*/ -# define importNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/initDeclNodeList.h b/src/Headers/initDeclNodeList.h index 5c6529f..4a6c85c 100644 --- a/src/Headers/initDeclNodeList.h +++ b/src/Headers/initDeclNodeList.h @@ -29,16 +29,9 @@ extern initDeclNodeList initDeclNodeList_add (/*@returned@*/ initDeclNodeList p_s, /*@only@*/ initDeclNode p_el) ; -extern /*@only@*/ cstring initDeclNodeList_unparse (initDeclNodeList p_s) ; extern void initDeclNodeList_free (/*@only@*/ initDeclNodeList p_s) ; -/*@constant int initDeclNodeListBASESIZE;@*/ -# define initDeclNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/intSet.h b/src/Headers/intSet.h index 2d1ce70..f5e4075 100644 --- a/src/Headers/intSet.h +++ b/src/Headers/intSet.h @@ -35,18 +35,11 @@ extern int intSet_size (intSet p_s); # define intSet_size(s) ((s)->entries) extern bool intSet_insert (intSet p_s, int p_el); -extern /*@unused@*/ bool intSet_member (intSet p_s, int p_el); -extern /*@only@*/ /*@unused@*/ cstring intSet_unparse (intSet p_s); extern void intSet_free (/*@only@*/ intSet p_s); extern /*@only@*/ cstring intSet_unparseText (intSet p_s); -/*@constant int intSetBASESIZE;@*/ -# define intSetBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - diff --git a/src/Headers/interfaceNode.h b/src/Headers/interfaceNode.h index d737a72..a1d19f7 100644 --- a/src/Headers/interfaceNode.h +++ b/src/Headers/interfaceNode.h @@ -21,7 +21,5 @@ typedef struct { /* the list that made up is chained thru next */ } *interfaceNode; -extern /*@unused@*/ cstring interfaceNode_unparse (interfaceNode p_x); extern void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode p_x); - diff --git a/src/Headers/iterNode.h b/src/Headers/iterNode.h index f766625..a9d9b6a 100644 --- a/src/Headers/iterNode.h +++ b/src/Headers/iterNode.h @@ -9,5 +9,3 @@ typedef struct { paramNodeList params; } *iterNode; -extern /*@unused@*/ /*@only@*/ cstring - iterNode_unparse (/*@null@*/ iterNode p_i) /*@*/ ; diff --git a/src/Headers/lctype.h b/src/Headers/lctype.h index 41de16e..b44925f 100644 --- a/src/Headers/lctype.h +++ b/src/Headers/lctype.h @@ -229,9 +229,6 @@ extern /*@only@*/ cstring ctype_dump (ctype p_c) /*@*/ ; extern /*@observer@*/ cstring ctype_enumTag (ctype p_c) /*@*/ ; extern /*@observer@*/ cstring ctype_unparse (ctype p_c) /*@*/ ; extern /*@observer@*/ cstring ctype_unparseDeep (ctype p_c) /*@*/ ; -extern /*@unused@*/ /*@observer@*/ cstring ctype_unparseSafe (ctype p_c) /*@*/ ; - -extern ctkind ctkind_fromInt (int p_i) /*@*/ ; extern bool ctype_matchDef (ctype p_c1, ctype p_c2) /*@*/ ; extern ctype ctype_undump (char **p_c); @@ -254,7 +251,6 @@ extern ctype ctype_createUnnamedStruct (/*@only@*/ uentryList p_f) ; extern ctype ctype_createUnnamedUnion (/*@only@*/ uentryList p_f) ; extern ctype ctype_createUser (typeId p_u) ; -extern bool ctype_isUnnamedSU (ctype p_c) /*@*/ ; extern bool ctype_isUser (ctype p_c) /*@*/ ; extern int ctype_getSize (ctype p_c) @@ -317,7 +313,6 @@ extern cprim ctype_toCprim (ctype p_c) /*@*/ ; /*@noaccess cprim@*/ extern int ctype_compare (ctype p_c1, ctype p_c2) /*@*/ ; -extern /*@unused@*/ int ctype_count (void); extern ctype ctype_makeExplicitConj (ctype p_c1, ctype p_c2); @@ -375,7 +370,9 @@ extern void ctype_loadTable (FILE *p_f); extern void ctype_destroyMod (void); extern void ctype_initTable (void); extern /*@only@*/ cstring ctype_unparseTable (void); +# if 0 extern /*@unused@*/ void ctype_printTable (void); +# endif extern ctype ctype_widest (ctype, ctype) /*@*/ ; diff --git a/src/Headers/letDeclNodeList.h b/src/Headers/letDeclNodeList.h index bdd2b24..2bb38ce 100644 --- a/src/Headers/letDeclNodeList.h +++ b/src/Headers/letDeclNodeList.h @@ -27,16 +27,9 @@ extern /*@only@*/ letDeclNodeList letDeclNodeList_new(void); extern letDeclNodeList letDeclNodeList_add (/*@returned@*/ letDeclNodeList p_s, /*@only@*/ letDeclNode p_el); -extern /*@only@*/ cstring letDeclNodeList_unparse (letDeclNodeList p_s) ; extern void letDeclNodeList_free (/*@only@*/ letDeclNodeList p_s) ; -/*@constant int letDeclNodeListBASESIZE;@*/ -# define letDeclNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/lh.h b/src/Headers/lh.h index f896920..9f31c9b 100644 --- a/src/Headers/lh.h +++ b/src/Headers/lh.h @@ -8,7 +8,6 @@ */ extern void lhCleanup (void) /*@modifies internalState, fileSystem@*/ ; -extern void lhIncludeBool (void) /*@modifies internalState@*/ ; extern void lhInit (inputStream p_f) /*@modifies internalState@*/ ; extern void lhOutLine (/*@only@*/ cstring p_s) /*@modifies internalState@*/ ; extern void lhExternals (interfaceNodeList p_x) /*@modifies internalState@*/ ; diff --git a/src/Headers/llerror.h b/src/Headers/llerror.h index eb5d7fb..859639d 100644 --- a/src/Headers/llerror.h +++ b/src/Headers/llerror.h @@ -406,23 +406,12 @@ extern void ppllerror (/*@only@*/ cstring p_s); extern void genppllerrorhint (flagcode p_code, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint); extern void genppllerror (flagcode p_code, /*@only@*/ cstring p_s); -extern /*@unused@*/ void pplldiagmsg (/*@only@*/ cstring p_s); extern void loadllmsg (/*@only@*/ cstring p_s); extern void llgenindentmsgnoloc (/*@only@*/ cstring p_s); extern /*@observer@*/ cstring lldecodeerror (int) /*@*/ ; -/* -** should be static, but used in cpperror (which shouldn't exist) -*/ - -extern void prepareMessage (void) - /*@modifies internalState, g_messagestream@*/ ; - -extern void closeMessage (void) - /*@modifies internalState, g_messagestream@*/ ; - extern void llflush (void) /*@modifies systemState@*/ ; # else diff --git a/src/Headers/lslOpList.h b/src/Headers/lslOpList.h index c57be56..e1b0916 100644 --- a/src/Headers/lslOpList.h +++ b/src/Headers/lslOpList.h @@ -18,15 +18,9 @@ abst_typedef struct extern /*@only@*/ lslOpList lslOpList_new(void); extern void lslOpList_add (lslOpList p_s, /*@exposed@*/ lslOp p_el) ; -extern /*@unused@*/ /*@only@*/ cstring lslOpList_unparse (lslOpList p_s) ; extern void lslOpList_free (/*@only@*/ lslOpList p_s) ; -/*@constant int lslOpListBASESIZE;@*/ -# define lslOpListBASESIZE SMALLBASESIZE # else # error "Multiple include" # endif - - - diff --git a/src/Headers/lslOpSet.h b/src/Headers/lslOpSet.h index 4a3e7f4..c1ff4de 100644 --- a/src/Headers/lslOpSet.h +++ b/src/Headers/lslOpSet.h @@ -43,13 +43,9 @@ extern /*@only@*/ lslOpSet lslOpSet_new (void) /*@*/ ; extern bool lslOpSet_insert (lslOpSet p_s, /*@only@*/ lslOp p_el) /*@modifies p_s@*/ ; -extern /*@unused@*/ /*@only@*/ cstring lslOpSet_unparse (lslOpSet p_s) /*@*/ ; extern void lslOpSet_free (/*@only@*/ lslOpSet p_s); extern /*@only@*/ lslOpSet lslOpSet_copy (lslOpSet p_s) /*@*/ ; -/*@constant int lslOpSetBASESIZE;@*/ -# define lslOpSetBASESIZE MIDBASESIZE - # else # error "Multiple include" # endif diff --git a/src/Headers/lsymbol.h b/src/Headers/lsymbol.h index 95baebe..707d247 100644 --- a/src/Headers/lsymbol.h +++ b/src/Headers/lsymbol.h @@ -29,8 +29,6 @@ extern /*@observer@*/ cstring lsymbol_toString(lsymbol) /*@*/ ; extern bool lsymbol_equal (lsymbol p_s1, lsymbol p_s2) /*@*/ ; # define lsymbol_equal(s1, s2) ((s1) == (s2)) -extern /*@unused@*/ void lsymbol_printStats (void); - extern void lsymbol_initMod (void) /*@modifies internalState@*/ ; extern void lsymbol_destroyMod (void) /*@modifies internalState@*/ ; diff --git a/src/Headers/lsymbolSet.h b/src/Headers/lsymbolSet.h index c5f64fd..efe94ad 100644 --- a/src/Headers/lsymbolSet.h +++ b/src/Headers/lsymbolSet.h @@ -37,12 +37,8 @@ extern /*@falsewhennull@*/ bool lsymbolSet_isDefined (lsymbolSet p_l) /*@*/ ; extern /*@only@*/ lsymbolSet lsymbolSet_new(void) /*@*/ ; extern bool lsymbolSet_insert (lsymbolSet p_s, lsymbol p_el) /*@modifies p_s@*/ ; extern bool lsymbolSet_member (lsymbolSet p_s, lsymbol p_el) /*@*/ ; -extern /*@unused@*/ /*@only@*/ cstring lsymbolSet_unparse (lsymbolSet p_s) /*@*/ ; extern void lsymbolSet_free (/*@only@*/ lsymbolSet p_s); -/*@constant int lsymbolSetBASESIZE;@*/ -# define lsymbolSetBASESIZE MIDBASESIZE - # else # error "Multiple include" # endif diff --git a/src/Headers/macrocache.h b/src/Headers/macrocache.h index 14bde21..84d7511 100644 --- a/src/Headers/macrocache.h +++ b/src/Headers/macrocache.h @@ -33,7 +33,6 @@ extern void extern /*@observer@*/ fileloc macrocache_processFileElements (macrocache p_m, cstring p_base) ; -extern /*@only@*/ /*@unused@*/ cstring macrocache_unparse (macrocache p_m) /*@*/ ; extern /*@only@*/ macrocache macrocache_create (void) /*@*/ ; extern void diff --git a/src/Headers/messageLog.h b/src/Headers/messageLog.h index d3b307b..1851021 100644 --- a/src/Headers/messageLog.h +++ b/src/Headers/messageLog.h @@ -36,16 +36,9 @@ extern /*@only@*/ messageLog messageLog_new (void) /*@*/ ; extern bool messageLog_add (messageLog p_s, fileloc p_fl, cstring p_mess) /*@modifies p_s@*/ ; -extern /*@only@*/ /*@unused@*/ cstring messageLog_unparse (messageLog p_s) /*@*/ ; extern void messageLog_free (/*@only@*/ messageLog p_s) ; -/*@constant int messageLogBASESIZE; @*/ -# define messageLogBASESIZE MIDBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/metaStateConstraintList.h b/src/Headers/metaStateConstraintList.h index c50201e..bab36bf 100644 --- a/src/Headers/metaStateConstraintList.h +++ b/src/Headers/metaStateConstraintList.h @@ -41,10 +41,6 @@ extern bool metaStateConstraintList_isEmpty (/*@sef@*/ metaStateConstraintList p extern metaStateConstraintList metaStateConstraintList_append (/*@returned@*/ metaStateConstraintList p_s, /*@only@*/ metaStateConstraintList p_t); -extern /*@observer@*/ metaStateConstraint metaStateConstraintList_getFirst (metaStateConstraintList p_s) /*@*/ ; - -extern /*@only@*/ metaStateConstraintList metaStateConstraintList_new (void) /*@*/ ; - extern metaStateConstraintList metaStateConstraintList_add (/*@returned@*/ metaStateConstraintList p_s, /*@observer@*/ metaStateConstraint p_el) /*@modifies p_s@*/ ; @@ -52,14 +48,7 @@ metaStateConstraintList_add (/*@returned@*/ metaStateConstraintList p_s, /*@obse extern metaStateConstraintList metaStateConstraintList_single (/*@observer@*/ metaStateConstraint p_el) /*@*/ ; -extern /*@unused@*/ /*@only@*/ cstring metaStateConstraintList_unparse (metaStateConstraintList p_s) ; extern void metaStateConstraintList_free (/*@only@*/ metaStateConstraintList p_s) ; -/*@constant int metaStateConstraintListBASESIZE;@*/ -# define metaStateConstraintListBASESIZE MIDBASESIZE - # endif - - - diff --git a/src/Headers/metaStateInfo.h b/src/Headers/metaStateInfo.h index b4424a7..5950f32 100644 --- a/src/Headers/metaStateInfo.h +++ b/src/Headers/metaStateInfo.h @@ -18,9 +18,6 @@ # ifndef MSINFO_H # define MSINFO_H -/*@constant int metaState_error@*/ -# define metaState_error -1 - struct s_metaStateInfo { /*@only@*/ cstring name; fileloc loc; @@ -64,17 +61,9 @@ extern void metaStateInfo_setDefaultValueContext (metaStateInfo p_info, mtContex extern void metaStateInfo_setDefaultRefValue (metaStateInfo p_info, int p_val) /*@modifies p_info@*/ ; -extern void metaStateInfo_setDefaultParamValue (metaStateInfo p_info, int p_val) - /*@modifies p_info@*/ ; - -extern void metaStateInfo_setDefaultResultValue (metaStateInfo p_info, int p_val) - /*@modifies p_info@*/ ; - extern int metaStateInfo_getDefaultValue (metaStateInfo p_info, sRef p_s) /*@*/ ; extern int metaStateInfo_getDefaultRefValue (metaStateInfo p_info) /*@*/ ; -extern int metaStateInfo_getDefaultParamValue (metaStateInfo p_info) /*@*/ ; -extern int metaStateInfo_getDefaultResultValue (metaStateInfo p_info) /*@*/ ; extern int metaStateInfo_getDefaultGlobalValue (metaStateInfo p_info) /*@*/ ; extern /*@observer@*/ mtContextNode metaStateInfo_getContext (metaStateInfo p_info) /*@*/ ; @@ -95,6 +84,3 @@ extern void metaStateInfo_free (/*@only@*/ metaStateInfo) ; # error "Multiple include" # endif - - - diff --git a/src/Headers/metaStateTable.h b/src/Headers/metaStateTable.h index 59a1e80..069c6ff 100644 --- a/src/Headers/metaStateTable.h +++ b/src/Headers/metaStateTable.h @@ -52,9 +52,6 @@ extern bool metaStateTable_contains (metaStateTable p_h, cstring p_key) /*@*/ ; # define metaStateTable_contains(p_h,p_key) \ (genericTable_contains ((genericTable) (p_h), p_key)) -extern /*@unused@*/ /*@only@*/ cstring metaStateTable_stats(metaStateTable p_h); -# define metaStateTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) - extern void metaStateTable_free (/*@only@*/ metaStateTable p_h); # define metaStateTable_free(p_h) (genericTable_free ((genericTable) (p_h))) @@ -84,6 +81,3 @@ extern int metaStateTable_size (metaStateTable p_h); # error "Multiple include" # endif - - - diff --git a/src/Headers/misc.h b/src/Headers/misc.h index 997b2e4..051ab89 100644 --- a/src/Headers/misc.h +++ b/src/Headers/misc.h @@ -6,7 +6,6 @@ /* ** misc.h ** -** (general.c) */ # ifndef MISC_H @@ -22,11 +21,9 @@ extern unsigned int int_toNonNegative (int p_x) /*@*/ /*@ensures result == p_x@* extern int size_toInt (size_t p_x) /*@*/ /*@ensures result == p_x@*/ ; extern long size_toLong (size_t p_x) /*@*/ /*@ensures result == p_x@*/ ; extern size_t size_fromInt (int p_x) /*@*/ /*@ensures result == p_x@*/ ; -extern size_t size_fromLong (long p_x) /*@*/ /*@ensures result == p_x@*/ ; extern size_t size_fromLongUnsigned (long unsigned p_x) /*@*/ /*@ensures result == p_x@*/ ; extern int longUnsigned_toInt (long unsigned int p_x) /*@*/ /*@ensures result == p_x@*/ ; extern int long_toInt (long p_x) /*@*/ /*@ensures result == p_x@*/ ; -extern long unsigned longUnsigned_fromInt (int p_x) /*@*/ /*@ensures result == p_x@*/ ; extern long unsigned size_toLongUnsigned (size_t p_x) /*@*/ /*@ensures result == p_x@*/ ; extern char char_fromInt (int p_x) /*@*/ ; extern int int_log (int p_x) /*@*/ ; diff --git a/src/Headers/modifiesClause.h b/src/Headers/modifiesClause.h index b190153..b9e03c3 100644 --- a/src/Headers/modifiesClause.h +++ b/src/Headers/modifiesClause.h @@ -21,7 +21,6 @@ extern modifiesClause modifiesClause_createNoMods (/*@only@*/ lltok) /*@*/ ; extern bool modifiesClause_isNoMods (modifiesClause) ; # define modifiesClause_isNoMods(m) ((m)->isnomods) -extern /*@observer@*/ sRefSet modifiesClause_getMods (modifiesClause) ; extern /*@only@*/ sRefSet modifiesClause_takeMods (modifiesClause) ; extern /*@observer@*/ fileloc modifiesClause_getLoc (modifiesClause) /*@*/ ; diff --git a/src/Headers/modifyNode.h b/src/Headers/modifyNode.h index 6d8fd37..9259e26 100644 --- a/src/Headers/modifyNode.h +++ b/src/Headers/modifyNode.h @@ -13,15 +13,3 @@ typedef struct { /*@reldef@*/ storeRefNodeList list; } *modifyNode; -extern /*@unused@*/ /*@only@*/ cstring modifyNode_unparse (/*@null@*/ modifyNode p_m); - - - - - - - - - - - diff --git a/src/Headers/mtContextNode.h b/src/Headers/mtContextNode.h index 20d9ac0..59a0eb9 100644 --- a/src/Headers/mtContextNode.h +++ b/src/Headers/mtContextNode.h @@ -46,7 +46,6 @@ extern void mtContextNode_free (/*@only@*/ mtContextNode) ; extern bool mtContextNode_isReference (mtContextNode) /*@*/; extern bool mtContextNode_isResult (mtContextNode) /*@*/; extern bool mtContextNode_isParameter (mtContextNode) /*@*/; -extern bool mtContextNode_isClause (mtContextNode) /*@*/; extern bool mtContextNode_isLiteral (mtContextNode) /*@*/; extern bool mtContextNode_isNull (mtContextNode) /*@*/; @@ -56,8 +55,6 @@ extern bool mtContextNode_matchesRef (mtContextNode, sRef) /*@*/ ; extern bool mtContextNode_matchesRefStrict (mtContextNode, sRef) /*@*/ ; /* Doesn't allow matches with unknown type. */ -extern void mtContextNode_showRefError (mtContextNode, sRef) ; - # else # error "Multiple include" # endif diff --git a/src/Headers/mtDeclarationPiece.h b/src/Headers/mtDeclarationPiece.h index e974390..409a85a 100644 --- a/src/Headers/mtDeclarationPiece.h +++ b/src/Headers/mtDeclarationPiece.h @@ -45,7 +45,6 @@ extern mtDeclarationPiece mtDeclarationPiece_createPostconditions (/*@only@*/ mt extern mtDeclarationPiece mtDeclarationPiece_createPreconditions (/*@only@*/ mtTransferClauseList) /*@*/ ; extern mtDeclarationPiece mtDeclarationPiece_createLosers (/*@only@*/ mtLoseReferenceList) /*@*/ ; -extern /*@observer@*/ mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece) /*@*/ ; extern /*@only@*/ mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece p_node) /*@modifies p_node@*/ ; extern /*@observer@*/ mtValuesNode mtDeclarationPiece_getValues (mtDeclarationPiece) /*@*/ ; @@ -53,7 +52,6 @@ extern /*@observer@*/ mtDefaultsNode mtDeclarationPiece_getDefaults (mtDeclarati extern /*@observer@*/ mtAnnotationsNode mtDeclarationPiece_getAnnotations (mtDeclarationPiece) /*@*/ ; extern /*@observer@*/ mtMergeNode mtDeclarationPiece_getMerge (mtDeclarationPiece) /*@*/ ; extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getTransfers (mtDeclarationPiece) /*@*/ ; -extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece) /*@*/ ; extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPiece) /*@*/ ; extern /*@observer@*/ cstring mtDeclarationPiece_getDefaultValue (mtDeclarationPiece) /*@*/ ; diff --git a/src/Headers/mttok.h b/src/Headers/mttok.h index 322c75b..dd321e3 100644 --- a/src/Headers/mttok.h +++ b/src/Headers/mttok.h @@ -41,7 +41,6 @@ extern /*@observer@*/ cstring mttok_observeText (mttok p_t) /*@*/ ; # define mttok_observeText(t) ((t)->text) extern bool mttok_isIdentifier (mttok p_t) /*@*/ ; -extern bool mttok_isError (mttok p_t) /*@*/ ; # else # error "Multiple include" diff --git a/src/Headers/multiVal.h b/src/Headers/multiVal.h index 71b88c2..1974812 100644 --- a/src/Headers/multiVal.h +++ b/src/Headers/multiVal.h @@ -35,7 +35,6 @@ extern multiVal multiVal_divide (multiVal p_m1, multiVal p_m2) /*@*/ ; # define multiVal_isUnknown(m) ((m) == multiVal_undefined) extern /*@observer@*/ /*@dependent@*/ cstring multiVal_forceString (multiVal p_m) /*@*/ ; -extern /*@unused@*/ double multiVal_forceDouble (multiVal p_m) /*@*/ ; extern char multiVal_forceChar (multiVal p_m) /*@*/ ; extern long multiVal_forceInt (multiVal p_m) /*@*/ ; diff --git a/src/Headers/opFormNode.h b/src/Headers/opFormNode.h index 81b2c28..bedac39 100644 --- a/src/Headers/opFormNode.h +++ b/src/Headers/opFormNode.h @@ -27,5 +27,3 @@ struct s_opFormNode { ltoken close; /* keeps the closeSym token */ } ; -extern /*@unused@*/ /*@only@*/ cstring - opFormNode_unparse (/*@null@*/ opFormNode p_n) /*@*/ ; diff --git a/src/Headers/osd.h b/src/Headers/osd.h index 6d06759..a7ab1c0 100644 --- a/src/Headers/osd.h +++ b/src/Headers/osd.h @@ -47,8 +47,6 @@ extern /*@only@*/ cstring osd_pathListConcat (const char*, const char*); extern bool osd_pathPrefixInPathList (cstring path, cstring pathList); -extern void osd_setTempError (void) /*@modifies internalState@*/ ; - /*@constant int CALL_SUCCESS@*/ # define CALL_SUCCESS 0 extern int osd_system (cstring p_cmd) /*@modifies fileSystem@*/ ; diff --git a/src/Headers/privateNode.h b/src/Headers/privateNode.h index 437c5a1..6ce2377 100644 --- a/src/Headers/privateNode.h +++ b/src/Headers/privateNode.h @@ -19,4 +19,3 @@ typedef struct { } content; } *privateNode; -extern /*@unused@*/ /*@only@*/ cstring privateNode_unparse(privateNode p_n); diff --git a/src/Headers/programNode.h b/src/Headers/programNode.h index d04f25d..b0845d2 100644 --- a/src/Headers/programNode.h +++ b/src/Headers/programNode.h @@ -19,5 +19,4 @@ typedef struct { } *programNode; extern void programNode_free (/*@only@*/ /*@null@*/ programNode p_x); -extern /*@only@*/ cstring programNode_unparse (programNode p_p); diff --git a/src/Headers/qual.h b/src/Headers/qual.h index 8b67ac5..4e29f5c 100644 --- a/src/Headers/qual.h +++ b/src/Headers/qual.h @@ -66,7 +66,6 @@ extern qual qual_undump (char **p_s) /*@modifies *p_s@*/ ; ** QEXITS QMAYEXIT QNULLTERMINATED */ -extern qual qual_fromInt (int p_q) /*@*/ ; extern /*@observer@*/ cstring qual_unparse (qual p_q) /*@*/ ; extern bool qual_match (qual p_q1, qual p_q2) /*@*/ ; @@ -439,7 +438,3 @@ extern qual qual_abstractFromCodeChar (char) /*@*/ ; # error "Multiple include" # endif - - - - diff --git a/src/Headers/qualList.h b/src/Headers/qualList.h index 68e2b68..2ce76c4 100644 --- a/src/Headers/qualList.h +++ b/src/Headers/qualList.h @@ -52,26 +52,10 @@ extern /*@only@*/ cstring qualList_toCComments (qualList p_s); extern void qualList_clear (qualList p_q); -/*@constant int qualListBASESIZE;@*/ -# define qualListBASESIZE 8 - extern bool qualList_hasAliasQualifier (qualList p_s); extern bool qualList_hasExposureQualifier (qualList p_s); -/* start modifications */ -extern bool qualList_hasNullTerminatedQualifier(qualList p_s); - -extern bool qualList_hasBufQualifiers(qualList p_s); - -# define qualList_hasBufQualifiers(p_s) \ - (qualList_hasNullTerminatedQualifier(p_s)) - -/* end modification/s */ - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/quantifierNode.h b/src/Headers/quantifierNode.h index c003a87..2a85334 100644 --- a/src/Headers/quantifierNode.h +++ b/src/Headers/quantifierNode.h @@ -11,4 +11,3 @@ typedef struct { } *quantifierNode; extern quantifierNode quantifierNode_copy (quantifierNode p_x); -extern void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode p_x); diff --git a/src/Headers/quantifierNodeList.h b/src/Headers/quantifierNodeList.h index b178f81..9b15ca0 100644 --- a/src/Headers/quantifierNodeList.h +++ b/src/Headers/quantifierNodeList.h @@ -29,17 +29,10 @@ extern quantifierNodeList quantifierNodeList_add (/*@returned@*/ quantifierNodeList p_s, /*@only@*/ quantifierNode p_el); extern /*@only@*/ cstring quantifierNodeList_unparse (quantifierNodeList p_s) ; -extern /*@unused@*/ void quantifierNodeList_free (/*@only@*/ quantifierNodeList p_s) ; extern /*@only@*/ quantifierNodeList quantifierNodeList_copy (quantifierNodeList p_s) ; -/*@constant int quantifierNodeListBASESIZE;@*/ -# define quantifierNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/reader.h b/src/Headers/reader.h index d0c585b..343abfe 100644 --- a/src/Headers/reader.h +++ b/src/Headers/reader.h @@ -10,7 +10,7 @@ extern /*@null@*/ char *reader_readLine (FILE *p_f, /*@returned@*/ /*@out@*/ char *p_s, int p_max) /*@modifies *p_f, p_s@*/ ; -extern int reader_getInt (const char **p_s) /*@modifies *p_s@*/ ; +extern int reader_getInt (char **p_s) /*@modifies *p_s@*/ ; extern char reader_loadChar (char **p_s) /*@modifies *p_s@*/ ; extern double reader_getDouble (char **p_s) /*@modifies *p_s@*/ ; diff --git a/src/Headers/renamingNode.h b/src/Headers/renamingNode.h index 7bcfd26..b521fba 100644 --- a/src/Headers/renamingNode.h +++ b/src/Headers/renamingNode.h @@ -17,4 +17,3 @@ typedef struct { } content; } *renamingNode; -extern /*@only@*/ cstring renamingNode_unparse (/*@null@*/ renamingNode p_x); diff --git a/src/Headers/replaceNode.h b/src/Headers/replaceNode.h index 34c0d93..c8ae3ca 100644 --- a/src/Headers/replaceNode.h +++ b/src/Headers/replaceNode.h @@ -18,5 +18,4 @@ typedef struct { } *replaceNode; extern void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode p_x); -extern /*@only@*/ cstring replaceNode_unparse (/*@null@*/ replaceNode p_x); diff --git a/src/Headers/replaceNodeList.h b/src/Headers/replaceNodeList.h index 55eb702..fc37178 100644 --- a/src/Headers/replaceNodeList.h +++ b/src/Headers/replaceNodeList.h @@ -35,16 +35,9 @@ extern /*@only@*/ replaceNodeList replaceNodeList_new(void); extern replaceNodeList replaceNodeList_add (/*@returned@*/ replaceNodeList p_s, /*@only@*/ replaceNode p_el) ; -extern /*@only@*/ cstring replaceNodeList_unparse (replaceNodeList p_s) ; extern void replaceNodeList_free (/*@only@*/ replaceNodeList p_s) ; -/*@constant int replaceNodeListBASESIZE;@*/ -# define replaceNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h index 80c079a..0bb6b1a 100644 --- a/src/Headers/sRef.h +++ b/src/Headers/sRef.h @@ -151,7 +151,6 @@ extern void sRef_setDefNull (sRef p_s, fileloc p_loc); extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; -extern /*@falsewhennull@*/ bool sRef_isReasonable (sRef p_s) /*@*/ ; /*@constant null sRef sRef_undefined; @*/ # define sRef_undefined ((sRef) NULL) @@ -280,7 +279,9 @@ extern bool sRef_isModified (sRef p_s) /*@*/ ; extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ; extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ; +#ifdef DEADCODE extern bool sRef_sameObject (sRef p_s1, sRef p_s2) /*@*/ ; +#endif extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ; extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ; @@ -526,8 +527,6 @@ extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isKept(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT)) -extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ; - extern bool sRef_isStack (sRef p_s) /*@*/ ; extern bool sRef_isLocalState (sRef p_s) /*@*/ ; extern bool sRef_isUnique (sRef p_s) /*@*/ ; @@ -559,10 +558,11 @@ extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ; extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ; extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ; -extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ; extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ; extern bool sRef_isExternal (sRef p_s) /*@*/ ; +#if 0 extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ; +#endif extern cstring sRef_unparseFull (sRef p_s) /*@*/ ; extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ; extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc) @@ -621,8 +621,6 @@ extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; /* start modifications */ /* functions for making modification to null-term info */ -extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct s_bbufinfo p_b, fileloc p_loc); -extern struct s_bbufinfo sRef_getNullTerminatedState(sRef p_s); extern void sRef_setNullTerminatedState (sRef p_s); extern void sRef_setPossiblyNullTerminatedState (sRef p_s); extern void sRef_setNotNullTerminatedState (sRef p_s); @@ -640,7 +638,6 @@ extern int sRef_getLen(sRef p_s); #define sRef_getLen(p_s) \ ((p_s)->bufinfo.len) -extern /*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef) /*@*/ ; extern /*@falsewhennull@*/ bool sRef_hasStateInfoLoc (sRef) /*@*/ ; extern /*@falsewhennull@*/ bool sRef_hasAliasInfoLoc (sRef) /*@*/ ; @@ -670,7 +667,6 @@ extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s); extern bool sRef_isFixedArray (sRef p_s) /*@*/; extern size_t sRef_getArraySize (sRef p_s) /*@*/; -extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s); extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ; /* end modifications */ @@ -690,8 +686,6 @@ extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@ extern bool sRef_hasValue (sRef p_s) /*@*/ ; extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ; -extern /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ; - extern void sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; diff --git a/src/Headers/sRefList.h b/src/Headers/sRefList.h deleted file mode 100644 index ec71f23..0000000 --- a/src/Headers/sRefList.h +++ /dev/null @@ -1,63 +0,0 @@ -/* -** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. -** See ../LICENSE for license information. -*/ -/* -** sRefList.h (from slist_templace.h) -*/ - -# ifndef sRefLIST_H -# define sRefLIST_H - -typedef /*@dependent@*/ sRef d_sRef ; - -struct s_sRefList -{ - int nelements; - int nspace; - /*@reldef@*/ /*@relnull@*/ d_sRef *elements; -} ; - -/*@iter sRefList_elements (sef sRefList x, yield exposed sRef el); @*/ -# define sRefList_elements(x, m_el) \ - { if (!sRefList_isUndefined(x)) \ - { int m_ind; sRef *m_elements = &((x)->elements[0]); \ - for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ - { sRef m_el = *(m_elements++); - -# define end_sRefList_elements }}} - -extern int sRefList_size (sRefList p_s) /*@*/ ; - -extern /*@nullwhentrue@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ; -extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ; -extern /*@unused@*/ /*@falsewhennull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ; - -# define sRefList_isEmpty(s) (sRefList_size(s) == 0) - -/*@constant null sRefList sRefList_undefined; @*/ -# define sRefList_undefined ((sRefList)0) - -# define sRefList_isUndefined(c) ((c) == sRefList_undefined) -# define sRefList_isDefined(c) ((c) != sRefList_undefined) - -extern /*@only@*/ sRefList sRefList_new (void); -extern /*@only@*/ sRefList sRefList_single (/*@dependent@*/ sRef p_el); - -extern /*@notnull@*/ sRefList - sRefList_add (/*@returned@*/ sRefList p_s, /*@exposed@*/ sRef p_el) /*@modifies p_s@*/ ; - -extern cstring sRefList_unparse (sRefList p_s) /*@*/ ; -extern void sRefList_free (/*@only@*/ sRefList p_s) ; -extern /*@only@*/ sRefList sRefList_copy (sRefList p_s) /*@*/ ; - -/*@constant int sRefListBASESIZE;@*/ -# define sRefListBASESIZE MIDBASESIZE - -# else -# error "Multiple include" -# endif - - - - diff --git a/src/Headers/sRefSet.h b/src/Headers/sRefSet.h index e96a0be..5456053 100644 --- a/src/Headers/sRefSet.h +++ b/src/Headers/sRefSet.h @@ -46,9 +46,6 @@ struct s_sRefSet # define end_sRefSet_allElements }}} -/*@constant int sRefSetBASESIZE;@*/ -# define sRefSetBASESIZE SMALLBASESIZE - /*@constant null sRefSet sRefSet_undefined;@*/ # define sRefSet_undefined ((sRefSet) 0) @@ -81,7 +78,9 @@ extern /*@only@*/ sRefSet sRefSet_new (void) /*@*/ ; extern /*@only@*/ sRefSet sRefSet_single (/*@exposed@*/ sRef); extern sRefSet sRefSet_insert (/*@returned@*/ sRefSet p_s, /*@exposed@*/ sRef p_el); extern bool sRefSet_member (sRefSet p_s, sRef p_el) /*@*/ ; +#ifdef DEADCODE extern bool sRefSet_containsSameObject (sRefSet p_s, sRef p_el) /*@*/ ; +#endif extern /*@only@*/ cstring sRefSet_unparse (sRefSet p_s) /*@*/ ; extern void sRefSet_free (/*@only@*/ sRefSet p_s) /*@modifies p_s@*/; extern void sRefSet_clear (sRefSet p_s) /*@modifies p_s@*/; @@ -102,7 +101,6 @@ extern /*@only@*/ sRefSet sRefSet_accessField (sRefSet p_s, /*@observer@*/ cstri extern /*@only@*/ sRefSet sRefSet_realNewUnion (sRefSet p_s1, sRefSet p_s2); extern /*@only@*/ cstring sRefSet_unparseDebug (sRefSet p_s) /*@*/ ; extern /*@unused@*/ cstring sRefSet_unparseFull (sRefSet p_s) /*@*/ ; -extern int sRefSet_compare (sRefSet p_s1, sRefSet p_s2) /*@*/ ; extern bool sRefSet_modifyMember (sRefSet p_s, sRef p_m) /*@modifies p_m@*/ ; extern /*@only@*/ sRefSet sRefSet_undump (char **p_s) /*@modifies *p_s@*/ ; extern /*@only@*/ cstring sRefSet_dump (sRefSet p_sl) /*@*/ ; @@ -126,5 +124,3 @@ extern void sRefSet_markImmutable (sRefSet p_s) /*@modifies p_s@*/ ; # error "Multiple include" # endif - - diff --git a/src/Headers/sRefTable.h b/src/Headers/sRefTable.h index 4b3db5e..ee31c19 100644 --- a/src/Headers/sRefTable.h +++ b/src/Headers/sRefTable.h @@ -21,9 +21,6 @@ abst_typedef /*@null@*/ struct /*@reldef@*/ /*@relnull@*/ ow_sRef *elements; } *sRefTable; -/*@constant int sRefTableBASESIZE; @*/ -# define sRefTableBASESIZE HUGEBASESIZE - /*@constant null sRefTable sRefTable_undefined; @*/ # define sRefTable_undefined ((sRefTable) NULL) @@ -37,7 +34,6 @@ extern /*@unused@*/ /*@falsewhennull@*/ bool # define sRefTable_isEmpty(s) ((s) == sRefTable_undefined || ((s)->entries == 0)) -extern /*@unused@*/ /*@only@*/ cstring sRefTable_unparse (sRefTable p_s) /*@*/ ; extern void sRefTable_free (/*@only@*/ sRefTable p_s) /*@modifies p_s@*/; extern void sRefTable_clear (sRefTable p_s) /*@modifies p_s@*/ ; extern sRefTable @@ -49,5 +45,3 @@ extern sRefTable # error "Multiple include" # endif - - diff --git a/src/Headers/shift.h b/src/Headers/shift.h index 36a30ad..11ce345 100644 --- a/src/Headers/shift.h +++ b/src/Headers/shift.h @@ -11,5 +11,3 @@ extern void LSLGenShift (ltoken p_tok); extern void LSLGenShiftOnly (/*@only@*/ ltoken p_tok); extern /*@only@*/ ltoken LSLGenTopPopShiftStack(void); - -extern void LSLGenInit(bool p_LSLParse); diff --git a/src/Headers/sigNodeSet.h b/src/Headers/sigNodeSet.h index ff2e750..ffd6552 100644 --- a/src/Headers/sigNodeSet.h +++ b/src/Headers/sigNodeSet.h @@ -51,14 +51,13 @@ extern int sigNodeSet_size (/*@sef@*/ sigNodeSet p_s) /*@*/ ; extern /*@only@*/ sigNodeSet sigNodeSet_new(void) /*@*/ ; extern /*@only@*/ sigNodeSet sigNodeSet_singleton (/*@owned@*/ sigNode p_el) /*@*/ ; extern bool sigNodeSet_insert (sigNodeSet p_s, /*@owned@*/ sigNode p_el) /*@modifies p_s@*/ ; +# if 0 extern /*@only@*/ cstring sigNodeSet_unparse (sigNodeSet p_s) /*@*/ ; +# endif extern /*@only@*/ cstring sigNodeSet_unparsePossibleAritys (sigNodeSet p_s) /*@*/ ; extern void sigNodeSet_free (/*@only@*/ sigNodeSet p_s); extern /*@only@*/ cstring sigNodeSet_unparseSomeSigs (sigNodeSet p_s) /*@*/ ; -/*@constant int sigNodeSetBASESIZE;@*/ -# define sigNodeSetBASESIZE MIDBASESIZE - # else # error "Multiple include" # endif diff --git a/src/Headers/sort.h b/src/Headers/sort.h index 9540a76..c096141 100644 --- a/src/Headers/sort.h +++ b/src/Headers/sort.h @@ -152,8 +152,6 @@ extern bool sort_setExporting (bool p_flag) /*@modifies internalState@*/ ; # define sort_isNoSort(s) ((s) == 0) /* assume NOSORTHANDLE is #define to 0 in sort.c */ -extern /*@unused@*/ void sort_printStats(void) /*@modifies g_warningstream@*/ ; - extern bool sort_equal (sort p_s1, sort p_s2) /*@*/ ; extern sort sort_fromLsymbol (lsymbol p_sortid) /*@modifies internalState@*/ ; @@ -172,4 +170,3 @@ extern sort g_sortDouble; # error "Multiple include" # endif - diff --git a/src/Headers/sortSet.h b/src/Headers/sortSet.h index 0dff13d..1e8e218 100644 --- a/src/Headers/sortSet.h +++ b/src/Headers/sortSet.h @@ -38,16 +38,12 @@ extern int sortSet_size (/*@sef@*/ sortSet p_s); extern /*@only@*/ sortSet sortSet_new(void); extern bool sortSet_insert (sortSet p_s, sort p_el); extern bool sortSet_member (sortSet p_s, sort p_el); -extern /*@only@*/ cstring sortSet_unparse (sortSet p_s); extern /*@only@*/ cstring sortSet_unparseClean (sortSet p_s); extern /*@only@*/ cstring sortSet_unparseOr (sortSet p_s); extern void sortSet_free (/*@only@*/ sortSet p_s); extern sort sortSet_choose (sortSet p_s); extern /*@only@*/ sortSet sortSet_copy (sortSet p_s); -/*@constant int sortSetBASESIZE;@*/ -# define sortSetBASESIZE MIDBASESIZE - # else # error "Multiple include" # endif diff --git a/src/Headers/sortSetList.h b/src/Headers/sortSetList.h index 017d4f1..28542b9 100644 --- a/src/Headers/sortSetList.h +++ b/src/Headers/sortSetList.h @@ -33,19 +33,12 @@ extern void sortSetList_addh (sortSetList p_s, /*@dependent@*/ /*@exposed@*/ sor extern void sortSetList_reset (sortSetList p_s) ; extern void sortSetList_advance (sortSetList p_s) ; /* was "list_pointToNext" */ -extern /*@unused@*/ /*@only@*/ cstring sortSetList_unparse (sortSetList p_s) ; extern void sortSetList_free (/*@only@*/ sortSetList p_s) ; extern /*@observer@*/ sortSet sortSetList_head (sortSetList p_s) ; extern /*@observer@*/ sortSet sortSetList_current (sortSetList p_s) ; -/*@constant int sortSetListBASESIZE;@*/ -# define sortSetListBASESIZE (8) - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/splintMacros.nf b/src/Headers/splintMacros.nf index 1d5a738..fa1ca0c 100644 --- a/src/Headers/splintMacros.nf +++ b/src/Headers/splintMacros.nf @@ -30,16 +30,6 @@ ** prevent it being skipped when +neverinclude is used.) */ -#ifndef PARAMS -#ifdef __STDC -/*@notfunction@*/ -#define PARAMS(P) P -#else -/*@notfunction@*/ -#define PARAMS(P) () -#endif -#endif /* !PARAMS */ - /*@notfunction@*/ # define BADEXIT \ /*@notreached@*/ do { llassertprint(FALSE, ("Reached dead code!")); \ @@ -77,13 +67,6 @@ }} while (FALSE) /*@notfunction@*/ -# define llassertprintret(tst,p,r) \ - do { if (!(tst)) \ - { llbug (message("%q:%d: %q", cstring_makeLiteral (__FILE__), __LINE__, message p)); \ - /*@-unreachable@*/ return (r); /*@=unreachable@*/ \ - } } while (FALSE) - -/*@notfunction@*/ # define abst_typedef typedef /*@abstract@*/ /*@notfunction@*/ @@ -125,7 +108,7 @@ */ /*@notfunction@*/ -# define DPRINTF(s) +# define DPRINTF(s) /*@notfunction@*/ # define INTCOMPARERETURN(x,y) \ diff --git a/src/Headers/stateClause.h b/src/Headers/stateClause.h index 6b14170..27191bd 100644 --- a/src/Headers/stateClause.h +++ b/src/Headers/stateClause.h @@ -66,7 +66,6 @@ extern bool stateClause_isGlobal (stateClause p_cl) /*@*/ ; extern bool stateClause_isBefore (stateClause p_cl) /*@*/ ; extern bool stateClause_isBeforeOnly (stateClause p_cl) /*@*/ ; extern bool stateClause_isAfter (stateClause p_cl) /*@*/ ; -extern bool stateClause_isEnsures (stateClause p_cl) /*@*/ ; extern bool stateClause_sameKind (stateClause p_s1, stateClause p_s2) /*@*/ ; @@ -91,12 +90,6 @@ extern stateClause extern stateClause stateClause_createPlain (lltok p_tok, /*@only@*/ sRefSet p_s) /*@*/ ; -extern stateClause stateClause_createDefines (/*@only@*/ sRefSet p_s) /*@*/ ; -extern stateClause stateClause_createUses (/*@only@*/ sRefSet p_s) /*@*/ ; -extern stateClause stateClause_createAllocates (/*@only@*/ sRefSet p_s) /*@*/ ; -extern stateClause stateClause_createReleases (/*@only@*/ sRefSet p_s) /*@*/ ; -extern stateClause stateClause_createSets (/*@only@*/ sRefSet p_s) /*@*/ ; - extern /*@observer@*/ fileloc stateClause_loc (stateClause) /*@*/ ; extern bool stateClause_isMemoryAllocation (stateClause p_cl) /*@*/ ; extern bool stateClause_isQual (stateClause p_cl) /*@*/ ; @@ -121,4 +114,3 @@ extern bool stateClause_isMetaState (stateClause p_s); # error "Multiple include" # endif - diff --git a/src/Headers/stateClauseList.h b/src/Headers/stateClauseList.h index 00a01f0..39e6ccf 100644 --- a/src/Headers/stateClauseList.h +++ b/src/Headers/stateClauseList.h @@ -47,11 +47,6 @@ extern /*@only@*/ stateClauseList stateClauseList_copy (stateClauseList p_s) /*@ extern cstring stateClauseList_dump (stateClauseList p_s) /*@*/ ; extern stateClauseList stateClauseList_undump (char **p_s) /*@modifies *p_s@*/ ; -extern int stateClauseList_compare (stateClauseList p_s1, stateClauseList p_s2) /*@*/ ; - -/*@constant int stateClauseListBASESIZE;@*/ -# define stateClauseListBASESIZE MIDBASESIZE - extern void stateClauseList_checkEqual (uentry p_old, uentry p_unew) /*@modifies g_warningstream@*/ ; @@ -86,4 +81,3 @@ extern void stateClauseList_checkEqual (uentry p_old, uentry p_unew) # error "Multiple include" # endif - diff --git a/src/Headers/stateInfo.h b/src/Headers/stateInfo.h index e686ed6..ac44fd0 100644 --- a/src/Headers/stateInfo.h +++ b/src/Headers/stateInfo.h @@ -96,9 +96,6 @@ extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) ; extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeLoc (fileloc p_loc, stateAction p_action) /*@*/ ; -extern /*@only@*/ /*@notnull@*/ stateInfo -stateInfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc, stateAction p_action) /*@*/ ; - extern /*@observer@*/ fileloc stateInfo_getLoc (stateInfo p_info) ; extern /*@only@*/ cstring stateInfo_unparse (stateInfo p_s) /*@*/ ; diff --git a/src/Headers/stateValue.h b/src/Headers/stateValue.h index 9101906..edc5e4a 100644 --- a/src/Headers/stateValue.h +++ b/src/Headers/stateValue.h @@ -37,8 +37,6 @@ extern bool stateValue_isImplicit (stateValue) /*@*/ ; extern int stateValue_getValue (stateValue p_s) /*@*/ ; -extern void stateValue_update (stateValue p_res, stateValue p_val) /*@modifies p_res@*/ ; - extern /*@observer@*/ fileloc stateValue_getLoc (stateValue p_s) /*@*/ ; # define stateValue_getLoc(p_s) (stateInfo_getLoc (stateValue_getInfo (p_s))) @@ -46,8 +44,6 @@ extern bool stateValue_hasLoc (stateValue p_s) /*@*/ ; extern /*@observer@*/ stateInfo stateValue_getInfo (stateValue p_s) /*@*/ ; -extern void stateValue_updateValue (/*@sef@*/ stateValue p_s, int p_value, /*@only@*/ stateInfo p_info) /*@modifies p_s@*/ ; - extern void stateValue_updateValueLoc (stateValue p_s, int p_value, fileloc p_loc) /*@modifies p_s@*/ ; extern void stateValue_show (stateValue p_s, metaStateInfo p_msinfo) ; @@ -59,8 +55,6 @@ extern /*@only@*/ cstring extern cstring stateValue_unparse (stateValue p_s) /*@*/ ; -extern bool stateValue_sameValue (stateValue p_s1, stateValue p_s2) /*@*/ ; - extern bool stateValue_isError (/*@sef@*/ stateValue p_s) /*@*/ ; # define stateValue_isError(p_s) (stateValue_isDefined (p_s) && (stateValue_getValue (p_s) == stateValue_error)) diff --git a/src/Headers/stmtNode.h b/src/Headers/stmtNode.h index a3f9066..9f3bfc8 100644 --- a/src/Headers/stmtNode.h +++ b/src/Headers/stmtNode.h @@ -9,4 +9,3 @@ struct s_stmtNode { termNodeList args; } ; -extern /*@unused@*/ /*@notnull@*/ /*@only@*/ cstring stmtNode_unparse (stmtNode p_x); diff --git a/src/Headers/strOrUnionNode.h b/src/Headers/strOrUnionNode.h index 8c29057..c8365dc 100644 --- a/src/Headers/strOrUnionNode.h +++ b/src/Headers/strOrUnionNode.h @@ -12,6 +12,3 @@ typedef struct { sort sort; /*@owned@*/ stDeclNodeList structdecls; } *strOrUnionNode; - -extern /*@unused@*/ cstring - strOrUnionNode_unparse (/*@null@*/ strOrUnionNode p_n); diff --git a/src/Headers/symtable.h b/src/Headers/symtable.h index 4c12d58..f6ec578 100644 --- a/src/Headers/symtable.h +++ b/src/Headers/symtable.h @@ -174,8 +174,6 @@ extern void symtable_dump(symtable p_stable, FILE *p_f, bool p_lco); extern void symtable_import(inputStream p_imported, ltoken p_tok, mapping p_map); -extern /*@unused@*/ void symtable_printStats (symtable p_s); - extern lsymbol lsymbol_sortFromType (symtable, lsymbol); extern cstring tagKind_unparse (tagKind p_k); extern lsymbol lsymbol_translateSort (mapping p_m, lsymbol p_s); diff --git a/src/Headers/taggedUnionNode.h b/src/Headers/taggedUnionNode.h index 9b73bc2..ec137ba 100644 --- a/src/Headers/taggedUnionNode.h +++ b/src/Headers/taggedUnionNode.h @@ -8,5 +8,3 @@ typedef struct { declaratorNode declarator; } *taggedUnionNode; -extern /*@unused@*/ /*@only@*/ cstring - taggedUnionNode_unparse (taggedUnionNode p_n) /*@*/ ; diff --git a/src/Headers/traitRefNodeList.h b/src/Headers/traitRefNodeList.h index c6ae4dd..2d3a402 100644 --- a/src/Headers/traitRefNodeList.h +++ b/src/Headers/traitRefNodeList.h @@ -26,16 +26,9 @@ extern /*@only@*/ traitRefNodeList traitRefNodeList_new(void); extern traitRefNodeList traitRefNodeList_add (/*@returned@*/ traitRefNodeList p_s, /*@only@*/ traitRefNode p_el); -extern /*@only@*/ cstring traitRefNodeList_unparse (traitRefNodeList p_s) ; extern void traitRefNodeList_free (/*@only@*/ traitRefNodeList p_s) ; -/*@constant int traitRefNodeListBASESIZE;@*/ -# define traitRefNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/typeExpr.h b/src/Headers/typeExpr.h index 42b44ba..86537bc 100644 --- a/src/Headers/typeExpr.h +++ b/src/Headers/typeExpr.h @@ -30,14 +30,8 @@ struct s_typeExpr sort sort; } ; -extern void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr p_x); extern /*@only@*/ cstring typeExpr_unparse (/*@null@*/ typeExpr p_x); -extern /*@only@*/ cstring typeExpr_unparseNoBase (/*@null@*/ typeExpr p_x); /* like a declaratorNode but without varId */ typedef typeExpr abstDeclaratorNode; -extern void abstDeclaratorNode_free (/*@only@*/ /*@null@*/ abstDeclaratorNode p_x); -# define abstDeclaratorNode_free(x) typeExpr_free(x); - - diff --git a/src/Headers/typeNameNodeList.h b/src/Headers/typeNameNodeList.h index c749347..958d728 100644 --- a/src/Headers/typeNameNodeList.h +++ b/src/Headers/typeNameNodeList.h @@ -34,16 +34,9 @@ extern /*@only@*/ typeNameNodeList typeNameNodeList_new(void); extern typeNameNodeList typeNameNodeList_add (/*@returned@*/ typeNameNodeList p_s, /*@only@*/ typeNameNode p_el) ; -extern /*@only@*/ cstring typeNameNodeList_unparse (typeNameNodeList p_s) ; extern void typeNameNodeList_free (/*@only@*/ typeNameNodeList p_s) ; -/*@constant int typeNameNodeListBASESIZE;@*/ -# define typeNameNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/typeNode.h b/src/Headers/typeNode.h index 68881a8..4e97ef5 100644 --- a/src/Headers/typeNode.h +++ b/src/Headers/typeNode.h @@ -15,9 +15,6 @@ typedef struct { } content; } *typeNode; -extern /*@unused@*/ /*@only@*/ cstring - typeNode_unparse (/*@null@*/ typeNode p_t) /*@*/ ; - # else # error "Multiple include" # endif diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index d60d77f..e11b8c0 100644 --- a/src/Headers/uentry.h +++ b/src/Headers/uentry.h @@ -510,12 +510,8 @@ extern bool uentry_hasWarning (uentry p_ue) /*@*/ ; extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn) /*@modifies p_ue*/; -extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses) - /*@modifies p_ue@*/ ; - extern void uentry_setType (uentry p_e, ctype p_t); -extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue); extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ; extern void @@ -573,7 +569,9 @@ extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modif extern bool uentry_isYield (uentry p_ue) /*@*/ ; extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ; extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ; +# if 0 extern int uentry_xcomparealpha (uentry *p_p1, uentry *p_p2) /*@*/ ; +# endif extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ; extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ; extern void uentry_copyState (uentry p_res, uentry p_other); @@ -582,7 +580,6 @@ extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, f extern bool uentry_isReturned (uentry p_u); extern bool uentry_isRefCountedDatatype (uentry p_e); extern sstate uentry_getDefState (uentry p_u); -extern /*@unused@*/ void uentry_markFree (/*@owned@*/ uentry p_u); extern /*@dependent@*/ sRef uentry_getOrigSref (uentry p_e); extern void uentry_destroyMod (void) /*@modifies internalState@*/; extern void uentry_showDefSpecInfo (uentry p_ce, fileloc p_fwhere); @@ -618,9 +615,6 @@ extern void uentry_setSize(uentry p_e, int p_size); extern void uentry_setLen(uentry p_e, int p_len); 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) /*@*/ ; /* Global Markers */ @@ -665,5 +659,3 @@ extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ; # error "Multiple include" # endif - - diff --git a/src/Headers/usymtab.h b/src/Headers/usymtab.h index 0a8961d..5df84c3 100644 --- a/src/Headers/usymtab.h +++ b/src/Headers/usymtab.h @@ -86,7 +86,9 @@ extern void usymtab_printLocal (void) extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno) /*@globals internalState@*/; +# if 0 extern void usymtab_free (void) /*@modifies internalState@*/ ; +# endif extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ; extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k) @@ -378,8 +380,9 @@ extern void usymtab_checkDistinctName (uentry p_e, int p_scope) /*@modifies *g_warningstream, p_e@*/ ; extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ; -extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ; +# if 0 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ; +# endif # ifdef DEBUGSPLINT extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ; @@ -389,5 +392,3 @@ extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ; # error "Multiple include" # endif - - diff --git a/src/Headers/valueTable.h b/src/Headers/valueTable.h index ea76b57..b2cded4 100644 --- a/src/Headers/valueTable.h +++ b/src/Headers/valueTable.h @@ -41,9 +41,6 @@ extern bool valueTable_contains (valueTable p_h, cstring p_key) /*@*/ ; # define valueTable_contains(p_h,p_key) \ (stateValue_isDefined (valueTable_lookup (p_h, p_key))) -extern /*@unused@*/ /*@only@*/ cstring valueTable_stats(valueTable p_h); -# define valueTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) - extern void valueTable_free (/*@only@*/ valueTable p_h); # define valueTable_free(p_h) (genericTable_free ((genericTable) (p_h))) @@ -66,6 +63,3 @@ extern int valueTable_size (valueTable p_h) /*@*/ ; # error "Multiple include" # endif - - - diff --git a/src/Headers/varDeclarationNode.h b/src/Headers/varDeclarationNode.h index 60f7630..c5f95e0 100644 --- a/src/Headers/varDeclarationNode.h +++ b/src/Headers/varDeclarationNode.h @@ -17,8 +17,6 @@ typedef struct { } *varDeclarationNode; extern void varDeclarationNode_free (/*@only@*/ /*@null@*/ varDeclarationNode p_x); -extern /*@unused@*/ /*@only@*/ cstring - varDeclarationNode_unparse (/*@null@*/ varDeclarationNode p_x) /*@*/; # else # error "Multiple include" diff --git a/src/Headers/varDeclarationNodeList.h b/src/Headers/varDeclarationNodeList.h index 245de53..905c6c0 100644 --- a/src/Headers/varDeclarationNodeList.h +++ b/src/Headers/varDeclarationNodeList.h @@ -29,16 +29,9 @@ extern void /*@keep@*/ varDeclarationNode p_el) /*@modifies p_s@*/ ; -extern /*@only@*/ cstring varDeclarationNodeList_unparse (varDeclarationNodeList p_s) /*@*/ ; extern void varDeclarationNodeList_free (/*@only@*/ varDeclarationNodeList p_s) ; -/*@constant int varDeclarationNodeListBASESIZE;@*/ -# define varDeclarationNodeListBASESIZE SMALLBASESIZE - # else # error "Multiple include" # endif - - - diff --git a/src/Headers/varNode.h b/src/Headers/varNode.h index 6c594d5..aa3363d 100644 --- a/src/Headers/varNode.h +++ b/src/Headers/varNode.h @@ -14,7 +14,6 @@ typedef struct { /* with sort, useful in quantified */ } *varNode; extern varNode varNode_copy (varNode p_x); -extern void varNode_free (/*@only@*/ /*@null@*/ varNode p_x); # else # error "Multiple include" diff --git a/src/Headers/varNodeList.h b/src/Headers/varNodeList.h index fdbd358..96e4c83 100644 --- a/src/Headers/varNodeList.h +++ b/src/Headers/varNodeList.h @@ -28,15 +28,8 @@ extern varNodeList varNodeList_add (/*@returned@*/ varNodeList p_s, /*@only@*/ v extern varNodeList varNodeList_copy (varNodeList p_s); extern /*@only@*/ cstring varNodeList_unparse (varNodeList p_s) ; -extern void varNodeList_free (/*@only@*/ varNodeList p_s) ; - -/*@constant int varNodeListBASESIZE;@*/ -# define varNodeListBASESIZE SMALLBASESIZE # else # error "Multiple include" # endif - - - diff --git a/src/Makefile.am b/src/Makefile.am index 51a2bce..87050e4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -51,7 +51,6 @@ LISTSRC = \ flagSpec.c \ idDeclList.c \ qualList.c \ - sRefList.c \ sRefSetList.c \ uentryList.c @@ -455,7 +454,6 @@ HEADERSRC = \ $(INCDIR)/sortSet.h \ $(INCDIR)/sortSetList.h \ $(INCDIR)/sRef.h \ - $(INCDIR)/sRefList.h \ $(INCDIR)/sRefSet.h \ $(INCDIR)/sRefSetList.h \ $(INCDIR)/sRefTable.h \ diff --git a/src/abstract.c b/src/abstract.c index 2fd2f1e..435f273 100644 --- a/src/abstract.c +++ b/src/abstract.c @@ -38,7 +38,6 @@ # include "basic.h" # include "lslparse.h" # include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */ -# include "lclscan.h" # include "lh.h" # include "imports.h" @@ -71,6 +70,8 @@ static /*@only@*/ lclTypeSpecNode lclTypeSpecNode_copySafe (lclTypeSpecNode p_n) /*@*/ ; static void lclTypeSpecNode_free (/*@null@*/ /*@only@*/ lclTypeSpecNode p_n); static void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack p_x); +static /*@unused@*/ /*@only@*/ cstring + opFormNode_unparse (/*@null@*/ opFormNode p_n) /*@*/ ; static void opFormNode_free (/*@only@*/ /*@null@*/ opFormNode p_op); static quantifiedTermNode quantifiedTermNode_copy (quantifiedTermNode p_q) /*@*/ ; static void nameAndReplaceNode_free (/*@only@*/ /*@null@*/ nameAndReplaceNode p_x); @@ -95,6 +96,16 @@ static void LCLBootstrap (void); static cstring printMiddle (int p_j); static void paramNode_checkQualifiers (lclTypeSpecNode p_t, typeExpr p_d); +static /*@only@*/ cstring enumSpecNode_unparse(/*@null@*/ enumSpecNode p_n) /*@*/ ; +static /*@only@*/ cstring strOrUnionNode_unparse (/*@null@*/ strOrUnionNode p_n); + +static void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr p_x); +static /*@only@*/ cstring typeExpr_unparseNoBase (/*@null@*/ typeExpr p_x); + +void abstDeclaratorNode_free (/*@only@*/ /*@null@*/ abstDeclaratorNode p_x); +# define abstDeclaratorNode_free(x) typeExpr_free(x); + + void resetImports (cstring current) { @@ -497,6 +508,7 @@ interfaceNode_makePrivFcn (/*@only@*/ fcnNode x) return (i); } +# ifdef DEADCODE /*@only@*/ cstring exportNode_unparse (exportNode n) { @@ -549,6 +561,7 @@ privateNode_unparse (privateNode n) } return cstring_undefined; } +# endif /* DEADCODE */ void lclPredicateNode_free (/*@null@*/ /*@only@*/ lclPredicateNode x) { @@ -560,6 +573,7 @@ void lclPredicateNode_free (/*@null@*/ /*@only@*/ lclPredicateNode x) } } +# ifdef DEADCODE static /*@only@*/ cstring lclPredicateNode_unparse (/*@null@*/ lclPredicateNode p) /*@*/ { @@ -597,6 +611,7 @@ lclPredicateNode_unparse (/*@null@*/ lclPredicateNode p) /*@*/ } return cstring_undefined; } +# endif /* DEADCODE */ bool ltoken_similar (ltoken t1, ltoken t2) @@ -624,6 +639,7 @@ ltoken_similar (ltoken t1, ltoken t2) return FALSE; } +# ifdef DEADCODE /*@only@*/ cstring iterNode_unparse (/*@null@*/ iterNode i) { @@ -722,6 +738,7 @@ constDeclarationNode_unparse (/*@null@*/ constDeclarationNode x) return cstring_undefined; } +# endif /* DEADCODE */ /*@only@*/ storeRefNode makeStoreRefNodeTerm (/*@only@*/ termNode t) @@ -1191,6 +1208,7 @@ makeRenamingNode (/*@only@*/ typeNameNodeList n, /*@only@*/ replaceNodeList r) return (ren); } +# ifdef DEADCODE /*@only@*/ cstring renamingNode_unparse (/*@null@*/ renamingNode x) { @@ -1208,6 +1226,7 @@ renamingNode_unparse (/*@null@*/ renamingNode x) } return cstring_undefined; } +# endif /* DEADCODE */ /*@only@*/ replaceNode makeReplaceNameNode (ltoken t, typeNameNode tn, nameNode nn) @@ -1250,6 +1269,7 @@ makeReplaceNode (ltoken t, typeNameNode tn, return (r); } +# ifdef DEADCODE /*@only@*/ cstring replaceNode_unparse (/*@null@*/ replaceNode x) { @@ -1272,6 +1292,7 @@ replaceNode_unparse (/*@null@*/ replaceNode x) } return cstring_undefined; } +# endif /* DEADCODE */ /*@only@*/ nameNode makeNameNodeForm (/*@only@*/ /*@null@*/ opFormNode opform) @@ -1523,7 +1544,7 @@ static cstring printMiddle (int j) return cstring_fromCharsO (s); } -/*@only@*/ cstring +static /*@only@*/ cstring opFormNode_unparse (/*@null@*/ opFormNode n) { if (n != (opFormNode) 0) @@ -1849,7 +1870,7 @@ makeEnumSpecNode2 (ltoken t, ltoken tagid) return (n); } -/*@only@*/ cstring +static /*@only@*/ cstring enumSpecNode_unparse (/*@null@*/ enumSpecNode n) { if (n != (enumSpecNode) 0) @@ -2003,7 +2024,7 @@ makeForwardstrOrUnionNode (ltoken str, suKind k, ltoken tagid) { strOrUnionNode n = (strOrUnionNode) dmalloc (sizeof (*n)); - sort sort = sort_makeNoSort (); + sort sort; tagInfo t; /* a reference, not a definition */ @@ -2059,7 +2080,7 @@ makeForwardstrOrUnionNode (ltoken str, suKind k, return (n); } -/*@only@*/ cstring +static /*@only@*/ cstring strOrUnionNode_unparse (/*@null@*/ strOrUnionNode n) { if (n != (strOrUnionNode) 0) @@ -2287,7 +2308,7 @@ static /*@only@*/ cstring return s; } -void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x) +static void typeExpr_free (/*@only@*/ /*@null@*/ typeExpr x) { if (x != (typeExpr) 0) { @@ -2378,7 +2399,7 @@ typeExpr_unparse (/*@null@*/ typeExpr x) return s; } -/*@only@*/ cstring +static /*@only@*/ cstring typeExpr_unparseNoBase (/*@null@*/ typeExpr x) { cstring s = cstring_undefined; /* print out types in order of appearance in source */ @@ -2745,6 +2766,7 @@ makeAbstractNode (ltoken t, ltoken name, return n; } +# ifdef DEADCODE /*@only@*/ cstring abstractNode_unparse (abstractNode n) { @@ -2762,6 +2784,7 @@ abstractNode_unparse (abstractNode n) } return cstring_undefined; } +# endif /* DEADCODE */ void setExposedType (lclTypeSpecNode s) @@ -2782,6 +2805,7 @@ makeExposedNode (ltoken t, lclTypeSpecNode s, return n; } +# ifdef DEADCODE /*@only@*/ cstring exposedNode_unparse (exposedNode n) { @@ -2793,6 +2817,7 @@ exposedNode_unparse (exposedNode n) } return cstring_undefined; } +# endif /* DEADCODE */ /*@only@*/ declaratorInvNode makeDeclaratorInvNode (declaratorNode d, abstBodyNode b) @@ -2804,6 +2829,7 @@ makeDeclaratorInvNode (declaratorNode d, abstBodyNode b) return (n); } +# ifdef DEADCODE /*@only@*/ cstring declaratorInvNode_unparse (declaratorInvNode d) { @@ -2842,6 +2868,7 @@ taggedUnionNode_unparse (taggedUnionNode n) } return cstring_undefined; } +# endif /* DEADCODE */ static /*@observer@*/ paramNodeList typeExpr_toParamNodeList (/*@null@*/ typeExpr te) @@ -3428,7 +3455,7 @@ lclTypeSpecNode_unparseAltComments (/*@null@*/ lclTypeSpecNode typespec) /*@*/ cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec) { - if (typespec != (lclTypeSpecNode) 0) + if (typespec != lclTypeSpecNode_undefined) { cstring s = qualList_toCComments (typespec->quals); @@ -3519,7 +3546,7 @@ cstring lclTypeSpecNode_unparseComments (/*@null@*/ lclTypeSpecNode typespec) ("%q /*@alt %q@*/", lclTypeSpecNode_unparseComments (typespec->content.conj->a), lclTypeSpecNode_unparseAltComments (typespec->content.conj->b))); - } + } BADDEFAULT; } } @@ -4325,6 +4352,7 @@ makeUnchangedTermNode2 (ltoken op, storeRefNodeList x) return (t); } +# ifdef DEADCODE /*@only@*/ cstring claimNode_unparse (claimNode c) { @@ -4344,6 +4372,7 @@ claimNode_unparse (claimNode c) } return cstring_undefined; } +# endif /* DEADCODE */ static void WrongArity (ltoken tok, int expect, int size) @@ -4761,6 +4790,7 @@ static void modifyNode_free (/*@null@*/ /*@only@*/ modifyNode m) } } +# ifdef DEADCODE /*@only@*/ cstring modifyNode_unparse (/*@null@*/ modifyNode m) { @@ -4843,6 +4873,7 @@ stmtNode_unparse (stmtNode x) return s; } +# endif /* DEADCODE */ /*@only@*/ lslOp makelslOpNode (/*@only@*/ /*@null@*/ nameNode name, @@ -4871,6 +4902,7 @@ stmtNode_unparse (stmtNode x) return x; } +# ifdef DEADCODE /*@only@*/ cstring lslOp_unparse (lslOp x) { @@ -4888,6 +4920,7 @@ lslOp_unparse (lslOp x) return cstring_fromCharsO (s); } +# endif /* DEADCODE */ static bool sameOpFormNode (/*@null@*/ opFormNode n1, /*@null@*/ opFormNode n2) @@ -5060,7 +5093,7 @@ makeTypeSpecifier (ltoken typedefname) if (ltoken_getText (typedefname) == lsymbol_bool) { - lhIncludeBool (); + /* empty */ ; } if (typeInfo_exists (ti)) @@ -5946,6 +5979,7 @@ quantifierNode quantifierNode_copy (quantifierNode x) return ret; } +# ifdef DEADCODE void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x) { if (x != NULL) @@ -5955,6 +5989,7 @@ void quantifierNode_free (/*@null@*/ /*@only@*/ quantifierNode x) sfree (x); } } +# endif /* DEADCODE */ void replaceNode_free (/*@only@*/ /*@null@*/ replaceNode x) { @@ -6088,6 +6123,7 @@ varNode varNode_copy (varNode x) return ret; } +# ifdef DEADCODE void varNode_free (/*@only@*/ /*@null@*/ varNode x) { if (x != NULL) @@ -6097,6 +6133,7 @@ void varNode_free (/*@only@*/ /*@null@*/ varNode x) sfree (x); } } +# endif /* DEADCODE */ void stmtNode_free (/*@only@*/ /*@null@*/ stmtNode x) { @@ -6146,6 +6183,7 @@ void typeNamePack_free (/*@only@*/ /*@null@*/ typeNamePack x) } } +# ifdef DEADCODE cstring interfaceNode_unparse (interfaceNode x) { if (x != NULL) @@ -6171,6 +6209,7 @@ cstring interfaceNode_unparse (interfaceNode x) BADBRANCHRET (cstring_undefined); } +# endif /* DEADCODE */ void interfaceNode_free (/*@null@*/ /*@only@*/ interfaceNode x) { diff --git a/src/aliasTable.c b/src/aliasTable.c index fbc0732..c38f2a0 100644 --- a/src/aliasTable.c +++ b/src/aliasTable.c @@ -387,7 +387,6 @@ static /*@only@*/ sRefSet aliasTable_aliasedByLimit (aliasTable s, sRef sr, int { sRefSet res; - if (sRef_isConj (sr)) { res = sRefSet_unionFree (aliasTable_canAlias (s, sRef_getConjA (sr)), @@ -396,9 +395,9 @@ static /*@only@*/ sRefSet aliasTable_aliasedByLimit (aliasTable s, sRef sr, int else { res = aliasTable_canAliasAux (s, sr, 0); - } + } - return res; + return res; } /* @@ -484,6 +483,7 @@ static /*@only@*/ sRefSet else { BADBRANCH; + ret = sRefSet_undefined; } if (ind != ATINVALID) diff --git a/src/annotationInfo.c b/src/annotationInfo.c index c3fd230..f653a3e 100644 --- a/src/annotationInfo.c +++ b/src/annotationInfo.c @@ -175,6 +175,7 @@ cstring annotationInfo_dump (annotationInfo a) BADBRANCHRET (annotationInfo_undefined); } +# ifdef DEADCODE void annotationInfo_showContextRefError (annotationInfo a, sRef sr) { mtContextNode mcontext; @@ -201,3 +202,4 @@ void annotationInfo_showContextRefError (annotationInfo a, sRef sr) mtContextNode_showRefError (mcontext, sr); } } +# endif /* DEADCODE */ diff --git a/src/cgrammar.y b/src/cgrammar.y index 943236c..775a855 100644 --- a/src/cgrammar.y +++ b/src/cgrammar.y @@ -91,7 +91,6 @@ qualList tquallist; ctype ctyp; /*@dependent@*/ sRef sr; - /*@only@*/ sRef osr; /*@only@*/ functionClauseList funcclauselist; /*@only@*/ functionClause funcclause; @@ -108,7 +107,6 @@ /*@only@*/ metaStateExpression msexpr; /*@observer@*/ metaStateInfo msinfo; - /*@only@*/ sRefList srlist; /*@only@*/ globSet globset; /*@only@*/ qtype qtyp; /*@only@*/ cstring cname; @@ -1638,9 +1636,8 @@ paramTypeList ; paramList - : { storeLoc (); } paramDecl { $$ = uentryList_single ($2); } - | paramList TCOMMA { storeLoc (); } paramDecl - { $$ = uentryList_add ($1, $4); } + : { ; } paramDecl { $$ = uentryList_single ($2); } + | paramList TCOMMA { ; } paramDecl { $$ = uentryList_add ($1, $4); } ; paramDecl diff --git a/src/checking.c b/src/checking.c index c574aee..d8a0e49 100644 --- a/src/checking.c +++ b/src/checking.c @@ -35,7 +35,6 @@ # include "basic.h" # include "llgrammar.h" # include "checking.h" -# include "lclscan.h" /*@+ignorequals@*/ diff --git a/src/clabstract.c b/src/clabstract.c index 3dbaffa..e4689ee 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -30,13 +30,11 @@ # include "splintMacros.nf" # include "basic.h" -# include "usymtab_interface.h" +# include "cscannerHelp.h" # include "structNames.h" # include "nameChecks.h" -# include "cgrammar.h" - /* ** Lots of variables are needed because of interactions with the ** parser. This is easier than restructuring the grammar so the @@ -47,7 +45,6 @@ static /*@only@*/ constraintList implicitFcnConstraints = NULL; static void clabstract_prepareFunction (uentry p_e) /*@modifies p_e@*/ ; -static bool fcnNoGlobals = FALSE; static void processVariable (/*@temp@*/ idDecl p_t) /*@modifies internalState@*/ ; static bool s_processingVars = FALSE; @@ -62,7 +59,6 @@ static /*@owned@*/ uentry saveFunction = uentry_undefined; static int saveIterParamNo; static idDecl fixStructDecl (/*@returned@*/ idDecl p_d); static void checkTypeDecl (uentry p_e, ctype p_rep); -static /*@dependent@*/ fileloc saveStoreLoc = fileloc_undefined; static storageClassCode storageClass = SCNONE; static void declareEnumList (/*@temp@*/ enumNameList p_el, ctype p_c, fileloc p_loc); static void resetGlobals (void); @@ -167,16 +163,6 @@ static void reflectStorageClass (uentry u) } -void storeLoc (void) -{ - saveStoreLoc = g_currentloc; -} - -void setFunctionNoGlobals (void) -{ - fcnNoGlobals = TRUE; -} - static void reflectGlobalQualifiers (sRef sr, qualList quals) { DPRINTF (("Reflect global qualifiers: %s / %s", @@ -285,7 +271,7 @@ extern void declareCIter (cstring name, /*@owned@*/ uentryList params) fileloc_copy (g_currentloc)); usymtab_supEntry (uentry_makeEndIter (name, fileloc_copy (g_currentloc))); - ue = usymtab_supGlobalEntryReturn (ue); + (void) usymtab_supGlobalEntryReturn (ue); } extern void nextIterParam (void) @@ -309,8 +295,6 @@ makeCurrentParam (idDecl t) { uentry ue; - saveStoreLoc = fileloc_undefined; - /* param number unknown */ ue = uentry_makeParam (t, 0); @@ -1161,33 +1145,11 @@ void setProcessingGlobalsList (void) { s_processingGlobals = TRUE; - fcnNoGlobals = FALSE; -} - -static bool ProcessingGlobMods = FALSE; - -void -setProcessingGlobMods (void) -{ - ProcessingGlobMods = TRUE; -} - -void -clearProcessingGlobMods (void) -{ - ProcessingGlobMods = FALSE; -} - -bool -isProcessingGlobMods (void) -{ - return (ProcessingGlobMods); } static void resetGlobals (void) { s_processingGlobals = FALSE; - fcnNoGlobals = FALSE; } void @@ -1290,6 +1252,12 @@ checkDoneParams (void) } } +static void +unsetProcessingTypedef (void) +{ + s_processingTypedef = FALSE; +} + void clabstract_declareType (/*@only@*/ exprNodeList decls, /*@only@*/ warnClause warn) { llassert (s_processingTypedef); @@ -1331,12 +1299,6 @@ void clabstract_declareType (/*@only@*/ exprNodeList decls, /*@only@*/ warnClaus unsetProcessingTypedef (); } -void -unsetProcessingTypedef (void) -{ - s_processingTypedef = FALSE; -} - void checkConstant (qtype t, idDecl id) { uentry e; @@ -1628,7 +1590,7 @@ void processNamedDecl (idDecl t) reflectStorageClass (e); checkTypeDecl (e, ct); - e = usymtab_supReturnTypeEntry (e); + (void) usymtab_supReturnTypeEntry (e); } else { diff --git a/src/clause.c b/src/clause.c index 1a0f41f..d167d93 100644 --- a/src/clause.c +++ b/src/clause.c @@ -49,7 +49,7 @@ clause_unparse (clause cl) case FALSEEXITCLAUSE: return (cstring_makeLiteralTemp ("falseexit")); } - BADEXIT; + BADBRANCHRET (cstring_undefined); } cstring diff --git a/src/constraint.c b/src/constraint.c index 5778762..c34957f 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -31,12 +31,14 @@ # include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" -# include "exprChecks.h" -# include "exprNodeSList.h" static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c); +/*drl added 12/19/2002 */ +static bool +constraint_isConstantOnly (constraint p_c); + static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void) /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/; @@ -140,6 +142,7 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c) } } +# ifdef DEADCODE /*like copy except it doesn't allocate memory for the constraint*/ void constraint_overWrite (constraint c1, constraint c2) @@ -181,7 +184,7 @@ void constraint_overWrite (constraint c1, constraint c2) c1->generatingExpr = c2->generatingExpr; /*@=assignexpose@*/ } - +# endif /* DEADCODE */ static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void) @@ -294,8 +297,6 @@ constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind) { constraint ret = constraint_makeNew (); - po = po; - ind = ind; ret->lexpr = constraintExpr_makeMaxReadExpr (po); ret->ar = GTE; ret->expr = constraintExpr_makeValueExpr (ind); @@ -635,6 +636,7 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc) } } +# ifdef DEADCODE /*drl added 8-11-001*/ cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/ { @@ -650,7 +652,7 @@ cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/ return ret; } - +# endif /* DEADCODE */ void constraint_printError (constraint c, fileloc loc) @@ -695,7 +697,7 @@ void constraint_printError (constraint c, fileloc loc) } /*drl added 12/19/2002 print - a different error fro "likely" bounds-errors*/ + a different error for "likely" bounds-errors*/ isLikely = constraint_isConstantOnly (c); @@ -775,7 +777,7 @@ static cstring constraint_unparseDeep (constraint c) static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c) { - cstring st = cstring_undefined; + cstring st; cstring genExpr; llassert (constraint_isDefined (c) ); @@ -805,8 +807,8 @@ static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@ cstring constraint_unparseDetailed (constraint c) { - cstring st = cstring_undefined; - cstring temp = cstring_undefined; + cstring st; + cstring temp; cstring genExpr; bool isLikely; @@ -863,48 +865,36 @@ cstring constraint_unparseDetailed (constraint c) /*@only@*/ cstring constraint_unparse (constraint c) /*@*/ { - cstring st = cstring_undefined; - cstring type = cstring_undefined; + cstring st; + cstring type; + llassert (c !=NULL); + if (c->post) { - if (context_getFlag (FLG_PARENCONSTRAINT)) - { - type = cstring_makeLiteral ("ensures: "); - } - else - { - type = cstring_makeLiteral ("ensures"); - } + type = cstring_makeLiteral ("ensures"); } else { - if (context_getFlag (FLG_PARENCONSTRAINT)) - { - type = cstring_makeLiteral ("requires: "); - } - else - { - type = cstring_makeLiteral ("requires"); - } - + type = cstring_makeLiteral ("requires"); + } + + if (context_getFlag (FLG_PARENCONSTRAINT)) + { + st = message ("%q: : %q %q %q", + type, + constraintExpr_print (c->lexpr), + arithType_print (c->ar), + constraintExpr_print (c->expr)); + } + else + { + st = message ("%q %q %q %q", + type, + constraintExpr_print (c->lexpr), + arithType_print (c->ar), + constraintExpr_print (c->expr)); } - if (context_getFlag (FLG_PARENCONSTRAINT)) - { - st = message ("%q: %q %q %q", - type, - constraintExpr_print (c->lexpr), - arithType_print (c->ar), - constraintExpr_print (c->expr)); - } - else - { - st = message ("%q %q %q %q", - type, - constraintExpr_print (c->lexpr), - arithType_print (c->ar), - constraintExpr_print (c->expr)); - } return st; } @@ -934,6 +924,7 @@ cstring constraint_unparseOr (constraint c) /*@*/ } +# ifdef DEADCODE /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, exprNodeList arglist) { @@ -947,7 +938,7 @@ cstring constraint_unparseOr (constraint c) /*@*/ return precondition; } - +# endif /* DEADCODE */ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall) { @@ -1012,14 +1003,12 @@ constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @ if (c->orig->orig == NULL) { c->orig->orig = temp; - temp = NULL; } else { llcontbug ((message ("Expected c->orig->orig to be null"))); constraint_free (c->orig->orig); c->orig->orig = temp; - temp = NULL; } } else @@ -1227,7 +1216,8 @@ bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c) /*drl added 12/19/2002*/ /*whether constraints consist only of terms which are constants*/ -bool constraint_isConstantOnly (constraint c) +static bool +constraint_isConstantOnly (constraint c) { bool l, r; diff --git a/src/constraintExpr.c b/src/constraintExpr.c index 8fcef4b..04c2313 100644 --- a/src/constraintExpr.c +++ b/src/constraintExpr.c @@ -34,9 +34,6 @@ # include "basic.h" # include "cgrammar.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - static ctype constraintExpr_getOrigType (constraintExpr p_e); static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/; @@ -569,10 +566,12 @@ constraintExpr constraintExpr_makeExprNode (exprNode e) -/*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e) +#if 0 +static /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e) { return oldconstraintExpr_makeTermExprNode(e); } +#endif static constraintExpr constraintExpr_makeTerm (/*@only@*/ constraintTerm t) { @@ -1606,6 +1605,7 @@ cstring constraintExpr_unparse (/*@temp@*/ constraintExpr ex) /*@*/ return st; } +# ifdef DEADCODE constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr expr, exprNodeList arglist) { constraintTerm Term; @@ -1653,6 +1653,7 @@ constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr } return expr; } +# endif /* DEADCODE */ #if 0 /*@only@*/ constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct) @@ -1774,7 +1775,6 @@ constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr data = constraintExprData_binaryExprSetExpr1 (data, expr1); expr2 = constraintExpr_doFixResult (expr2, fcnCall); data = constraintExprData_binaryExprSetExpr2 (data, expr2); - break; default: llassert(FALSE); @@ -1841,8 +1841,8 @@ long constraintExpr_getValue (constraintExpr expr) bool constraintExpr_canGetValue (constraintExpr expr) { - llassert ( constraintExpr_isDefined (expr) ); - if (constraintExpr_isUndefined (expr) ) + llassert ( constraintExpr_isDefined (expr)); + if (constraintExpr_isUndefined (expr)) { return FALSE; } @@ -1853,10 +1853,7 @@ bool constraintExpr_canGetValue (constraintExpr expr) return constraintTerm_canGetValue (constraintExprData_termGetTerm (expr->data) ); default: return FALSE; - } - - BADEXIT; } fileloc constraintExpr_loc (constraintExpr expr) @@ -1930,13 +1927,9 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall) { ret = constraintExpr_makeExprNode(fcnCall); constraintExpr_free(e); - e = NULL; - } - else - { - e = NULL; } break; + default: BADEXIT; } @@ -2339,16 +2332,11 @@ int constraintExpr_getDepth (constraintExpr ex) case unaryExpr: ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) ); ret++; - break; case binaryexpr: - ret = 0; ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) ); - ret++; - ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) ); - break; default: BADEXIT; diff --git a/src/constraintExprData.c b/src/constraintExprData.c index dadd29d..b31e0c0 100644 --- a/src/constraintExprData.c +++ b/src/constraintExprData.c @@ -29,9 +29,6 @@ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - static /*@out@*/ constraintExprData constraintExprData_alloc (void) { constraintExprData ret; diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 251086e..a2aae6e 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -28,15 +28,11 @@ /* #define DEBUGPRINT 1 */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - /*drl We need to access the internal representation of exprNode because these functions walk down the parse tree and need a richer information than is accessible through the exprNode interface.*/ @@ -55,6 +51,15 @@ static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist); +static void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, + /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint); +static /*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode p_e); +static constraintList exprNode_getPostConditions ( + /*@dependent@*/ /*@observer@*/ exprNode p_fcn, exprNodeList p_arglist, + /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall) /*@*/; +static /*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode p_e); + + static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e) { llassert(exprNode_isDefined(e)); @@ -106,15 +111,15 @@ static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e) } /* evans 2002-03-2 - parameter was dependent */ -bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) +void exprNode_generateConstraints (/*@temp@*/ exprNode e) { if (exprNode_isError (e)) - return FALSE; + return; if (exprNode_isUnhandled (e)) { DPRINTF((message("Warning ignoring %s", exprNode_unparse (e)))); - return FALSE; + return; } DPRINTF ((message ("exprNode_generateConstraints Analyzing %s at %s", exprNode_unparse(e), @@ -134,7 +139,7 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) /* fileloc_free(loc); */ exprNode_stmt(e); - return FALSE; + return; } @@ -148,7 +153,7 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) DPRINTF ((message ("e->requiresConstraints %s", constraintList_unparseDetailed (e->requiresConstraints)))); - return FALSE; + return; } static void exprNode_stmt (/*@temp@*/ exprNode e) @@ -1169,7 +1174,7 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b } } -void exprNode_exprTraverse (/*@dependent@*/ exprNode e, +static void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint) { @@ -1848,7 +1853,7 @@ constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e) /* walk down the tree and get all requires Constraints in each subexpression*/ -/*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e) +static /*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e) { exprNode t1; exprData data; @@ -1980,7 +1985,7 @@ constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e) /* walk down the tree and get all Ensures Constraints in each subexpression*/ -/*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e) +static /*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e) { exprNode t1; exprData data; @@ -2150,7 +2155,7 @@ void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, } /*drl moved out of constraintResolve.c 07-03-001 */ -constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) +static constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) { constraintList postconditions; uentry temp; diff --git a/src/constraintList.c b/src/constraintList.c index 9482b0d..96e96c6 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -554,6 +554,8 @@ Commenting out because function is not yet stable return ret; } + +# ifdef DEADCODE constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/ exprNodeList arglist) { @@ -570,6 +572,7 @@ constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, return ret; } +# endif /* DEADCODE */ constraintList constraintList_togglePost (/*@returned@*/ constraintList c) { diff --git a/src/constraintResolve.c b/src/constraintResolve.c index c5c2105..528cecb 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -29,13 +29,9 @@ /* #define DEBUGPRINT 1 */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - /*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */ static constraint inequalitySubstitute (/*@returned@*/ constraint p_c, constraintList p_p); @@ -52,6 +48,13 @@ static bool resolveOr (/*@temp@*/constraint p_c, /*@observer@*/ /*@temp@*/ const static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList p_pre2, constraintList p_post1); +static /*@only@*/ constraintList constraintList_subsumeEnsures (constraintList p_list1, constraintList p_list2); +static /*@only@*/ constraintList constraintList_fixConflicts (constraintList p_list1, constraintList p_list2); + +static bool fileloc_closer (/*@observer@*/ fileloc p_loc1, + /*@observer@*/ fileloc p_loc2, + /*@observer@*/ fileloc p_loc3) /*@*/; + /*@only@*/ constraintList constraintList_mergeEnsuresFreeFirst (constraintList list1, constraintList list2) { @@ -219,7 +222,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) } -/*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2) +static /*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2) { constraintList ret; ret = constraintList_makeNew(); @@ -720,7 +723,7 @@ static bool conflict (constraint c, constraintList list) remove form list1 and change list2. */ -constraintList constraintList_fixConflicts (constraintList list1, constraintList list2) +static constraintList constraintList_fixConflicts (constraintList list1, constraintList list2) { constraintList ret; ret = constraintList_makeNew(); @@ -1258,7 +1261,7 @@ constraint inequalitySubstitute (/*@returned@*/ constraint c, constraintList p llassert(constraint_isDefined(el) ); - if ((el->ar == LT ) ) + if (el->ar == LT) { constraintExpr temp2; @@ -1329,7 +1332,7 @@ static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, con )); temp2 = constraintExpr_copy (el->expr); constraintExpr_free(c->expr); - if ((el->ar == LTE ) ) + if (el->ar == LTE) { c->expr = temp2; } @@ -1428,20 +1431,10 @@ static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, co } -/*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList target, /*@observer@*/ constraintList subList) -{ -constraintList ret; - -ret = constraintList_substitute (target, subList); - -constraintList_free(target); - -return ret; -} - /* we try to do substitutions on each constraint in target using the constraint in sublist*/ -/*@only@*/ constraintList constraintList_substitute (constraintList target,/*2observer@*/ constraintList subList) +static /*@only@*/ constraintList +constraintList_substitute (constraintList target,/*2observer@*/ constraintList subList) { constraintList ret; @@ -1461,6 +1454,15 @@ return ret; return ret; } +/*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList target, /*@observer@*/ constraintList subList) +{ + constraintList ret; + ret = constraintList_substitute (target, subList); + constraintList_free(target); + + return ret; +} + static constraint constraint_solve (/*@returned@*/ constraint c) { @@ -1551,7 +1553,7 @@ constraint constraint_simplify ( /*@returned@*/ constraint c) /* returns true if fileloc for term1 is closer to file for term2 than term3*/ -bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3) +static bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3) { if (!fileloc_isDefined (loc1) ) diff --git a/src/constraintTerm.c b/src/constraintTerm.c index c5ff79e..49315fd 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -28,13 +28,9 @@ /* #define DEBUGPRINT 1 */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - bool constraintTerm_isDefined (constraintTerm t) { return t != NULL; @@ -263,6 +259,7 @@ constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fi } +# ifdef DEADCODE static cstring constraintTerm_getName (constraintTerm term) { cstring s; @@ -315,6 +312,7 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi return term; } +# endif /* DEADCODE */ cstring constraintTerm_unparse (constraintTerm term) /*@*/ { @@ -458,6 +456,7 @@ long constraintTerm_getValue (constraintTerm term) return sRef_undefined; } +# ifdef DEADCODE bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) { cstring s1, s2; @@ -484,6 +483,7 @@ bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) return FALSE; } } +# endif /* DEADCODE */ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) { diff --git a/src/context.c b/src/context.c index 97a7262..55975e6 100644 --- a/src/context.c +++ b/src/context.c @@ -28,10 +28,8 @@ # include "splintMacros.nf" # include "basic.h" -# include "usymtab_interface.h" # include "exprChecks.h" # include "filelocStack.h" -# include "llmain.h" # include "intSet.h" # include "osd.h" @@ -174,10 +172,12 @@ static void context_restoreFlag (flagcode p_f, fileloc p_loc) /*@+enumindex@*/ +# ifdef DEADCODE cstring context_unparseFlagMarkers (void) { return (flagMarkerList_unparse (gc.markers)); } +# endif /* DEADCODE */ void context_setPreprocessing (void) { @@ -541,7 +541,6 @@ context_exitLCLfile (void) cstring_free (lclname); } - gc.kind = CX_LCL; gc.kind = CX_GLOBAL; gc.facct = typeIdSet_emptySet (); } @@ -1493,11 +1492,12 @@ void context_exitFunctionDeclaration (void) } } +# ifdef DEADCODE bool context_inFunctionDeclaration (void) { return (gc.kind == CX_FCNDECLARATION); } - +# endif /* DEADCODE */ void context_enterMacro (/*@observer@*/ uentry e) @@ -2114,7 +2114,7 @@ context_hasFileAccess (typeId t) return (typeIdSet_member (gc.facct, t)); } -/*@only@*/ cstring +static /*@only@*/ cstring context_unparseAccess (void) { return (message ("%q / %q", typeIdSet_unparse (gc.acct), @@ -2799,6 +2799,7 @@ context_getValue (flagcode flag) return (gc.values[index]); } +# ifdef DEADCODE int context_getCounter (flagcode flag) { @@ -2826,6 +2827,7 @@ context_decCounter (flagcode flag) llassert (index >= 0 && index <= NUMVALUEFLAGS); gc.counters[index]--; } +# endif /* DEADCODE */ bool context_showFunction (void) { @@ -4469,6 +4471,7 @@ bool context_inProtectVars (void) return (gc.protectVars); } +# ifdef DEADCODE void context_hideShowscan (void) { gc.flags[FLG_SHOWSCAN] = FALSE; @@ -4478,6 +4481,7 @@ void context_unhideShowscan (void) { gc.flags[FLG_SHOWSCAN] = TRUE; } +# endif /* DEADCODE */ bool context_inHeader (void) { @@ -4734,6 +4738,7 @@ bool context_isMacroMissingParams (void) return (gc.macroMissingParams); } +# ifdef DEADCODE void context_showFilelocStack (void) { filelocStack_printIncludes (gc.locstack); @@ -4743,6 +4748,7 @@ metaStateTable context_getMetaStateTable (void) { return gc.stateTable; } +# endif /* DEADCODE */ metaStateInfo context_lookupMetaStateInfo (cstring key) { diff --git a/src/cpperror.c b/src/cpperror.c index 2a4945b..69f4559 100644 --- a/src/cpperror.c +++ b/src/cpperror.c @@ -81,8 +81,6 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # include # include -# define FATAL_EXIT_CODE EXIT_FAILURE - # include "splintMacros.nf" # include "basic.h" # include "cpplib.h" @@ -124,8 +122,7 @@ static void cppReader_printContainingFiles (cppReader *pfile) } /* Find the other, outer source files. */ - while ((ip = cppBuffer_prevBuffer (ip)), - ip != cppReader_nullBuffer (pfile)) + while ((ip = cppBuffer_prevBuffer (ip)) != cppReader_nullBuffer (pfile)) { int line, col; cstring temps; @@ -222,12 +219,14 @@ cppReader_fatalError (cppReader *pfile, /*@only@*/ cstring str) cppReader_message (pfile, 2, str); } +# ifdef DEADCODE void cppReader_pfatalWithName (cppReader *pfile, cstring name) { cppReader_perrorWithName (pfile, name); exit (FATAL_EXIT_CODE); } +# endif /* DEADCODE */ static /*@only@*/ fileloc cppReader_getLoc (cppReader *pfile) diff --git a/src/cppexp.c b/src/cppexp.c index 4ac6c7e..7ba3aa7 100644 --- a/src/cppexp.c +++ b/src/cppexp.c @@ -144,7 +144,7 @@ struct operation { /* maybe needs to actually deal with floating point numbers */ -struct operation +static struct operation cppReader_parseNumber (cppReader *pfile, char *start, int olen) /*@requires maxRead(start) >= (olen - 1) @*/ { struct operation op; @@ -809,7 +809,8 @@ cppReader_parseExpression (cppReader *pfile) switch (op.op) { case NAME: - top->value = 0, top->unsignedp = FALSE; + top->value = 0; + top->unsignedp = FALSE; goto set_value; case CPPEXP_INT: case CPPEXP_CHAR: diff --git a/src/cpphash.c b/src/cpphash.c index b2d446f..f575fbd 100644 --- a/src/cpphash.c +++ b/src/cpphash.c @@ -53,7 +53,6 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # include "splintMacros.nf" # include "basic.h" -# include # include "cpplib.h" # include "cpphash.h" diff --git a/src/cpplib.c b/src/cpplib.c index 9d186d1..6b442a7 100644 --- a/src/cpplib.c +++ b/src/cpplib.c @@ -48,22 +48,18 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. You are forbidden to forbid anyone else to use, share and improve what you give them. Help stamp out software-hoarding! */ -# include -# include -# include -# include # include # include # include "splintMacros.nf" # include "basic.h" + # include "lcllib.h" # include "cppconf.h" # include "cpplib.h" # include "cpperror.h" # include "cpphash.h" # include "cppexp.h" -# include "version.h" # include "osd.h" /* @@ -105,7 +101,10 @@ static enum cpp_token cpp_handleComment (cppReader *p_pfile, static bool cpp_shouldCheckMacro (cppReader *p_pfile, char *p_p) /*@modifies p_p@*/ ; +static size_t cppReader_checkMacroName (cppReader *p_pfile, char *p_symname, cstring p_usage); +#if 0 static size_t cppReader_checkMacroNameLoc (fileloc p_loc, char *p_symname, cstring p_usage) ; +#endif static bool cpp_skipIncludeFile (cstring p_fname) /*@*/ ; @@ -178,6 +177,17 @@ cppReader_getBuffer (/*@special@*/ cppReader *p_pfile) static int cpp_peekN (cppReader *p_pfile, int p_n) /*@*/ ; +static void cppReader_growBuffer (cppReader *, size_t); + +/* Make sure PFILE->token_buffer has space for at least N more characters. */ + +/*@function static void cpplib_reserve (sef cppReader *, sef/ size_t); @*/ +#define cpplib_reserve(PFILE, N) \ + do { \ + if ((cpplib_getWritten (PFILE) + (N) > (PFILE)->token_buffer_size)) \ + cppReader_growBuffer (PFILE, (N)); \ + } while (0) + /*@function static int cppBuffer_get (sef cppBuffer *p_b) modifies *p_b ; @*/ # define cppBuffer_get(BUFFER) \ ((BUFFER)->cur < (BUFFER)->rlimit ? *(BUFFER)->cur++ : EOF) @@ -186,12 +196,20 @@ static int cpp_peekN (cppReader *p_pfile, int p_n) /*@*/ ; # define cppBuffer_reachedEOF(b) \ ((b)->cur < (b)->rlimit ? FALSE : TRUE) +/* Append string STR (of length N) to PFILE's output buffer. Assume there is enough space. */ + +/*@ function static void cppReader_putStrN (sef cppReader *p_file, @unique@ char *p_str, + sef size_t p_n) modifies *p_file; @*/ +#define cppReader_putStrN(PFILE, STR, N) \ + do { memcpy ((PFILE)->limit, STR, (N)); (PFILE)->limit += (N); } while (0) + /* Append string STR (of length N) to PFILE's output buffer. Make space. */ + /*@function static void cppReader_puts (sef cppReader *p_file, char *p_str, sef size_t p_n) modifies *p_file; @*/ # define cppReader_puts(PFILE, STR, N) \ - cpplib_reserve(PFILE, N), cppReader_putStrN (PFILE, STR,N) - + do { cpplib_reserve(PFILE, N); cppReader_putStrN (PFILE, STR,N); } while (0) + /* Append character CH to PFILE's output buffer. Assume sufficient space. */ /*@function static void cppReader_putCharQ (cppReader *p_file, char p_ch) @@ -204,11 +222,13 @@ static void cppReader_putCharQ (cppReader *p_file, char p_ch) (*(p_file)->limit++ = (p_ch)); } */ + /* Append character CH to PFILE's output buffer. Make space if need be. */ /*@function static void cppReader_putChar (sef cppReader *p_file, char p_ch) modifies *p_file; @*/ -#define cppReader_putChar(PFILE, CH) (cpplib_reserve (PFILE, (size_t) 1), cppReader_putCharQ (PFILE, CH)) +#define cppReader_putChar(PFILE, CH) \ + do { cpplib_reserve (PFILE, (size_t) 1); cppReader_putCharQ (PFILE, CH); } while (0) /* Make sure PFILE->limit is followed by '\0'. */ /*@function static void cppReader_nullTerminateQ (cppReader *p_file) @@ -219,7 +239,7 @@ static void cppReader_putCharQ (cppReader *p_file, char p_ch) /*@function static void cppReader_nullTerminate (sef cppReader *p_file) modifies *p_file; @*/ # define cppReader_nullTerminate(PFILE) \ - (cpplib_reserve (PFILE, (size_t) 1), *(PFILE)->limit = 0) + do { cpplib_reserve (PFILE, (size_t) 1); *(PFILE)->limit = 0; } while (0) /*@function static void cppReader_adjustWritten (cppReader *p_file, size_t) modifies *p_file; @*/ @@ -527,7 +547,7 @@ quote_string (cppReader *pfile, char *src) /* Re-allocates PFILE->token_buffer so it will hold at least N more chars. */ -void +static void cppReader_growBuffer (cppReader *pfile, size_t n) { size_t old_written = cpplib_getWritten (pfile); @@ -636,7 +656,7 @@ cppReader_defineReal (cppReader *pfile, char *str) sfree (buf); } -void +static void cppReader_define (cppReader *pfile, char *str) { cppBuffer *tbuf = CPPBUFFER (pfile); @@ -812,8 +832,8 @@ cppReader_appendPathListIncludeChain (cppReader *pfile, cppReader_appendIncludeChain (pfile, first, last, system); } -void -cppOptions_init (cppOptions *opts) +static void +cppOptions_init (/*@out@*/ cppOptions *opts) { memset ((char *) opts, 0, sizeof *opts); assertSet (opts); @@ -1700,6 +1720,7 @@ collect_expansion (cppReader *pfile, char *buf, char *limit, return defn; /* Spurious warning here */ } +# if 0 /* FIXME */ /* ** evans 2001-12-31 @@ -2048,6 +2069,7 @@ collect_expansionLoc (fileloc loc, char *buf, char *limit, return defn; /*@=compdef@*/ } +# endif /* * special extension string that can be added to the last macro argument to @@ -2286,6 +2308,7 @@ nope: return mdef; } +# if 0 /*@null@*/ macroDef cpplib_createDefinition (cstring def, fileloc loc, @@ -2508,11 +2531,12 @@ nope: mdef.symnam = NULL; return mdef; } +# endif /* Check a purported macro name SYMNAME, and yield its length. USAGE is the kind of name this is intended for. */ -size_t cppReader_checkMacroName (cppReader *pfile, char *symname, cstring usage) +static size_t cppReader_checkMacroName (cppReader *pfile, char *symname, cstring usage) { char *p; size_t sym_length; @@ -2549,6 +2573,7 @@ size_t cppReader_checkMacroName (cppReader *pfile, char *symname, cstring usage) return sym_length; } +# if 0 /* FIXME */ /* ** evans 2001-12-31 @@ -2593,6 +2618,7 @@ size_t cppReader_checkMacroNameLoc (fileloc loc, char *symname, cstring usage) return sym_length; } +# endif /* Return zero if two DEFINITIONs are isomorphic. */ @@ -6761,8 +6787,8 @@ finclude (cppReader *pfile, int f, return 1; } -void -cpplib_init (cppReader *pfile) +static void +cpplib_init (/*@out@*/ cppReader *pfile) { memset ((char *) pfile, 0, sizeof (*pfile)); @@ -7163,7 +7189,6 @@ static bool expectiter = FALSE; /* preceeded by @iter@ */ static bool expectenditer = FALSE; /* second after @iter@ */ static bool expectfunction = FALSE; /* preceeded by @function@ */ static bool expectconstant = FALSE; /* preceeded by @constant@ */ -static bool expectmacro = FALSE; /* preceeded by notfunction or notparseable */ static void cpp_setLocation (cppReader *pfile) { @@ -7567,13 +7592,11 @@ cpp_handleComment (cppReader *pfile, struct parse_marker *smark) else if (mstring_equalPrefix (scomment, "notparseable")) { notparseable = TRUE; - expectmacro = TRUE; eliminateComment = TRUE; } else if (mstring_equalPrefix (scomment, "notfunction")) { notfunction = TRUE; - expectmacro = TRUE; eliminateComment = TRUE; } else if (mstring_equalPrefix (scomment, "iter")) diff --git a/src/cppmain.c b/src/cppmain.c index 3164c20..5044f82 100644 --- a/src/cppmain.c +++ b/src/cppmain.c @@ -50,11 +50,8 @@ Foundation, 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. # include "basic.h" # include "cpplib.h" # include "cpphash.h" -# include "cpperror.h" +# include "cpp.h" # include "llmain.h" -# include "osd.h" - -# include /* char *progname; */ diff --git a/src/cscannerHelp.c b/src/cscannerHelp.c index 073a25c..136ff30 100644 --- a/src/cscannerHelp.c +++ b/src/cscannerHelp.c @@ -43,7 +43,6 @@ static bool s_inSpecPart = FALSE; static int s_whichSpecPart; static char s_savechar = '\0'; static bool s_expectingMetaStateName = FALSE; -static bool s_lastWasString = FALSE; static bool s_expectingTypeName = TRUE; struct skeyword @@ -168,6 +167,9 @@ static struct skeyword s_keytable[] = { { NULL, BADTOK } } ; +static bool cscannerHelp_isConstraintToken (int p_tok) /*@*/ ; +static void cscannerHelp_advanceLine (void) /*@modifies g_currentloc, internalState@*/ ; + /* ** would be better if these weren't hard coded... */ @@ -657,11 +659,8 @@ bool cscannerHelp_handleSpecial (char *text) l = mstring_append(l, c); } - /* Need to safe original l for deallocating. */ ol = l; - l += strlen (l); - olc = cstring_fromChars (ol); if (cstring_equalPrefixLit (olc, "pragma")) @@ -1530,7 +1529,9 @@ static void cscanner_setLastIdentifier (/*@keep@*/ cstring id) /*@modifies s_las s_lastidprocessed = id; } -int cscannerHelp_processIdentifier (cstring id) +static int +cscannerHelp_processIdentifier (/*@only@*/ cstring id) + /*@modifies internalState@*/ { uentry le; @@ -1645,7 +1646,6 @@ int cscannerHelp_processIdentifier (cstring id) /* evans 2001-12-30: changed from exprNode_stringLiteral; bug reported by Jim Zelenka. */ c_lval.expr = exprNode_makeConstantString (id, fileloc_copy (g_currentloc)); s_tokLength = 0; - s_lastWasString = TRUE; tok = CCONSTANT; return tok; } @@ -2140,7 +2140,7 @@ void cscannerHelp_clearExpectingMetaStateName (void) s_expectingMetaStateName = FALSE; } -bool cscannerHelp_isConstraintToken (int tok) +static bool cscannerHelp_isConstraintToken (int tok) /* drl added 12/11/2002 Tell whether a token has special meaning within a function constraint @@ -2673,7 +2673,7 @@ void cscannerHelp_setTokLengthT (size_t len) cscannerHelp_setTokLength (size_toInt (len)); } -void cscannerHelp_advanceLine (void) +static void cscannerHelp_advanceLine (void) { s_tokLength = 0; beginLine (); @@ -2688,7 +2688,6 @@ int cscannerHelp_returnToken (int t) } s_tokLength = 0; - s_lastWasString = FALSE; return (t); } @@ -2702,7 +2701,6 @@ int cscannerHelp_returnString (cstring s) { c_lval.expr = exprNode_stringLiteral (s, fileloc_decColumn (g_currentloc, s_tokLength)); s_tokLength = 0; - s_lastWasString = TRUE; return (CCONSTANT); } @@ -2730,7 +2728,6 @@ int cscannerHelp_returnInt (ctype ct, long val) fileloc_decColumn (g_currentloc, s_tokLength), val); s_tokLength = 0; - s_lastWasString = FALSE; return (CCONSTANT); } @@ -2739,7 +2736,6 @@ int cscannerHelp_returnFloat (ctype ct, double f) c_lval.expr = exprNode_floatLiteral (f, ct, cstring_fromChars (c_text), fileloc_decColumn (g_currentloc, s_tokLength)); s_tokLength = 0; - s_lastWasString = FALSE; return (CCONSTANT); } @@ -2748,7 +2744,6 @@ int cscannerHelp_returnChar (char c) c_lval.expr = exprNode_charLiteral (c, cstring_fromChars (c_text), fileloc_decColumn (g_currentloc, s_tokLength)); s_tokLength = 0; - s_lastWasString = FALSE; return (CCONSTANT); } @@ -2756,7 +2751,6 @@ int cscannerHelp_returnType (int tok, ctype ct) { c_lval.ctyp = ct; s_tokLength = 0; - s_lastWasString = FALSE; return tok; } @@ -2764,7 +2758,6 @@ int cscannerHelp_returnExpr (exprNode e) { c_lval.expr = e; s_tokLength = 0; - s_lastWasString = TRUE; return (CCONSTANT); } @@ -2778,10 +2771,12 @@ void cscannerHelp_clearExpectingTypeName (void) s_expectingTypeName = FALSE; } +# ifdef DEADCODE bool cscannerHelp_isExpectingTypeName (void) { return s_expectingTypeName; } +# endif /* DEADCODE */ int cscannerHelp_processTextIdentifier (char *text) { @@ -2817,7 +2812,6 @@ int cscannerHelp_handleNewLine (void) /* Don't use return cscannerHelp_returnToken */ /* !!! evans 2002-03-13 */ c_lval.tok = lltok_create (TENDMACRO, fileloc_copy (g_currentloc)); - s_lastWasString = FALSE; return TENDMACRO; } } diff --git a/src/cstring.c b/src/cstring.c index 03befe5..7098ab1 100644 --- a/src/cstring.c +++ b/src/cstring.c @@ -27,7 +27,6 @@ # include "splintMacros.nf" # include "basic.h" -# include "osd.h" /*@only@*/ /*@notnull@*/ cstring cstring_newEmpty (void) @@ -204,10 +203,10 @@ void cstring_replaceAll (cstring s, char old, char snew) sp = strchr (sp, old); } - } + } } -void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) +void cstring_replaceLit (/*@unique@*/ cstring s, const char *old, const char *snew) /*@requires maxRead(snew) >= 0 /\ maxRead(old) >= 0 /\ maxRead(old) >= maxRead(snew) @*/ { llassert (strlen (old) >= strlen (snew)); @@ -219,7 +218,7 @@ void cstring_replaceLit (/*@unique@*/ cstring s, char *old, char *snew) while (sp != NULL) { int lendiff = size_toInt (strlen (old) - strlen (snew)); - char *tsnew = snew; + const char *tsnew = snew; llassert (lendiff >= 0); @@ -781,6 +780,7 @@ cstring_prependChar (char c, /*@temp@*/ cstring s1) return s; } +# ifdef DEADCODE bool cstring_hasNonAlphaNumBar (cstring s) { @@ -800,6 +800,7 @@ cstring_hasNonAlphaNumBar (cstring s) } return FALSE; } +# endif /* DEADCODE */ /*@only@*/ /*@notnull@*/ cstring cstring_create (size_t n) @@ -830,15 +831,17 @@ lsymbol cstring_toSymbol (cstring s) return res; } -cstring cstring_bsearch (cstring key, char **table, int nentries) +bool cstring_bsearch (cstring key, const char **table, int nentries) { + bool res = FALSE; + if (cstring_isDefined (key)) { int low = 0; int high = nentries; int mid = (high + low + 1) / 2; int last = -1; - cstring res = cstring_undefined; + const char * ckey = cstring_toCharsSafe (key); while (low <= high && mid < nentries) { @@ -847,11 +850,11 @@ cstring cstring_bsearch (cstring key, char **table, int nentries) llassert (mid != last); llassert (mid >= 0 && mid < nentries); - cmp = cstring_compare (key, table[mid]); + cmp = strcmp (ckey, table[mid]); if (cmp == 0) { - res = table[mid]; + res = TRUE; break; } else if (cmp < 0) /* key is before table[mid] */ @@ -866,17 +869,9 @@ cstring cstring_bsearch (cstring key, char **table, int nentries) last = mid; mid = (high + low + 1) / 2; } - - if (mid != 0 && mid < nentries - 1) - { - llassert (cstring_compare (key, table[mid - 1]) > 0); - llassert (cstring_compare (key, table[mid + 1]) < 0); - } - - return res; } - return cstring_undefined; + return res; } extern /*@observer@*/ cstring cstring_advanceWhiteSpace (cstring s) diff --git a/src/cstringList.c b/src/cstringList.c index 490175f..82748fd 100644 --- a/src/cstringList.c +++ b/src/cstringList.c @@ -173,6 +173,7 @@ cstringList_unparseSep (cstringList s, cstring sep) return st; } +# ifdef DEADCODE void cstringList_printSpaced (cstringList s, size_t indent, size_t gap, int linelen) { @@ -260,6 +261,7 @@ cstringList_unparseAbbrev (cstringList s) return st; } +# endif /* DEADCODE */ void cstringList_free (cstringList s) @@ -282,6 +284,7 @@ cstringList_free (cstringList s) } } +# ifdef DEADCODE void cstringList_alphabetize (cstringList s) { @@ -293,6 +296,7 @@ cstringList_alphabetize (cstringList s) /*@=modobserver@*/ } } +# endif /* DEADCODE */ int cstringList_getIndex (cstringList s, cstring key) { diff --git a/src/cstringSList.c b/src/cstringSList.c index a6dbc47..f431a1b 100644 --- a/src/cstringSList.c +++ b/src/cstringSList.c @@ -76,12 +76,14 @@ cstringSList_grow (/*@notnull@*/ cstringSList s) s->elements = newelements; } +# ifdef DEADCODE cstringSList cstringSList_single (/*@exposed@*/ cstring el) { cstringSList s = cstringSList_new (); s = cstringSList_add (s, el); return s; } +# endif /* DEADCODE */ cstringSList cstringSList_add (cstringSList s, /*@exposed@*/ cstring el) { @@ -102,6 +104,7 @@ cstringSList cstringSList_add (cstringSList s, /*@exposed@*/ cstring el) return s; } +# ifdef DEADCODE cstring cstringSList_get (cstringSList s, int index) { @@ -109,14 +112,9 @@ cstringSList_get (cstringSList s, int index) llassert (index < s->nelements); return s->elements[index]; } +# endif /* DEADCODE */ -cstring -cstringSList_unparse (cstringSList s) -{ - return cstringSList_unparseSep (s, cstring_makeLiteralTemp (", ")); -} - -cstring +static cstring cstringSList_unparseSep (cstringSList s, cstring sep) { cstring st = cstring_undefined; @@ -139,6 +137,12 @@ cstringSList_unparseSep (cstringSList s, cstring sep) return st; } +cstring +cstringSList_unparse (cstringSList s) +{ + return cstringSList_unparseSep (s, cstring_makeLiteralTemp (", ")); +} + void cstringSList_printSpaced (cstringSList s, size_t indent, size_t gap, int linelen) { diff --git a/src/cstringTable.c b/src/cstringTable.c index 885d8d5..2c9b83a 100644 --- a/src/cstringTable.c +++ b/src/cstringTable.c @@ -65,6 +65,7 @@ static void hentry_free (/*@only@*/ hentry h) sfree (h); } +# ifdef DEADCODE static bool hbucket_isEmpty (hbucket h) { @@ -88,6 +89,7 @@ hbucket_unparse (hbucket h) return s; } +# endif /* DEADCODE */ static hbucket hbucket_single (/*@only@*/ hentry e) @@ -152,6 +154,7 @@ hbucket_add (/*@notnull@*/ hbucket h, /*@only@*/ hentry e) h->nspace--; } +# ifdef DEADCODE static int hbucket_ncollisions (hbucket h) { @@ -160,6 +163,7 @@ hbucket_ncollisions (hbucket h) else return 0; } +# endif /* DEADCODE */ int hbucket_lookup (hbucket h, cstring key) @@ -213,6 +217,7 @@ cstringTable_free (/*@only@*/ cstringTable h) sfree (h); } +# ifdef DEADCODE static int cstringTable_countCollisions (cstringTable h) { @@ -248,6 +253,7 @@ cstringTable_countEmpty (cstringTable h) return (nc); } +# endif /* DEADCODE */ static unsigned int cstringTable_hashValue (/*@notnull@*/ cstringTable h, cstring key) @@ -281,6 +287,7 @@ cstringTable_create (unsigned long size) return h; } +# ifdef DEADCODE cstring cstringTable_unparse (cstringTable h) { cstring res = cstring_newEmpty (); @@ -322,6 +329,7 @@ cstringTable_stats (cstringTable h) h->size, cstringTable_countCollisions (h), cstringTable_countEmpty (h))); } +# endif /* DEADCODE */ static void cstringTable_rehash (/*@notnull@*/ cstringTable h) @@ -450,6 +458,7 @@ cstringTable_lookup (cstringTable h, cstring key) return (hbucket_lookup (hb, key)); } +# ifdef DEADCODE void cstringTable_update (cstringTable h, cstring key, int newval) { @@ -475,6 +484,7 @@ cstringTable_update (cstringTable h, cstring key, int newval) llbug (message ("cstringTable_update: %s not found", key)); } +# endif /* DEADCODE */ /* ** This is needed if oldkey is going to be released. diff --git a/src/ctbase.i b/src/ctbase.i index 4b1df5b..45bb594 100644 --- a/src/ctbase.i +++ b/src/ctbase.i @@ -144,7 +144,7 @@ static ctype ctbase_newBaseExpFcn (ctype p_c, ctype p_p) /*@*/ ; static bool ctbase_isFixedArray (/*@notnull@*/ ctbase p_c) /*@*/ ; /*@-macroundef@*/ -extern int cttable_lastIndex(); +extern int cttable_lastIndex(void); # define cttable_lastIndex() (cttab.size - 1) /*@=macroundef@*/ @@ -300,12 +300,14 @@ static int nctbases = 0; static /*@notnull@*/ /*@only@*/ ctbase ctbase_makeLiveFunction (ctype p_b, /*@only@*/ uentryList p_p); +# ifdef DEADCODE static bool ctbase_isUnnamedSU (ctbase c) { return (ctbase_isDefined (c) && (ctbase_isStruct (c) || ctbase_isUnion (c)) && isFakeTag (c->contents.su->name)); } +# endif /* DEADCODE */ static /*@observer@*/ ctbase ctbase_realType (ctbase c) { @@ -2658,7 +2660,7 @@ ctbase_almostEqual (ctbase c1, ctbase c2) called by ctype_getArraySize */ -size_t ctbase_getArraySize (ctbase ctb) +static size_t ctbase_getArraySize (ctbase ctb) { /*drl 1/25/2002 fixed discovered by Jim Francis */ ctbase r; @@ -2670,7 +2672,7 @@ size_t ctbase_getArraySize (ctbase ctb) return (r->contents.farray->size); } -bool ctbase_isBigger (ctbase ct1, ctbase ct2) +static bool ctbase_isBigger (ctbase ct1, ctbase ct2) { if (ct1 != NULL && ct2 != NULL && (ct1->type == CT_PRIM && ct2->type == CT_PRIM)) @@ -2693,7 +2695,7 @@ bool ctbase_isBigger (ctbase ct1, ctbase ct2) } } -int ctbase_getSize (ctbase ct) +static int ctbase_getSize (ctbase ct) { if (ct == NULL) { @@ -2737,7 +2739,7 @@ int ctbase_getSize (ctbase ct) case CT_ENUM: case CT_CONJ: break; - BADDEFAULT; + BADDEFAULT; } return 0; diff --git a/src/cttable.i b/src/cttable.i index 18ec2cc..4aec98b 100644 --- a/src/cttable.i +++ b/src/cttable.i @@ -272,6 +272,7 @@ cttable_unparse (void) return (s); } +#if 0 void cttable_print (void) { @@ -303,6 +304,7 @@ cttable_print (void) } /*@noaccess ctbase@*/ } +#endif /* ** cttable_dump diff --git a/src/ctype.c b/src/ctype.c index 3553963..c9b7481 100644 --- a/src/ctype.c +++ b/src/ctype.c @@ -33,6 +33,7 @@ # include "structNames.h" static void ctype_recordConj (ctype p_c); +static ctkind ctkind_fromInt (int p_i); /* @@ -76,7 +77,7 @@ static bool ctype_isBroken (ctype c) } } -ctkind +static ctkind ctkind_fromInt (int i) { /*@+enumint@*/ @@ -125,11 +126,13 @@ ctype_unparseTable (void) return (cttable_unparse ()); } +# if 0 void ctype_printTable (void) { cttable_print (); } +# endif bool ctype_isUserBool (ctype ct) @@ -171,11 +174,13 @@ ctype_createNumAbstract (typeId u) (ctentry_makeNew (CTK_PLAIN, ctbase_createNumAbstract (u)))); } +# ifdef DEADCODE int ctype_count (void) { return (cttab.size); } +# endif /* DEADCODE */ ctype ctype_realType (ctype c) @@ -1928,6 +1933,7 @@ ctype_unparse (ctype c) } } +# ifdef DEADCODE cstring ctype_unparseSafe (ctype c) { @@ -1958,6 +1964,7 @@ ctype_unparseSafe (ctype c) return ret; } } +# endif /* DEADCODE */ cstring ctype_unparseDeep (ctype c) @@ -2249,6 +2256,7 @@ ctype_createUnnamedUnion (/*@only@*/ uentryList f) } } +# ifdef DEADCODE bool ctype_isUnnamedSU (ctype c) { @@ -2261,6 +2269,7 @@ ctype_isUnnamedSU (ctype c) return FALSE; } } +# endif /* DEADCODE */ ctype ctype_createForwardStruct (cstring n) diff --git a/src/ctypeList.c b/src/ctypeList.c index 0572338..1987c0f 100644 --- a/src/ctypeList.c +++ b/src/ctypeList.c @@ -79,6 +79,7 @@ void ctypeList_addh (ctypeList s, ctype el) s->nelements++; } +# ifdef DEADCODE ctypeList ctypeList_add (ctypeList s, ctype el) { llassert (ctypeListBASESIZE > 0); @@ -131,6 +132,7 @@ ctypeList_unparse (ctypeList ct) return s; } +# endif /* DEADCODE */ void ctypeList_free (/*@only@*/ ctypeList s) @@ -148,9 +150,3 @@ ctypeList_free (/*@only@*/ ctypeList s) } } - - - - - - diff --git a/src/declaratorInvNodeList.c b/src/declaratorInvNodeList.c index 256cc30..975f1af 100644 --- a/src/declaratorInvNodeList.c +++ b/src/declaratorInvNodeList.c @@ -32,6 +32,10 @@ # include "splintMacros.nf" # include "basic.h" + +/*@constant int declaratorInvNodeListBASESIZE;@*/ +# define declaratorInvNodeListBASESIZE SMALLBASESIZE + declaratorInvNodeList declaratorInvNodeList_new (void) { @@ -86,6 +90,7 @@ declaratorInvNodeList_add (declaratorInvNodeList s, declaratorInvNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring declaratorInvNodeList_unparse (declaratorInvNodeList s) { @@ -99,6 +104,7 @@ declaratorInvNodeList_unparse (declaratorInvNodeList s) return st; } +# endif /* DEADCODE */ void declaratorInvNodeList_free (declaratorInvNodeList s) diff --git a/src/enumNameList.c b/src/enumNameList.c index cbc08a7..85fb30d 100644 --- a/src/enumNameList.c +++ b/src/enumNameList.c @@ -34,6 +34,10 @@ # include "splintMacros.nf" # include "basic.h" + +/*@constant int enumNameListBASESIZE;@*/ +# define enumNameListBASESIZE SMALLBASESIZE + enumNameList enumNameList_new (void) { @@ -116,6 +120,7 @@ enumNameList_push (/*@returned@*/ enumNameList s, /*@only@*/ enumName el) return s; } +#ifdef DEADCODE /*@only@*/ enumNameList enumNameList_copy (enumNameList s) { @@ -128,6 +133,7 @@ enumNameList_copy (enumNameList s) return r; } +#endif bool enumNameList_member (enumNameList s, cstring m) diff --git a/src/exprChecks.c b/src/exprChecks.c index 0b5e813..769f08d 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -557,12 +557,11 @@ exprNode_checkAllMods (sRefSet mods, uentry ue) bool realParams = FALSE; uentry le = context_getHeader (); fileloc fl = uentry_whereSpecified (le); - uentryList specParamNames = uentryList_undefined; uentryList paramNames = context_getParams (); if (uentry_isFunction (le)) { - specParamNames = uentry_getParams (le); + uentryList specParamNames = uentry_getParams (le); if (uentryList_isUndefined (specParamNames)) { @@ -1614,7 +1613,3 @@ static void checkSafeReturnExpr (/*@notnull@*/ exprNode e) } } - - - - diff --git a/src/exprData.c b/src/exprData.c index 197902f..d23443f 100644 --- a/src/exprData.c +++ b/src/exprData.c @@ -2,13 +2,9 @@ ** exprData.c */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - void exprData_freeShallow (/*@only@*/ exprData data, exprKind kind) { /*@-compdestroy@*/ @@ -542,7 +538,7 @@ exprData_makeIter (/*@exposed@*/ uentry sname, /*@keep@*/ exprNodeList args, return ed; } -/*@only@*/ exprData exprData_makeTriple (/*@keep@*/ exprNode pred, +static /*@only@*/ exprData exprData_makeTriple (/*@keep@*/ exprNode pred, /*@keep@*/ exprNode tbranch, /*@keep@*/ exprNode fbranch) { diff --git a/src/exprNode.c b/src/exprNode.c index 30a198b..cf04f20 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -25,9 +25,9 @@ ** exprNode.c */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" + # include "cscannerHelp.h" # include "cgrammar.h" @@ -40,6 +40,7 @@ static bool exprNode_isEmptyStatement (exprNode p_e); static /*@exposed@*/ exprNode exprNode_firstStatement (/*@returned@*/ exprNode p_e); static bool exprNode_isFalseConstant (exprNode p_e) /*@*/ ; static bool exprNode_isStatement (exprNode p_e); +static /*@falsewhennull@*/ bool exprNode_isBlock (exprNode p_e) /*@*/ ; static void checkGlobUse (uentry p_glob, bool p_isCall, /*@notnull@*/ exprNode p_e); static void exprNode_addUse (exprNode p_e, /*@exposed@*/ sRef p_s); static bool exprNode_matchArgType (ctype p_ct, exprNode p_e); @@ -810,7 +811,7 @@ exprNode_combineLiterals (exprNode e, exprNode rest) return e; } -/*@only@*/ exprNode +static /*@notnull@*/ /*@only@*/ exprNode exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) { exprNode e = exprNode_createLoc (ctype_string, loc); @@ -1450,7 +1451,6 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, int i = argno; fileloc formatloc; - int nargs = exprNodeList_size (args); uentryList params = uentry_getParams (fcn); exprNode a; @@ -1470,8 +1470,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, char *format = cstring_toCharsSafe (multiVal_forceString (exprNode_getValue (a))); char *code = format; char *ocode = code; - - nargs = exprNodeList_size (args); + int nargs = exprNodeList_size (args); while ((code = strchr (code, '%')) != NULL) { @@ -1784,7 +1783,6 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, { int i = argno; fileloc formatloc; - int nargs = exprNodeList_size (args); uentryList params = uentry_getParams (fcn); exprNode a; @@ -1804,8 +1802,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, char *format = cstring_toCharsSafe (multiVal_forceString (exprNode_getValue (a))); char *code = format; char *ocode = code; - - nargs = exprNodeList_size (args); + int nargs = exprNodeList_size (args); while ((code = strchr (code, '%')) != NULL) { @@ -2096,7 +2093,6 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, ** the last argument before the elips is the format string */ - int nargs = exprNodeList_size (args); int i = argno; fileloc formatloc; exprNode a; @@ -2131,8 +2127,7 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, cstring format = multiVal_forceString (exprNode_getValue (a)); char *code = cstring_toCharsSafe (format); char *ocode = code; - - nargs = exprNodeList_size (args); + int nargs = exprNodeList_size (args); while ((code = strchr (code, '%')) != NULL) { @@ -6561,7 +6556,7 @@ exprNode exprNode_notReached (/*@returned@*/ exprNode stmt) return (stmt); } -bool exprNode_isDefaultMarker (exprNode e) +static bool exprNode_isDefaultMarker (exprNode e) { if (exprNode_isDefined (e)) { @@ -6581,7 +6576,7 @@ bool exprNode_isCaseMarker (exprNode e) return FALSE; } -bool exprNode_isLabelMarker (exprNode e) +static bool exprNode_isLabelMarker (exprNode e) { if (exprNode_isDefined (e)) { @@ -6939,7 +6934,7 @@ exprNode exprNode_makeBlock (/*@only@*/ exprNode e) return ret; } -bool exprNode_isBlock (exprNode e) +static bool exprNode_isBlock (exprNode e) { return (exprNode_isDefined (e) && ((e)->kind == XPR_BLOCK)); @@ -9431,52 +9426,7 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e) case XPR_INIT: ret = idDecl_getName (exprData_getInitId (data)); break; - case XPR_LABEL: - case XPR_TOK: - case XPR_ITERCALL: - case XPR_EMPTY: - case XPR_CALL: - case XPR_INITBLOCK: - case XPR_BODY: - case XPR_FETCH: - case XPR_OP: - case XPR_POSTOP: - case XPR_PREOP: - case XPR_OFFSETOF: - case XPR_ALIGNOFT: - case XPR_ALIGNOF: - case XPR_SIZEOFT: - case XPR_SIZEOF: - case XPR_VAARG: - case XPR_CAST: - case XPR_ITER: - case XPR_FOR: - case XPR_FORPRED: - case XPR_BREAK: - case XPR_RETURN: - case XPR_NULLRETURN: - case XPR_COMMA: - case XPR_COND: - case XPR_IF: - case XPR_IFELSE: - case XPR_WHILE: - case XPR_WHILEPRED: - case XPR_DOWHILE: - case XPR_GOTO: - case XPR_CONTINUE: - case XPR_FTDEFAULT: - case XPR_DEFAULT: - case XPR_SWITCH: - case XPR_FTCASE: - case XPR_CASE: - case XPR_BLOCK: - case XPR_STMT: - case XPR_STMTLIST: - case XPR_FACCESS: - case XPR_ARROW: - case XPR_NODE: - case XPR_NUMLIT: - case XPR_STRINGLITERAL: + default: ret = cstring_undefined; break; } diff --git a/src/exprNodeList.c b/src/exprNodeList.c index 371a703..fed3a2b 100644 --- a/src/exprNodeList.c +++ b/src/exprNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int exprNodeListBASESIZE;@*/ +# define exprNodeListBASESIZE SMALLBASESIZE + /*@only@*/ exprNodeList exprNodeList_new (void) { diff --git a/src/exprNodeSList.c b/src/exprNodeSList.c index a2acd66..d716250 100644 --- a/src/exprNodeSList.c +++ b/src/exprNodeSList.c @@ -33,6 +33,9 @@ # include "basic.h" # include "exprNodeSList.h" +/*@constant int exprNodeSListBASESIZE;@*/ +# define exprNodeSListBASESIZE SMALLBASESIZE + exprNodeSList exprNodeSList_new (void) { @@ -71,7 +74,7 @@ exprNodeSList_grow (exprNodeSList s) s->elements = newelements; } -void exprNodeSList_addh (exprNodeSList s, /*@exposed@*/ /*@dependent@*/ exprNode el) +static /*@unused@*/ void exprNodeSList_addh (exprNodeSList s, /*@exposed@*/ /*@dependent@*/ exprNode el) { llassert (exprNodeSListBASESIZE > 0); @@ -110,6 +113,7 @@ exprNodeSList exprNodeSList_append (/*@returned@*/ exprNodeSList s1, /*@only@*/ return (s); } +# ifdef DEADCODE /*@only@*/ cstring exprNodeSList_unparse (exprNodeSList s) { @@ -128,6 +132,7 @@ exprNodeSList_unparse (exprNodeSList s) return st; } +# endif /* DEADCODE */ void exprNodeSList_free (exprNodeSList s) diff --git a/src/fcnNodeList.c b/src/fcnNodeList.c index d9c91d6..af9f0ae 100644 --- a/src/fcnNodeList.c +++ b/src/fcnNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int fcnNodeListBASESIZE;@*/ +# define fcnNodeListBASESIZE SMALLBASESIZE + fcnNodeList fcnNodeList_new (void) { @@ -92,6 +95,7 @@ fcnNodeList_add (fcnNodeList s, fcnNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring fcnNodeList_unparse (fcnNodeList s) { @@ -108,6 +112,7 @@ fcnNodeList_unparse (fcnNodeList s) return st; } +# endif /* DEADCODE */ void fcnNodeList_free (/*@null@*/ /*@only@*/ fcnNodeList s) diff --git a/src/fileLib.c b/src/fileLib.c index b96b386..80fc337 100644 --- a/src/fileLib.c +++ b/src/fileLib.c @@ -45,7 +45,7 @@ fileLib_isCExtension (cstring ext) bool fileLib_isLCLFile (cstring s) { - return (fileLib_hasExtension (s, LCL_EXTENSION)); + return cstring_equal (fileLib_getExtension (s), LCL_EXTENSION); } /*@only@*/ cstring fileLib_withoutExtension (/*@temp@*/ cstring s, cstring suffix) @@ -155,11 +155,6 @@ fileLib_addExtension (/*@temp@*/ cstring s, cstring suffix) } } -bool fileLib_hasExtension (cstring s, cstring ext) -{ - return cstring_equal (fileLib_getExtension (s), ext); -} - /*@observer@*/ cstring fileLib_getExtension (/*@returned@*/ cstring s) { llassert (cstring_isDefined (s)); diff --git a/src/fileTable.c b/src/fileTable.c index 15dd35c..5af1fbd 100644 --- a/src/fileTable.c +++ b/src/fileTable.c @@ -38,7 +38,6 @@ # include "splintMacros.nf" # include "basic.h" # include "osd.h" -# include "llmain.h" /*@access fileId*/ @@ -55,6 +54,7 @@ static fileId fileTable_internAddEntry (fileTable p_ft, /*@only@*/ ftentry p_e) /*@modifies p_ft@*/ ; static /*@only@*/ cstring makeTempName (cstring p_pre, cstring p_suf); +# ifdef DEADCODE static /*@only@*/ cstring fileType_unparse (fileType ft) { @@ -77,6 +77,7 @@ fileType_unparse (fileType ft) BADEXIT; } +# endif /* DEADCODE */ static int fileTable_getIndex (fileTable ft, cstring s) @@ -97,6 +98,7 @@ fileTable_getIndex (fileTable ft, cstring s) return res; } +# ifdef DEADCODE static cstring ftentry_unparse (fileTable ft, ftentry fte) { if (fileId_isValid (fte->fder)) @@ -134,6 +136,7 @@ fileTable_unparse (fileTable ft) return s; } +# endif /* DEADCODE */ void fileTable_printTemps (fileTable ft) { diff --git a/src/fileloc.c b/src/fileloc.c index d636d75..66f5245 100644 --- a/src/fileloc.c +++ b/src/fileloc.c @@ -880,6 +880,7 @@ bool fileloc_isStandardLib (fileloc f) return (fileloc_isDefined (f) && f->kind == FL_STDLIB); } +# ifdef DEADCODE /*@only@*/ cstring fileloc_unparseDirect (fileloc fl) { if (fileloc_isDefined (fl)) @@ -893,6 +894,7 @@ bool fileloc_isStandardLib (fileloc f) return (cstring_makeLiteral ("")); } } +# endif /* DEADCODE */ bool fileloc_isUser (fileloc f) { diff --git a/src/filelocList.c b/src/filelocList.c index ce6b74c..e58c0f0 100644 --- a/src/filelocList.c +++ b/src/filelocList.c @@ -27,7 +27,9 @@ # include "splintMacros.nf" # include "basic.h" -# include "filelocList.h" + +/*@constant int filelocListBASESIZE;@*/ +# define filelocListBASESIZE MIDBASESIZE /* ** Invariant: If any member of the list is fileloc_undefined, then @@ -174,6 +176,7 @@ filelocList return s; } +# ifdef DEADCODE /*@only@*/ cstring filelocList_unparse (filelocList s) { @@ -196,6 +199,7 @@ filelocList_unparse (filelocList s) st = message ("%q ]", st); return st; } +# endif /* DEADCODE */ int filelocList_realSize (filelocList s) { diff --git a/src/filelocStack.c b/src/filelocStack.c index b037dd1..7174a1c 100644 --- a/src/filelocStack.c +++ b/src/filelocStack.c @@ -29,6 +29,9 @@ # include "basic.h" # include "filelocStack.h" +/*@constant int filelocStackBASESIZE;@*/ +# define filelocStackBASESIZE MIDBASESIZE + static /*@notnull@*/ /*@only@*/ filelocStack filelocStack_newEmpty (void) { @@ -134,6 +137,7 @@ bool filelocStack_popPushFile (filelocStack s, fileloc el) return TRUE; } +# ifdef DEADCODE /*@only@*/ cstring filelocStack_unparse (filelocStack s) { @@ -158,6 +162,7 @@ filelocStack_unparse (filelocStack s) st = message ("%q ]", st); return st; } +# endif /* DEADCODE */ int filelocStack_includeDepth (filelocStack s) { @@ -226,8 +231,3 @@ filelocStack_free (/*@only@*/ filelocStack s) } } - - - - - diff --git a/src/flagMarkerList.c b/src/flagMarkerList.c index 0c57af0..64d8ee7 100644 --- a/src/flagMarkerList.c +++ b/src/flagMarkerList.c @@ -34,7 +34,11 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int flagMarkerListBASESIZE;@*/ +# define flagMarkerListBASESIZE SMALLBASESIZE + static int flagMarkerList_lastBeforeLoc (flagMarkerList p_s, fileloc p_loc) /*@*/ ; +static /*@only@*/ cstring flagMarkerList_unparse (flagMarkerList p_s) /*@*/ ; static bool flagMarkerList_contains (flagMarkerList p_s, flagMarker p_fm) /*@*/ ; @@ -307,7 +311,7 @@ static void flagMarkerList_splice (flagMarkerList s, } -/*@only@*/ cstring +static /*@only@*/ cstring flagMarkerList_unparse (flagMarkerList s) { int i; diff --git a/src/functionClause.c b/src/functionClause.c index 27f862c..5f30732 100644 --- a/src/functionClause.c +++ b/src/functionClause.c @@ -129,6 +129,7 @@ extern bool functionClause_matchKind (functionClause p, functionClauseKind kind) } } +# ifdef DEADCODE extern stateClause functionClause_getState (functionClause node) { llassert (functionClause_isDefined (node)); @@ -136,6 +137,7 @@ extern stateClause functionClause_getState (functionClause node) return node->val.state; } +# endif /* DEADCODE */ extern stateClause functionClause_takeState (functionClause fc) { @@ -149,6 +151,7 @@ extern stateClause functionClause_takeState (functionClause fc) return res; } +# ifdef DEADCODE extern functionConstraint functionClause_getEnsures (functionClause node) { llassert (functionClause_isDefined (node)); @@ -156,6 +159,7 @@ extern functionConstraint functionClause_getEnsures (functionClause node) return node->val.constraint; } +# endif /* DEADCODE */ extern functionConstraint functionClause_takeEnsures (functionClause fc) { @@ -189,6 +193,7 @@ extern functionConstraint functionClause_takeRequires (functionClause fc) return res; } +# ifdef DEADCODE extern warnClause functionClause_getWarn (functionClause node) { llassert (functionClause_isDefined (node)); @@ -196,6 +201,7 @@ extern warnClause functionClause_getWarn (functionClause node) return node->val.warn; } +# endif /* DEADCODE */ extern warnClause functionClause_takeWarn (functionClause fc) { diff --git a/src/functionClauseList.c b/src/functionClauseList.c index 07a4d2c..1b0ff8d 100644 --- a/src/functionClauseList.c +++ b/src/functionClauseList.c @@ -31,6 +31,9 @@ # include "splintMacros.nf" # include "basic.h" + +/*@constant int functionClauseListBASESIZE;@*/ +# define functionClauseListBASESIZE MIDBASESIZE functionClauseList functionClauseList_new (void) @@ -74,14 +77,8 @@ functionClauseList_grow (/*@notnull@*/ functionClauseList s) s->elements = newelements; } -functionClauseList functionClauseList_single (/*@keep@*/ functionClause el) -{ - functionClauseList s = functionClauseList_new (); - s = functionClauseList_add (s, el); - return s; -} - -functionClauseList functionClauseList_add (functionClauseList s, /*@keep@*/ functionClause el) +static functionClauseList functionClauseList_add (/*@returned@*/ functionClauseList s, /*@keep@*/ functionClause el) + /*@modifies s@*/ { if (!functionClauseList_isDefined (s)) { @@ -100,6 +97,13 @@ functionClauseList functionClauseList_add (functionClauseList s, /*@keep@*/ func return s; } +static /*@only@*/ functionClauseList functionClauseList_single (/*@keep@*/ functionClause el) +{ + functionClauseList s = functionClauseList_new (); + s = functionClauseList_add (s, el); + return s; +} + functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ functionClause el) { int i; @@ -127,13 +131,7 @@ functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ return s; } -cstring -functionClauseList_unparse (functionClauseList s) -{ - return functionClauseList_unparseSep (s, cstring_makeLiteralTemp (" ")); -} - -cstring +static cstring functionClauseList_unparseSep (functionClauseList s, cstring sep) { cstring st = cstring_undefined; @@ -156,6 +154,12 @@ functionClauseList_unparseSep (functionClauseList s, cstring sep) return st; } +cstring +functionClauseList_unparse (functionClauseList s) +{ + return functionClauseList_unparseSep (s, cstring_makeLiteralTemp (" ")); +} + void functionClauseList_free (functionClauseList s) { diff --git a/src/genericTable.c b/src/genericTable.c index c01683f..f4f0991 100644 --- a/src/genericTable.c +++ b/src/genericTable.c @@ -35,6 +35,9 @@ /*@constant null ghbucket ghbucket_undefined; @*/ # define ghbucket_undefined 0 +/*@constant int GHBUCKET_BASESIZE; @*/ +# define GHBUCKET_BASESIZE 2 + static /*@nullwhentrue@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h) { return (h == ghbucket_undefined); @@ -62,11 +65,13 @@ ghentry_free (/*@only@*/ ghentry ghe) sfree (ghe); } +# if 0 static bool ghbucket_isEmpty (ghbucket h) { return (h == ghbucket_undefined || h->size == 0); } +# endif int genericTable_size (genericTable h) { @@ -158,6 +163,7 @@ ghbucket_add (/*@notnull@*/ ghbucket h, /*@only@*/ ghentry e) h->nspace--; } +# if 0 static int ghbucket_ncollisions (ghbucket h) { @@ -166,6 +172,7 @@ ghbucket_ncollisions (ghbucket h) else return 0; } +# endif /*@exposed@*/ /*@null@*/ void * ghbucket_lookup (ghbucket h, cstring key) @@ -220,6 +227,7 @@ genericTable_free (/*@only@*/ genericTable h) } } +# if 0 static int genericTable_countCollisions (genericTable h) { @@ -255,6 +263,7 @@ genericTable_countEmpty (genericTable h) return (nc); } +# endif static unsigned int genericTable_hashValue (/*@notnull@*/ genericTable h, cstring key) @@ -319,6 +328,7 @@ genericTable_print (genericTable h) /*@=mustfree@*/ # endif +# ifdef DEADCODE /*@only@*/ cstring genericTable_stats (genericTable h) { @@ -327,6 +337,7 @@ genericTable_stats (genericTable h) h->size, genericTable_countCollisions (h), genericTable_countEmpty (h))); } +# endif /* DEADCODE */ static void genericTable_addEntry (/*@notnull@*/ genericTable h, /*@only@*/ ghentry e) @@ -462,6 +473,7 @@ genericTable_update (genericTable h, cstring key, /*@only@*/ void *newval) llbug (message ("genericTable_update: %s not found", key)); } +# ifdef DEADCODE void genericTable_remove (genericTable h, cstring key) { @@ -491,6 +503,7 @@ genericTable_remove (genericTable h, cstring key) llbug (message ("genericTable_removeKey: %s not found", key)); } +# endif /* DEADCODE */ bool genericTable_contains (genericTable h, cstring key) { diff --git a/src/globSet.c b/src/globSet.c index 78090f7..5992b0f 100644 --- a/src/globSet.c +++ b/src/globSet.c @@ -100,6 +100,7 @@ globSet_member (globSet s, sRef el) return sRef_undefined; } +# ifdef DEADCODE bool globSet_hasStatic (globSet s) { @@ -113,6 +114,7 @@ globSet_hasStatic (globSet s) return FALSE; } +# endif /* DEADCODE */ void globSet_free (/*@only@*/ globSet s) @@ -171,9 +173,11 @@ globSet_unparse (globSet ll) return (sRefSet_unparsePlain (ll)); } +# ifdef DEADCODE int globSet_compare (globSet l1, globSet l2) { return (sRefSet_compare (l1, l2)); } +# endif /* DEADCODE */ diff --git a/src/globalsClause.c b/src/globalsClause.c index a0c9fca..0af71bc 100644 --- a/src/globalsClause.c +++ b/src/globalsClause.c @@ -38,10 +38,12 @@ globalsClause_create (lltok tok, globSet gl) return res; /* releases doesn't seem to work right here... */ } +# ifdef DEADCODE globSet globalsClause_getGlobs (globalsClause gclause) { return gclause->globs; } +# endif /* DEADCODE */ globSet globalsClause_takeGlobs (globalsClause gclause) { diff --git a/src/help.c b/src/help.c index 80c6cc0..791dbc6 100644 --- a/src/help.c +++ b/src/help.c @@ -28,7 +28,6 @@ # include "splintMacros.nf" # include "basic.h" # include "help.h" -# include "osd.h" # include "llmain.h" # include "version.h" diff --git a/src/idDecl.c b/src/idDecl.c index d60e65e..5aa3e5a 100644 --- a/src/idDecl.c +++ b/src/idDecl.c @@ -28,7 +28,7 @@ # include "splintMacros.nf" # include "basic.h" -/*@only@*/ idDecl +static /*@only@*/ idDecl idDecl_createClauses (/*@only@*/ cstring s, /*@only@*/ qtype t, /*@only@*/ functionClauseList clauses) { idDecl d = (idDecl) dmalloc (sizeof (*d)); diff --git a/src/idDeclList.c b/src/idDeclList.c index 5ebf296..2ed854c 100644 --- a/src/idDeclList.c +++ b/src/idDeclList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int idDeclListBASESIZE;@*/ +# define idDeclListBASESIZE SMALLBASESIZE + idDeclList idDeclList_singleton (/*@only@*/ idDecl e) { @@ -75,6 +78,7 @@ idDeclList idDeclList_add (idDeclList s, /*@only@*/ idDecl el) return s; } +# ifdef DEADCODE /*@only@*/ cstring idDeclList_unparse (idDeclList s) { @@ -94,6 +98,7 @@ idDeclList_unparse (idDeclList s) st = message ("%q ]", st); return st; } +# endif /* DEADCODE */ void idDeclList_free (idDeclList s) diff --git a/src/importNodeList.c b/src/importNodeList.c index 6b10399..33e40a3 100644 --- a/src/importNodeList.c +++ b/src/importNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int importNodeListBASESIZE;@*/ +# define importNodeListBASESIZE SMALLBASESIZE + /*@only@*/ importNodeList importNodeList_new (void) { @@ -77,6 +80,7 @@ importNodeList_add (importNodeList s, importNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring importNodeList_unparse (importNodeList s) { @@ -98,6 +102,7 @@ importNodeList_unparse (importNodeList s) return st; } +# endif /* DEADCODE */ void importNodeList_free (importNodeList s) diff --git a/src/imports.c b/src/imports.c index 0aa4fdc..936cdda 100644 --- a/src/imports.c +++ b/src/imports.c @@ -34,12 +34,8 @@ # include "splintMacros.nf" # include "basic.h" # include "osd.h" -# include "llgrammar.h" /* need simpleOp, MULOP and logicalOp in makeInfixTermNode */ -# include "lclscan.h" -# include "checking.h" # include "imports.h" # include "lslparse.h" -# include "lh.h" # include "llmain.h" void @@ -385,5 +381,3 @@ processImport (lsymbol importSymbol, ltoken tok, impkind kind) context_leaveImport (); } - - diff --git a/src/initDeclNodeList.c b/src/initDeclNodeList.c index a17e81a..dfb58cc 100644 --- a/src/initDeclNodeList.c +++ b/src/initDeclNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int initDeclNodeListBASESIZE;@*/ +# define initDeclNodeListBASESIZE SMALLBASESIZE + /*@only@*/ initDeclNodeList initDeclNodeList_new (void) { @@ -77,6 +80,7 @@ initDeclNodeList_add (initDeclNodeList s, initDeclNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring initDeclNodeList_unparse (initDeclNodeList s) { @@ -103,6 +107,7 @@ initDeclNodeList_unparse (initDeclNodeList s) return st; } +# endif /* DEADCODE */ void initDeclNodeList_free (initDeclNodeList s) diff --git a/src/intSet.c b/src/intSet.c index 4d03792..322c578 100644 --- a/src/intSet.c +++ b/src/intSet.c @@ -33,6 +33,9 @@ # include "basic.h" # include "intSet.h" +/*@constant int intSetBASESIZE;@*/ +# define intSetBASESIZE SMALLBASESIZE + /*@only@*/ intSet intSet_new (void) { @@ -112,6 +115,7 @@ intSet_insert (intSet s, int el) } } +# ifdef DEADCODE bool intSet_member (intSet s, int el) { @@ -130,6 +134,7 @@ intSet_member (intSet s, int el) } return FALSE; } +# endif /* DEADCODE */ /*@only@*/ cstring intSet_unparseText (intSet s) @@ -151,6 +156,7 @@ intSet_unparseText (intSet s) return st; } +# ifdef DEADCODE /*@only@*/ cstring intSet_unparse (intSet s) { @@ -165,6 +171,7 @@ intSet_unparse (intSet s) st = message ("%q}", st); return st; } +# endif /* DEADCODE */ void intSet_free (intSet s) diff --git a/src/lclinit.c b/src/lclinit.c index ceae01c..5e696ac 100644 --- a/src/lclinit.c +++ b/src/lclinit.c @@ -1469,8 +1469,6 @@ lclinit_initMod (void) { int i; - LSLGenInit (FALSE); /* parsing LCLinit, not LSLinit */ - /* ** Insert the init file keywords into the token table as undefined ** SIMPLEIDs. They are defined as simpleIds since they must be treated diff --git a/src/lcllib.c b/src/lcllib.c index 4f793bb..57a3d95 100644 --- a/src/lcllib.c +++ b/src/lcllib.c @@ -39,7 +39,6 @@ # include "version.h" # include "lcllib.h" -# include "llmain.h" /*@constant int NUMLIBS; @*/ # define NUMLIBS 25 @@ -265,11 +264,11 @@ dumpState (cstring cfname) printDot (); - /* +# if 0 DPRINTF (("Before prepare dump:")); ctype_printTable (); DPRINTF (("Preparing dump...")); - */ +# endif usymtab_prepareDump (); diff --git a/src/lclscanline.c b/src/lclscanline.c index 1ce4378..3ef4372 100644 --- a/src/lclscanline.c +++ b/src/lclscanline.c @@ -400,7 +400,6 @@ static bool isSimpleEscape[CHARSIZE] = static bool reportEOL; static bool reportComments; -static lsymbol firstReserved; static char tokenBuffer[MAXCHAR]; @@ -1738,7 +1737,7 @@ LCLScanLineInit (void) ** mean empty. */ - firstReserved = lsymbol_fromChars (FIRSTRESERVEDNAME); + (void) lsymbol_fromChars (FIRSTRESERVEDNAME); setCodePoint (); /* Predefined LSL Tokens */ diff --git a/src/letDeclNodeList.c b/src/letDeclNodeList.c index 23f8663..62bd8de 100644 --- a/src/letDeclNodeList.c +++ b/src/letDeclNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int letDeclNodeListBASESIZE;@*/ +# define letDeclNodeListBASESIZE SMALLBASESIZE + /*@only@*/ letDeclNodeList letDeclNodeList_new (void) { @@ -80,6 +83,7 @@ letDeclNodeList_add (letDeclNodeList s, letDeclNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring letDeclNodeList_unparse (letDeclNodeList s) { @@ -102,6 +106,7 @@ letDeclNodeList_unparse (letDeclNodeList s) return st; } +# endif /* DEADCODE */ void letDeclNodeList_free (letDeclNodeList s) diff --git a/src/lh.c b/src/lh.c index 497e614..d6c8505 100644 --- a/src/lh.c +++ b/src/lh.c @@ -43,7 +43,6 @@ # include "basic.h" # include "osd.h" # include "lh.h" -# include "llmain.h" /*:private:*/ typedef struct @@ -54,7 +53,6 @@ static bool genLh; static outFile LhFile; -static bool needIncludeBool = FALSE; /* ** @@ -281,13 +279,6 @@ lhCleanup (void) } } -/* Write an #include of bool.h if we have't done so already. */ -extern void -lhIncludeBool (void) -{ - needIncludeBool = TRUE; -} - static cstring LSLRootName (cstring filespec) { @@ -313,7 +304,6 @@ void lhInit (inputStream f) /*@globals undef LhFile; @*/ static bool lherror = FALSE; genLh = context_msgLh (); - needIncludeBool = FALSE; if (!genLh) { diff --git a/src/llerror.c b/src/llerror.c index 9a6168f..ec3a3ee 100644 --- a/src/llerror.c +++ b/src/llerror.c @@ -100,7 +100,8 @@ printBugReport (void) static bool s_needsPrepare = TRUE; -void prepareMessage (void) +static void prepareMessage (void) + /*@modifies internalState, g_messagestream@*/ { DPRINTF (("Prepare message: %s", bool_unparse (context_loadingLibrary ()))); showHerald (); @@ -117,7 +118,8 @@ void prepareMessage (void) llflush (); } -void closeMessage (void) +static void closeMessage (void) + /*@modifies internalState, g_messagestream@*/ { if (context_isPreprocessing () && context_getFlag (FLG_SHOWSCAN)) @@ -454,8 +456,6 @@ mstring_split (/*@returned@*/ char **sp, char *lcolon, *lsemi, *lcomma; char *splitat; - splitat = NULL; - t = s + maxline - 1; savechar = *t; @@ -1779,6 +1779,7 @@ void ppllerror (/*@only@*/ cstring s) genppllerror (FLG_PREPROC, s); } +# ifdef DEADCODE void pplldiagmsg (cstring s) { if (!context_isInCommandLine ()) @@ -1796,6 +1797,7 @@ void pplldiagmsg (cstring s) lldiagmsg (s); } } +# endif /* DEADCODE */ void loadllmsg (cstring s) { diff --git a/src/llmain.c b/src/llmain.c index 6ac3b00..e9bc015 100644 --- a/src/llmain.c +++ b/src/llmain.c @@ -41,13 +41,11 @@ # include "lslsyntable.h" # include "lsltokentable.h" # include "lslinit.h" -# include "lslparse.h" # include "lclscan.h" # include "lclscanline.h" # include "lclsyntable.h" # include "lcltokentable.h" -# include "lclinit.h" # include "lcllib.h" # include "llgrammar.h" @@ -61,6 +59,7 @@ # include "Headers/version.h" /* Visual C++ finds the wrong version.h */ # include "rcfiles.h" +# include "cpp.h" # include "llmain.h" static void cleanupFiles (void); @@ -76,7 +75,6 @@ static char* specFullName (char *p_specfile, /*@out@*/ char **p_inpath) /*@modifies *p_inpath@*/ ; static bool anylcl = FALSE; -static clock_t inittime; static fileIdList preprocessFiles (fileIdList) /*@modifies fileSystem@*/ ; @@ -126,7 +124,6 @@ lslProcess (fileIdList lclfiles) bool overallStatus = FALSE; lslinit_process (); - inittime = clock (); context_resetSpecLines (); @@ -514,8 +511,6 @@ int main (int argc, char *argv[]) initAnnots (); # endif - inittime = clock (); - context_resetErrors (); context_clearInCommandLine (); diff --git a/src/loopHeuristics.c b/src/loopHeuristics.c index c09e75c..68ba164 100644 --- a/src/loopHeuristics.c +++ b/src/loopHeuristics.c @@ -32,13 +32,9 @@ /* #define DEBUGPRINT 1 */ -# include /* for isdigit */ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "exprNodeSList.h" - /* this file was created to split the loop heuristics functionality out of constraintGeneration.c and constraint.c*/ /*We need to access the internal representation of constraint see above for an explanation. diff --git a/src/lslOpList.c b/src/lslOpList.c index f85bcf9..3fae13a 100644 --- a/src/lslOpList.c +++ b/src/lslOpList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int lslOpListBASESIZE;@*/ +# define lslOpListBASESIZE SMALLBASESIZE + /*@only@*/ lslOpList lslOpList_new (void) { @@ -85,6 +88,7 @@ lslOpList_add (lslOpList s, lslOp el) s->nelements++; } +# ifdef DEADCODE /*@only@*/ cstring lslOpList_unparse (lslOpList s) { @@ -98,6 +102,7 @@ lslOpList_unparse (lslOpList s) return st; } +# endif /* DEADCODE */ void lslOpList_free (lslOpList s) diff --git a/src/lslOpSet.c b/src/lslOpSet.c index 0b51dd2..9a399df 100644 --- a/src/lslOpSet.c +++ b/src/lslOpSet.c @@ -32,7 +32,9 @@ # include "splintMacros.nf" # include "basic.h" -# include "checking.h" /* for lslOp_equal */ + +/*@constant int lslOpSetBASESIZE;@*/ +# define lslOpSetBASESIZE MIDBASESIZE static bool lslOpSet_member (lslOpSet p_s, lslOp p_el); @@ -138,6 +140,7 @@ lslOpSet_member (lslOpSet s, lslOp el) return FALSE; } +# ifdef DEADCODE /*@only@*/ cstring lslOpSet_unparse (lslOpSet s) { @@ -159,6 +162,7 @@ lslOpSet_unparse (lslOpSet s) return (cstring_makeLiteral ("{ }")); } } +# endif /* DEADCODE */ /*@only@*/ lslOpSet lslOpSet_copy (lslOpSet s) diff --git a/src/lslinit.c b/src/lslinit.c index de1b701..14c10eb 100644 --- a/src/lslinit.c +++ b/src/lslinit.c @@ -1557,8 +1557,6 @@ lslinit_initProcessInitFile (void) { int i; - LSLGenInit (TRUE); /* parsing LSLinit not LCLinit */ - /* ** Insert the init file keywords into the token table as undefined ** SIMPLEIDs. They are defined as simpleIds since they must be treated diff --git a/src/lslparse.c b/src/lslparse.c index eb252e4..e81dc90 100644 --- a/src/lslparse.c +++ b/src/lslparse.c @@ -38,14 +38,9 @@ # include "lslgrammar.h" # include "lslscan.h" # include "lslscanline.h" -# include "lslsyntable.h" # include "lsltokentable.h" -# include "lslinit.h" # include "lslparse.h" -# include "lclscan.h" -# include "llmain.h" - /*@+ignorequals@*/ /*@dependent@*/ /*@null@*/ lslOp g_importedlslOp = NULL; diff --git a/src/lsltokentable.c b/src/lsltokentable.c index a373224..64f0132 100644 --- a/src/lsltokentable.c +++ b/src/lsltokentable.c @@ -27,7 +27,6 @@ # include "splintMacros.nf" # include "basic.h" -# include "osd.h" # include "lsltokentable.h" diff --git a/src/lsymbol.c b/src/lsymbol.c index 95b7400..8a33609 100644 --- a/src/lsymbol.c +++ b/src/lsymbol.c @@ -341,12 +341,14 @@ lsymbol_destroyMod (void) sfree (hashArray); } +# ifdef DEADCODE void lsymbol_printStats (void) { /* only for debugging */ printf ("Number of lsymbols generated = %d\n", (int) FreeEntry); } +# endif /* DEADCODE */ /* ** note lsymbol_setbool, etc. defined in abstract.c diff --git a/src/lsymbolSet.c b/src/lsymbolSet.c index f656701..84f55f1 100644 --- a/src/lsymbolSet.c +++ b/src/lsymbolSet.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int lsymbolSetBASESIZE;@*/ +# define lsymbolSetBASESIZE MIDBASESIZE + lsymbolSet lsymbolSet_new (void) { lsymbolSet s = (lsymbolSet) dmalloc (sizeof (*s)); @@ -117,6 +120,7 @@ lsymbolSet_member (lsymbolSet s, lsymbol el) return FALSE; } +# ifdef DEADCODE /*@only@*/ cstring lsymbolSet_unparse (lsymbolSet s) { @@ -145,6 +149,7 @@ lsymbolSet_unparse (lsymbolSet s) return (cstring_makeLiteral ("{ }")); } } +# endif /* DEADCODE */ void lsymbolSet_free (/*@null@*/ lsymbolSet s) diff --git a/src/macrocache.c b/src/macrocache.c index 4fd0fee..6865f8e 100644 --- a/src/macrocache.c +++ b/src/macrocache.c @@ -33,7 +33,6 @@ # include "basic.h" # include "cscanner.h" # include "cgrammar.h" -# include "llmain.h" /*@constant int MCEBASESIZE;@*/ # define MCEBASESIZE 8 @@ -199,6 +198,7 @@ macrocache_exists (macrocache s, fileloc fl) return (DNE); } +# ifdef DEADCODE /*@only@*/ cstring macrocache_unparse (macrocache m) { @@ -217,6 +217,7 @@ macrocache_unparse (macrocache m) return (s); } +# endif /* DEADCODE */ /* ** needs to call lex by hand...yuk! diff --git a/src/messageLog.c b/src/messageLog.c index c6bcd33..8265eb6 100644 --- a/src/messageLog.c +++ b/src/messageLog.c @@ -28,6 +28,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int messageLogBASESIZE; @*/ +# define messageLogBASESIZE MIDBASESIZE + /*@only@*/ messageLog messageLog_new (void) { @@ -180,6 +183,7 @@ bool messageLog_add (messageLog s, fileloc fl, cstring mess) return TRUE; } +# ifdef DEADCODE /*@only@*/ cstring messageLog_unparse (messageLog s) { @@ -202,6 +206,7 @@ messageLog_unparse (messageLog s) st = message ("%q ]", st); return st; } +# endif /* DEADCODE */ void messageLog_free (messageLog s) diff --git a/src/metaStateConstraintList.c b/src/metaStateConstraintList.c index 8e1a759..a3bfd96 100644 --- a/src/metaStateConstraintList.c +++ b/src/metaStateConstraintList.c @@ -29,17 +29,14 @@ # include "basic.h" # include "metaStateConstraintList.h" +/*@constant int metaStateConstraintListBASESIZE;@*/ +# define metaStateConstraintListBASESIZE MIDBASESIZE + /* ** Invariant: If any member of the list is metaStateConstraint_undefined, then ** the 0th member is metaStateConstraint_undefined. */ -metaStateConstraintList -metaStateConstraintList_new (void) -{ - return (metaStateConstraintList_undefined); -} - static /*@notnull@*/ /*@only@*/ metaStateConstraintList metaStateConstraintList_newEmpty (void) { @@ -124,6 +121,7 @@ metaStateConstraintList_single (metaStateConstraint el) return metaStateConstraintList_add (res, el); } +# ifdef DEADCODE metaStateConstraint metaStateConstraintList_getFirst (metaStateConstraintList s) { @@ -154,6 +152,7 @@ metaStateConstraintList_unparse (metaStateConstraintList s) st = message ("%q ]", st); return st; } +# endif /* DEADCODE */ void metaStateConstraintList_free (/*@only@*/ metaStateConstraintList s) @@ -165,8 +164,3 @@ metaStateConstraintList_free (/*@only@*/ metaStateConstraintList s) } } - - - - - diff --git a/src/metaStateInfo.c b/src/metaStateInfo.c index a35c52d..e31b0ec 100644 --- a/src/metaStateInfo.c +++ b/src/metaStateInfo.c @@ -182,6 +182,7 @@ void metaStateInfo_setDefaultRefValue (metaStateInfo info, int val) metaStateInfo_setDefaultValueContext (info, MTC_REFERENCE, val); } +# ifdef DEADCODE void metaStateInfo_setDefaultResultValue (metaStateInfo info, int val) { metaStateInfo_setDefaultValueContext (info, MTC_RESULT, val); @@ -191,12 +192,14 @@ void metaStateInfo_setDefaultParamValue (metaStateInfo info, int val) { metaStateInfo_setDefaultValueContext (info, MTC_PARAM, val); } +# endif /* DEADCODE */ int metaStateInfo_getDefaultRefValue (metaStateInfo info) { return metaStateInfo_getDefaultValueContext (info, MTC_REFERENCE); } +# ifdef DEADCODE int metaStateInfo_getDefaultResultValue (metaStateInfo info) { return metaStateInfo_getDefaultValueContext (info, MTC_RESULT); @@ -206,4 +209,5 @@ int metaStateInfo_getDefaultParamValue (metaStateInfo info) { return metaStateInfo_getDefaultValueContext (info, MTC_PARAM); } +# endif /* DEADCODE */ diff --git a/src/misc.c b/src/misc.c index f4717ef..c221079 100644 --- a/src/misc.c +++ b/src/misc.c @@ -69,6 +69,7 @@ int int_log (int x) } /*@-czechfcns@*/ +# ifdef DEADCODE long unsigned int longUnsigned_fromInt (int x) { @@ -76,6 +77,7 @@ longUnsigned_fromInt (int x) return (long unsigned) x; } +# endif /* DEADCODE */ size_t size_fromInt (int x) /*@ensures result==x@*/ { @@ -85,6 +87,7 @@ size_t size_fromInt (int x) /*@ensures result==x@*/ return res; } +# ifdef DEADCODE size_t size_fromLong (long x) /*@ensures result==x@*/ { size_t res = (size_t) x; @@ -92,6 +95,7 @@ size_t size_fromLong (long x) /*@ensures result==x@*/ llassert ((long) res == x); return res; } +# endif /* DEADCODE */ size_t size_fromLongUnsigned (unsigned long x) /*@ensures result==x@*/ { diff --git a/src/modifiesClause.c b/src/modifiesClause.c index 0694556..e3f5388 100644 --- a/src/modifiesClause.c +++ b/src/modifiesClause.c @@ -75,11 +75,13 @@ extern cstring modifiesClause_unparse (modifiesClause node) } } +# ifdef DEADCODE extern sRefSet modifiesClause_getMods (modifiesClause m) { llassert (!m->isnomods); return m->srs; } +# endif /* DEADCODE */ extern sRefSet modifiesClause_takeMods (modifiesClause m) { diff --git a/src/mtContextNode.c b/src/mtContextNode.c index b4998b2..048112f 100644 --- a/src/mtContextNode.c +++ b/src/mtContextNode.c @@ -245,11 +245,13 @@ cstring mtContextNode_unparse (mtContextNode node) } } +# ifdef DEADCODE bool mtContextNode_isClause (mtContextNode n) { llassert (mtContextNode_isDefined (n)); return (n->context == MTC_CLAUSE); } +# endif /* DEADCODE */ bool mtContextNode_isParameter (mtContextNode n) { @@ -281,6 +283,7 @@ bool mtContextNode_isNull (mtContextNode n) return (n->context == MTC_NULL); } +# ifdef DEADCODE void mtContextNode_showRefError (mtContextNode context, sRef sr) { ctype ct; @@ -340,6 +343,5 @@ void mtContextNode_showRefError (mtContextNode context, sRef sr) BADBRANCH; } } - - +# endif /* DEADCODE */ diff --git a/src/mtDeclarationNode.c b/src/mtDeclarationNode.c index a90270b..d995b0d 100644 --- a/src/mtDeclarationNode.c +++ b/src/mtDeclarationNode.c @@ -28,6 +28,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int metaState_error@*/ +# define metaState_error -1 + extern mtDeclarationNode mtDeclarationNode_create (mttok name, mtDeclarationPieces pieces) /*@*/ { mtDeclarationNode res = (mtDeclarationNode) dmalloc (sizeof (*res)); diff --git a/src/mtDeclarationPiece.c b/src/mtDeclarationPiece.c index 3f2da7f..d617c9d 100644 --- a/src/mtDeclarationPiece.c +++ b/src/mtDeclarationPiece.c @@ -152,6 +152,7 @@ extern bool mtDeclarationPiece_matchKind (mtDeclarationPiece p, mtPieceKind kind } } +# ifdef DEADCODE extern mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece node) { llassert (mtDeclarationPiece_isDefined (node)); @@ -161,6 +162,7 @@ extern mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece node) return (mtContextNode) node->node; /*@=abstract@*/ } +# endif /* DEADCODE */ extern mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece node) { @@ -237,6 +239,7 @@ extern mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPi /*@=abstract@*/ } +# ifdef DEADCODE extern mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece node) { llassert (mtDeclarationPiece_isDefined (node)); @@ -246,6 +249,7 @@ extern mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationP return (mtTransferClauseList) node->node; /*@=abstract@*/ } +# endif /* DEADCODE */ extern mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece node) { diff --git a/src/mttok.c b/src/mttok.c index b8739bb..a354153 100644 --- a/src/mttok.c +++ b/src/mttok.c @@ -118,10 +118,12 @@ void mttok_free (mttok t) sfree (t); } +# ifdef DEADCODE bool mttok_isError (mttok t) { return ((t)->tok == MT_ERROR); } +# endif /* DEADCODE */ bool mttok_isIdentifier (mttok t) { diff --git a/src/multiVal.c b/src/multiVal.c index 28ccaea..f26e190 100644 --- a/src/multiVal.c +++ b/src/multiVal.c @@ -145,12 +145,14 @@ char multiVal_forceChar (multiVal m) return m->value.cval; } +# ifdef DEADCODE double multiVal_forceDouble (multiVal m) { llassert (multiVal_isDouble (m)); return m->value.fval; } +# endif /* DEADCODE */ /*@dependent@*/ /*@observer@*/ cstring multiVal_forceString (multiVal m) { diff --git a/src/nameChecks.c b/src/nameChecks.c index 668e93f..8edc220 100644 --- a/src/nameChecks.c +++ b/src/nameChecks.c @@ -1162,8 +1162,7 @@ checkCppName (uentry ue) "typeid", "using", "virtual", "xor", "xor_eq" } ; - if (cstring_isDefined (cstring_bsearch (name, &cppNames[0], - NCPPNAMES))) + if (cstring_bsearch (name, &cppNames[0], NCPPNAMES)) { if (optgenerror2 (FLG_CPPNAMES, FLG_NAMECHECKS, @@ -1227,8 +1226,7 @@ checkAnsiName (uentry ue) return; /* no errors for system files */ } - if (cstring_isDefined (cstring_bsearch (name, &reservedNames[0], - NRESERVEDNAMES))) + if (cstring_bsearch (name, &reservedNames[0], NRESERVEDNAMES)) { hasError |= optgenerror2 (FLG_ISORESERVED, FLG_NAMECHECKS, diff --git a/src/osd.c b/src/osd.c index 7c87a71..466b3f7 100644 --- a/src/osd.c +++ b/src/osd.c @@ -413,7 +413,8 @@ osd_getExePath (cstring path, cstring file, cstring *returnPath) static bool s_tempError = FALSE; -void osd_setTempError (void) +static void osd_setTempError (void) + /*@modifies internalState@*/ { s_tempError = TRUE; } diff --git a/src/programNodeList.c b/src/programNodeList.c index e6d0c70..d1e90c3 100644 --- a/src/programNodeList.c +++ b/src/programNodeList.c @@ -75,6 +75,7 @@ programNodeList_addh (programNodeList s, /*@keep@*/ programNode el) s->nelements++; } +# ifdef DEADCODE /*@only@*/ cstring programNodeList_unparse (programNodeList s) { @@ -96,6 +97,7 @@ programNodeList_unparse (programNodeList s) return st; } +# endif /* DEADCODE */ void programNodeList_free (programNodeList s) diff --git a/src/qual.c b/src/qual.c index 855a13f..d8de411 100644 --- a/src/qual.c +++ b/src/qual.c @@ -97,6 +97,7 @@ extern qual qual_createMetaState (annotationInfo info) return res; } +# ifdef DEADCODE static bool quenum_isValid (int q) { return ((quenum) q >= QU_UNKNOWN @@ -108,6 +109,7 @@ qual qual_fromInt (int q) llassertprint (quenum_isValid (q), ("Invalid qual: %d", q)); return (qual_createPlain ((quenum) q)); } +# endif /* DEADCODE */ cstring qual_unparse (qual q) { diff --git a/src/qualList.c b/src/qualList.c index af641c0..6f94cdf 100644 --- a/src/qualList.c +++ b/src/qualList.c @@ -28,6 +28,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int qualListBASESIZE;@*/ +# define qualListBASESIZE 8 + qualList qualList_new (void) { @@ -202,6 +205,7 @@ qualList_free (/*@only@*/ qualList s) } } +# ifdef DEADCODE /* start modifications */ /* requires: p is defined @@ -217,5 +221,5 @@ bool qualList_hasNullTerminatedQualifier(qualList s) { } /* end modification/s */ - +# endif /* DEADCODE */ diff --git a/src/quantifierNodeList.c b/src/quantifierNodeList.c index c950438..2bd284e 100644 --- a/src/quantifierNodeList.c +++ b/src/quantifierNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int quantifierNodeListBASESIZE;@*/ +# define quantifierNodeListBASESIZE SMALLBASESIZE + /*@only@*/ quantifierNodeList quantifierNodeList_new (void) { @@ -106,6 +109,7 @@ quantifierNodeList_unparse (quantifierNodeList s) return st; } +# ifdef DEADCODE void quantifierNodeList_free (quantifierNodeList s) { @@ -118,3 +122,5 @@ quantifierNodeList_free (quantifierNodeList s) sfree (s->elements); sfree (s); } +# endif /* DEADCODE */ + diff --git a/src/reader.c b/src/reader.c index bbd212d..26637e1 100644 --- a/src/reader.c +++ b/src/reader.c @@ -28,7 +28,7 @@ # include "splintMacros.nf" # include "basic.h" -int reader_getInt (const char **s) +int reader_getInt (char **s) { bool gotOne = FALSE; int i = 0; diff --git a/src/replaceNodeList.c b/src/replaceNodeList.c index 9497d4b..f6642eb 100644 --- a/src/replaceNodeList.c +++ b/src/replaceNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int replaceNodeListBASESIZE;@*/ +# define replaceNodeListBASESIZE SMALLBASESIZE + /*@only@*/ replaceNodeList replaceNodeList_new (void) { @@ -78,6 +81,7 @@ replaceNodeList return s; } +# ifdef DEADCODE /*@only@*/ cstring replaceNodeList_unparse (replaceNodeList s) { @@ -99,6 +103,7 @@ replaceNodeList_unparse (replaceNodeList s) return st; } +# endif /* DEADCODE */ void replaceNodeList_free (replaceNodeList s) diff --git a/src/sRef.c b/src/sRef.c index 9b57647..c438e30 100644 --- a/src/sRef.c +++ b/src/sRef.c @@ -36,8 +36,6 @@ # include "splintMacros.nf" # include "basic.h" -# include "exprChecks.h" -# include "transferChecks.h" # include "sRefTable.h" # include "structNames.h" @@ -108,7 +106,7 @@ extern void sRef_checkCompletelyReasonable (sRef s) /*@*/ } # endif -/*@falsewhennull@*/ bool sRef_isReasonable (sRef s) /*@*/ +static /*@falsewhennull@*/ bool sRef_isReasonable (sRef s) /*@*/ { if (sRef_isValid (s)) { @@ -337,7 +335,9 @@ static void sRef_checkValidAux (sRef s, sRefSet checkedsofar) case SK_CVAR: llassert (s->info->cvar->lexlevel >= 0); - /* llassert (s->info->cvar->lexlevel <= usymtab_getCurrentDepth ()); */ +#if 0 + llassert (s->info->cvar->lexlevel <= usymtab_getCurrentDepth ()); +#endif break; case SK_PARAM: @@ -410,14 +410,13 @@ static void sRef_checkValidAux (sRef s, sRefSet checkedsofar) } #endif -void sRef_checkValid (/*@unused@*/ sRef s) +# if 0 +static /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef s) /*@modifies stderr@*/ { - return; - /* sRefSet checkedsofar = sRefSet_new (); sRef_checkValidAux (s, checkedsofar); - */ } +# endif static /*@dependent@*/ /*@notnull@*/ /*@special@*/ sRef sRef_new (void) @@ -668,11 +667,13 @@ bool sRef_hasAliasInfoLoc (sRef s) && (fileloc_isDefined (s->definfo->loc))); } +# ifdef DEADCODE /*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef s) { return (sRef_isReasonable (s) && (s->expinfo != NULL) && (fileloc_isDefined (s->expinfo->loc))); } +# endif /* DEADCODE */ # if 0 static /*@observer@*/ /*@unused@*/ stateInfo sRef_getInfo (sRef s, cstring key) @@ -2100,11 +2101,13 @@ sRef_realSame (sRef s1, sRef s2) BADEXIT; } +#ifdef DEADCODE bool sRef_sameObject (sRef s1, sRef s2) { return (s1 == s2); } +#endif /* ** same is similar to similar, but not quite the same. @@ -4630,7 +4633,8 @@ sRef_makeUnsafe (sRef s) valueTable_unparse (s->state))); } -/*@unused@*/ cstring sRef_unparseDeep (sRef s) +#if 0 +cstring sRef_unparseDeep (sRef s) { cstring st = cstring_undefined; @@ -4646,6 +4650,7 @@ sRef_makeUnsafe (sRef s) return st; } +#endif /*@only@*/ cstring sRef_unparseState (sRef s) { @@ -5529,6 +5534,7 @@ void sRef_setNullState (sRef s, nstate n, fileloc loc) } } +# ifdef DEADCODE void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc) { switch (b.bufstate) { @@ -5550,6 +5556,7 @@ void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@u * setNullStateInnerComplete. */ } +# endif /* DEADCODE */ void sRef_setNullStateInnerComplete (sRef s, nstate n, fileloc loc) { @@ -5984,11 +5991,13 @@ bool sRef_isConst (sRef s) return (s->kind == SK_CONST); } +# ifdef DEADCODE bool sRef_isObject (sRef s) { PREDTEST (sRef_isObject, s); return (s->kind == SK_OBJECT); } +# endif /* DEADCODE */ bool sRef_isExternal (sRef s) { @@ -6095,7 +6104,9 @@ void sRef_free (/*@only@*/ sRef s) { DPRINTF (("Free sref: [%p]", s)); +# if 0 sRef_checkValid (s); +# endif multiVal_free (s->val); /* evans 2002-07-12 */ @@ -9250,10 +9261,7 @@ static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef s) ret->fname = s->info->fname; break; - case SK_RESULT: - case SK_CONST: - case SK_TYPE: - case SK_UNKNOWN: + default: llassertprint (s->info == NULL, ("s = %s", sRef_unparse (s))); ret = NULL; break; @@ -9397,10 +9405,7 @@ static void res->info->fname = other->info->fname; break; - case SK_CONST: - case SK_TYPE: - case SK_UNKNOWN: - case SK_RESULT: + default: llassert (res->info == NULL); break; } @@ -9444,13 +9449,7 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s) sfree (s->info->conj); break; - case SK_UNCONSTRAINED: - case SK_SPECIAL: - case SK_CONST: - case SK_NEW: - case SK_TYPE: - case SK_UNKNOWN: - case SK_RESULT: + default: break; } @@ -9623,6 +9622,7 @@ cstring sRef_nullMessage (sRef s) BADEXIT; } +# ifdef DEADCODE /*@observer@*/ cstring sRef_ntMessage (sRef s) { llassert (sRef_isReasonable (s)); @@ -9637,7 +9637,7 @@ cstring sRef_nullMessage (sRef s) } BADEXIT; } - +# endif /* DEADCODE */ sRef sRef_fixResultType (/*@returned@*/ sRef s, ctype typ, uentry ue) @@ -9789,10 +9789,12 @@ bool sRef_isKeep (sRef s) return (sRef_isReasonable (s) && (s->aliaskind == AK_KEEP)); } +# ifdef DEADCODE bool sRef_isTemp (sRef s) { return (sRef_isReasonable (s) && alkind_isTemp (s->aliaskind)); } +# endif /* DEADCODE */ bool sRef_isLocalState (sRef s) { @@ -10059,6 +10061,7 @@ bool sRef_definitelyNullAltContext (sRef s) } +# ifdef DEADCODE /* start modifications */ struct s_bbufinfo sRef_getNullTerminatedState (sRef p_s) { struct s_bbufinfo BUFSTATE_UNKNOWN; @@ -10070,6 +10073,7 @@ struct s_bbufinfo sRef_getNullTerminatedState (sRef p_s) { return p_s->bufinfo; return BUFSTATE_UNKNOWN; } +# endif /* DEADCODE */ void sRef_setNullTerminatedState(sRef p_s) { if(sRef_isReasonable (p_s)) { diff --git a/src/sRefList.c b/src/sRefList.c deleted file mode 100644 index ba277aa..0000000 --- a/src/sRefList.c +++ /dev/null @@ -1,143 +0,0 @@ -/* -** Splint - annotation-assisted static program checker -** Copyright (C) 1994-2003 University of Virginia, -** Massachusetts Institute of Technology -** -** This program is free software; you can redistribute it and/or modify it -** under the terms of the GNU General Public License as published by the -** Free Software Foundation; either version 2 of the License, or (at your -** option) any later version. -** -** This program is distributed in the hope that it will be useful, but -** WITHOUT ANY WARRANTY; without even the implied warranty of -** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -** General Public License for more details. -** -** The GNU General Public License is available from http://www.gnu.org/ or -** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, -** MA 02111-1307, USA. -** -** For information on splint: info@splint.org -** To report a bug: splint-bug@splint.org -** For more information: http://www.splint.org -*/ -/* -** sRefList.c (from slist_template.c) -*/ - -# include "splintMacros.nf" -# include "basic.h" - -sRefList -sRefList_new (void) -{ - return sRefList_undefined; -} - -static /*@only@*/ /*@notnull@*/ sRefList -sRefList_newEmpty (void) -{ - sRefList s = (sRefList) dmalloc (sizeof (*s)); - - s->nelements = 0; - s->nspace = sRefListBASESIZE; - s->elements = (sRef *) dmalloc (sizeof (*s->elements) * sRefListBASESIZE); - - return (s); -} - -/*@only@*/ sRefList sRefList_single (sRef el) -{ - sRefList res = sRefList_newEmpty (); - res = sRefList_add (res, el); - return res; -} - -static void -sRefList_grow (/*@notnull@*/ sRefList s) -{ - int i; - sRef *oldelements = s->elements; - - s->nspace += sRefListBASESIZE; - - s->elements = (sRef *) dmalloc (sizeof (*s->elements) * (s->nelements + s->nspace)); - - for (i = 0; i < s->nelements; i++) - { - s->elements[i] = oldelements[i]; - } - - sfree (oldelements); -} - -/*@notnull@*/ sRefList sRefList_add (sRefList s, sRef el) -{ - if (sRefList_isUndefined (s)) - { - s = sRefList_newEmpty (); - } - - if (s->nspace <= 0) - sRefList_grow (s); - - s->nspace--; - s->elements[s->nelements] = el; - s->nelements++; - - return (s); -} - -sRefList sRefList_copy (sRefList s) -{ - sRefList t = sRefList_new (); - - sRefList_elements (s, current) - { - t = sRefList_add (t, sRef_copy (current)); - } end_sRefList_elements; - - return t; -} - -/*@only@*/ cstring -sRefList_unparse (sRefList s) -{ - int i; - cstring st = cstring_undefined; - - if (sRefList_isDefined (s)) - { - for (i = 0; i < sRefList_size (s); i++) - { - if (i == 0) - { - st = message ("%q%q ", st, sRef_unparse (s->elements[i])); - } - else - st = message ("%q%q ", st, sRef_unparse (s->elements[i])); - } - } - - return st; -} - -int sRefList_size (sRefList s) -{ - if (sRefList_isUndefined (s)) return 0; - return s->nelements; -} - -void -sRefList_free (/*@only@*/ sRefList s) -{ - if (sRefList_isDefined (s)) - { - sfree (s->elements); - sfree (s); - } -} - - - - diff --git a/src/sRefSet.c b/src/sRefSet.c index 8f24218..381c026 100644 --- a/src/sRefSet.c +++ b/src/sRefSet.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int sRefSetBASESIZE;@*/ +# define sRefSetBASESIZE SMALLBASESIZE + sRefSet sRefSet_new (void) { @@ -578,11 +581,13 @@ sRefSet_hasRealElement (sRefSet s) return FALSE; } +#ifdef DEADCODE bool sRefSet_containsSameObject (sRefSet s, sRef el) { return (sRefSet_isElementCompare (sRef_sameObject, s, el)); } +#endif bool sRefSet_isSameMember (sRefSet s, sRef el) @@ -936,6 +941,7 @@ sRefSet sRefSet_fetchKnown (sRefSet s, int i) return t; } +# ifdef DEADCODE int sRefSet_compare (sRefSet s1, sRefSet s2) { sRefSet_allElements (s1, el) @@ -956,6 +962,7 @@ int sRefSet_compare (sRefSet s1, sRefSet s2) return 0; } +# endif /* DEADCODE */ bool sRefSet_equal (sRefSet s1, sRefSet s2) { diff --git a/src/sRefTable.c b/src/sRefTable.c index 292ab89..823a3a0 100644 --- a/src/sRefTable.c +++ b/src/sRefTable.c @@ -33,6 +33,9 @@ # include "basic.h" # include "sRefTable.h" +/*@constant int sRefTableBASESIZE; @*/ +# define sRefTableBASESIZE HUGEBASESIZE + static /*@notnull@*/ /*@only@*/ sRefTable sRefTable_new (void) { @@ -113,6 +116,7 @@ sRefTable_clear (sRefTable s) # endif } +# ifdef DEADCODE static int sRefTable_size (sRefTable s) { if (sRefTable_isNull (s)) return 0; @@ -137,6 +141,7 @@ sRefTable_unparse (sRefTable s) } return st; } +# endif /* DEADCODE */ void sRefTable_free (/*@only@*/ sRefTable s) diff --git a/src/shift.c b/src/shift.c index d423aa2..b6646cc 100644 --- a/src/shift.c +++ b/src/shift.c @@ -44,8 +44,6 @@ static o_ltoken Shifts[SHIFTMAX]; static int shiftIndex; -static bool Parsing_LSLinit = TRUE; - static bool LSLGenIsEmptyShiftStack (void) { @@ -96,9 +94,3 @@ LSLGenTopPopShiftStack (void) /*@=retalias@*/ /*@=dependenttrans@*/ } -void -LSLGenInit (bool LSLParse) -{ - Parsing_LSLinit = LSLParse; -} - diff --git a/src/sigNodeSet.c b/src/sigNodeSet.c index 1db051b..46cc84a 100644 --- a/src/sigNodeSet.c +++ b/src/sigNodeSet.c @@ -33,6 +33,9 @@ # include "basic.h" # include "intSet.h" +/*@constant int sigNodeSetBASESIZE;@*/ +# define sigNodeSetBASESIZE MIDBASESIZE + static bool sigNodeSet_member (sigNodeSet p_s, sigNode p_el); /*@only@*/ sigNodeSet @@ -130,6 +133,7 @@ sigNodeSet_member (sigNodeSet s, sigNode el) } } +# if 0 /*@only@*/ cstring sigNodeSet_unparse (sigNodeSet s) { @@ -151,6 +155,7 @@ sigNodeSet_unparse (sigNodeSet s) return st; } +# endif /*@only@*/ cstring sigNodeSet_unparseSomeSigs (sigNodeSet s) diff --git a/src/sort.c b/src/sort.c index 9783375..313fd3e 100644 --- a/src/sort.c +++ b/src/sort.c @@ -38,7 +38,6 @@ # include "splintMacros.nf" # include "basic.h" # include "llgrammar.h" -# include "lclscan.h" /*@+ignorequals@*/ @@ -118,7 +117,6 @@ sort g_sortFloat; sort g_sortDouble; sort g_sortCstring; -static sort sort_void; static sort char_obj_ptrSort; static sort char_obj_ArrSort; @@ -1922,7 +1920,7 @@ sort_init (void) lsymbol_fromChars ("int")); g_sortChar = sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("char")); - sort_void = sort_makeLiteralSort (ltoken_undefined, + (void) sort_makeLiteralSort (ltoken_undefined, lsymbol_fromChars ("void")); /* g_sortCstring is char__Vec, for C strings eg: "xyz" */ @@ -2053,14 +2051,6 @@ static sort sort_enterNewForce (sortNode s) /*@-globstate@*/ return (sor); /*@=globstate@*/ } -void -sort_printStats (void) -{ - /* only for debugging */ - printf ("sortTableSize = %d; sortTableAlloc = %d\n", sortTableSize, - sortTableAlloc); -} - sortNode sort_lookup (sort sor) { diff --git a/src/sortSet.c b/src/sortSet.c index 9678697..afc4dde 100644 --- a/src/sortSet.c +++ b/src/sortSet.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int sortSetBASESIZE;@*/ +# define sortSetBASESIZE MIDBASESIZE + sortSet sortSet_new (void) { sortSet s = (sortSet) dmalloc (sizeof (*s)); @@ -140,11 +143,13 @@ sortSet_member (sortSet s, sort el) return FALSE; } +# ifdef DEADCODE /*@only@*/ cstring sortSet_unparse (sortSet s) { return (message ("{ %q }", sortSet_unparseClean (s))); } +# endif /* DEADCODE */ /*@only@*/ cstring sortSet_unparseClean (sortSet s) diff --git a/src/sortSetList.c b/src/sortSetList.c index 23f64fb..6ca8f3e 100644 --- a/src/sortSetList.c +++ b/src/sortSetList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int sortSetListBASESIZE;@*/ +# define sortSetListBASESIZE (8) + /*@only@*/ sortSetList sortSetList_new (void) { @@ -112,6 +115,7 @@ sortSetList_current (sortSetList s) return (s->elements[s->current]); } +# ifdef DEADCODE /*@only@*/ cstring sortSetList_unparse (sortSetList s) { @@ -129,6 +133,7 @@ sortSetList_unparse (sortSetList s) st = message ("%q]", st); return st; } +# endif /* DEADCODE */ void sortSetList_free (sortSetList s) diff --git a/src/stateClause.c b/src/stateClause.c index bfe429e..b8154c3 100644 --- a/src/stateClause.c +++ b/src/stateClause.c @@ -111,10 +111,12 @@ bool stateClause_isAfter (stateClause cl) return (cl->state == TK_AFTER || cl->state == TK_BOTH); } +# ifdef DEADCODE bool stateClause_isEnsures (stateClause cl) { return (cl->state == TK_AFTER); } +# endif /* DEADCODE */ bool stateClause_isQual (stateClause cl) { @@ -658,22 +660,27 @@ cstring stateClause_unparse (stateClause s) stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs))); } -stateClause stateClause_createDefines (sRefSet s) +static stateClause stateClause_createDefines (/*@only@*/ sRefSet s) { return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s)); } -stateClause stateClause_createUses (sRefSet s) +static stateClause stateClause_createUses (/*@only@*/ sRefSet s) { return (stateClause_createRaw (TK_BOTH, SP_USES, s)); } -stateClause stateClause_createSets (sRefSet s) +static stateClause stateClause_createSets (/*@only@*/ sRefSet s) { return (stateClause_createRaw (TK_BOTH, SP_SETS, s)); } -stateClause stateClause_createReleases (sRefSet s) +static stateClause stateClause_createAllocates (/*@only@*/ sRefSet s) +{ + return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s)); +} + +static stateClause stateClause_createReleases (/*@only@*/ sRefSet s) { return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s)); } @@ -700,11 +707,6 @@ stateClause stateClause_createPlain (lltok tok, sRefSet s) BADBRANCHRET (stateClause_createUses (sRefSet_undefined)); } -stateClause stateClause_createAllocates (sRefSet s) -{ - return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s)); -} - bool stateClause_matchKind (stateClause s1, stateClause s2) { return (s1->state == s2->state && s1->kind == s2->kind diff --git a/src/stateClauseList.c b/src/stateClauseList.c index fe5bf2e..8c58c3e 100644 --- a/src/stateClauseList.c +++ b/src/stateClauseList.c @@ -28,6 +28,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int stateClauseListBASESIZE;@*/ +# define stateClauseListBASESIZE MIDBASESIZE + static /*@notnull@*/ stateClauseList stateClauseList_new (void) { stateClauseList s = (stateClauseList) dmalloc (sizeof (*s)); @@ -204,6 +207,7 @@ stateClauseList stateClauseList_undump (char **s) return pn; } +# ifdef DEADCODE int stateClauseList_compare (stateClauseList s1, stateClauseList s2) { if (stateClauseList_isUndefined (s1) @@ -223,7 +227,8 @@ int stateClauseList_compare (stateClauseList s1, stateClauseList s2) } } } - +# endif /* DEADCODE */ + static /*@exposed@*/ sRefSet stateClauseList_getClause (stateClauseList s, stateClause k) { diff --git a/src/stateInfo.c b/src/stateInfo.c index 24dc33e..a20def5 100644 --- a/src/stateInfo.c +++ b/src/stateInfo.c @@ -26,6 +26,10 @@ # include "basic.h" static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ; +static /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeRefLoc ( + /*@exposed@*/ sRef p_ref, fileloc p_loc, stateAction p_action) /*@*/ ; + + void stateInfo_free (/*@only@*/ stateInfo a) { @@ -221,23 +225,10 @@ stateInfo_currentLoc (void) /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeLoc (fileloc loc, stateAction action) { - stateInfo ret = (stateInfo) dmalloc (sizeof (*ret)); - - if (fileloc_isUndefined (loc)) { - ret->loc = fileloc_copy (g_currentloc); - } else { - ret->loc = fileloc_copy (loc); - } - - ret->ref = sRef_undefined; - ret->action = action; - ret->previous = stateInfo_undefined; - - DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret))); - return ret; + return stateInfo_makeRefLoc (sRef_undefined, loc, action); } -/*@only@*/ /*@notnull@*/ stateInfo +static /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action) /*@post:isnull result->previous@*/ { @@ -253,6 +244,7 @@ stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action) ret->action = action; ret->previous = stateInfo_undefined; + DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret))); return ret; } @@ -290,6 +282,7 @@ stateAction stateAction_fromNState (nstate ns) { case NS_ERROR: case NS_UNKNOWN: + default: return SA_UNKNOWN; case NS_NOTNULL: case NS_MNOTNULL: @@ -391,11 +384,7 @@ stateAction stateAction_fromSState (sstate ss) case SS_HOFFA: return SA_PKILLED; case SS_SPECIAL: return SA_DECLARED; case SS_RELDEF: return SA_DECLARED; - case SS_FIXED: - case SS_UNDEFGLOB: - case SS_KILLED: - case SS_UNDEFKILLED: - case SS_LAST: + default: llbug (message ("Unexpected sstate: %s", sstate_unparse (ss))); /*@notreached@*/ return SA_UNKNOWN; } @@ -446,10 +435,8 @@ static /*@observer@*/ cstring stateAction_unparse (stateAction sa) case SA_BECOMESNULL: return cstring_makeLiteralTemp ("becomes null"); case SA_BECOMESNONNULL: return cstring_makeLiteralTemp ("becomes non-null"); case SA_BECOMESPOSSIBLYNULL: return cstring_makeLiteralTemp ("becomes possibly null"); + default: BADBRANCHRET (cstring_undefined); } - - DPRINTF (("Bad state action: %d", sa)); - BADBRANCH; } void stateInfo_display (stateInfo s, cstring sname) diff --git a/src/stateValue.c b/src/stateValue.c index 873ba4b..e2e71db 100644 --- a/src/stateValue.c +++ b/src/stateValue.c @@ -56,6 +56,7 @@ stateValue stateValue_copy (stateValue s) { return res; } +# ifdef DEADCODE bool stateValue_sameValue (stateValue s1, stateValue s2) { if (stateValue_isDefined (s1) && stateValue_isDefined (s2)) @@ -67,6 +68,7 @@ bool stateValue_sameValue (stateValue s1, stateValue s2) return !stateValue_isDefined (s1) && !stateValue_isDefined (s2); } } +# endif /* DEADCODE */ extern cstring stateValue_unparse (stateValue s) { @@ -80,6 +82,7 @@ cstring stateValue_unparse (stateValue s) { } } +# ifdef DEADCODE void stateValue_updateValue (stateValue s, int value, stateInfo info) { llassert (stateValue_isDefined (s)); @@ -92,6 +95,7 @@ void stateValue_updateValue (stateValue s, int value, stateInfo info) DPRINTF (("update state value: %s", stateValue_unparse (s))); } +# endif /* DEADCODE */ void stateValue_updateValueLoc (stateValue s, int value, fileloc loc) { @@ -103,7 +107,8 @@ void stateValue_updateValueLoc (stateValue s, int value, fileloc loc) s->value = value; s->info = stateInfo_updateLoc (s->info, SA_CHANGED, loc); } - + +# ifdef DEADCODE void stateValue_update (stateValue res, stateValue val) { llassert (stateValue_isDefined (res)); @@ -114,6 +119,7 @@ void stateValue_update (stateValue res, stateValue val) DPRINTF (("update state: %s", stateValue_unparse (res))); } +# endif /* DEADCODE */ void stateValue_show (stateValue s, metaStateInfo msinfo) { diff --git a/src/symtable.c b/src/symtable.c index 477f296..63a0f75 100644 --- a/src/symtable.c +++ b/src/symtable.c @@ -43,7 +43,6 @@ # include "splintMacros.nf" # include "basic.h" # include "lslparse.h" -# include "lclscan.h" # include "lclsyntable.h" # include "llgrammar.h" @@ -142,7 +141,9 @@ static /*@only@*/ varInfo varInfo_copy (varInfo v) void symtable_free (symtable stable) { - /* symtable_printStats (stable); */ +#if 0 + symtable_printStats (stable); +#endif idTable_free (stable->idTable); symHashTable_free (stable->hTable); @@ -1935,7 +1936,6 @@ symHashTable_count (symHashTable * t) return (t->count); } -#endif static void symHashTable_printStats (symHashTable * t) @@ -2007,6 +2007,7 @@ symtable_printStats (symtable s) printf ("idTable size = %d; allocated = %d\n", s->idTable->size, s->idTable->allocated); } +#endif /*@only@*/ cstring tagKind_unparse (tagKind k) diff --git a/src/traitRefNodeList.c b/src/traitRefNodeList.c index 5099f94..a40eef6 100644 --- a/src/traitRefNodeList.c +++ b/src/traitRefNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int traitRefNodeListBASESIZE;@*/ +# define traitRefNodeListBASESIZE SMALLBASESIZE + /*@only@*/ traitRefNodeList traitRefNodeList_new (void) { @@ -77,6 +80,7 @@ traitRefNodeList_add (traitRefNodeList s, /*@only@*/ traitRefNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring traitRefNodeList_unparse (traitRefNodeList s) { @@ -96,6 +100,7 @@ traitRefNodeList_unparse (traitRefNodeList s) return (st); } +# endif /* DEADCODE */ void traitRefNodeList_free (traitRefNodeList s) diff --git a/src/typeNameNodeList.c b/src/typeNameNodeList.c index 67f2803..d58ce18 100644 --- a/src/typeNameNodeList.c +++ b/src/typeNameNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int typeNameNodeListBASESIZE;@*/ +# define typeNameNodeListBASESIZE SMALLBASESIZE + typeNameNodeList typeNameNodeList_new (void) { typeNameNodeList s = (typeNameNodeList) dmalloc (sizeof (*s)); @@ -77,6 +80,7 @@ typeNameNodeList_add (typeNameNodeList s, typeNameNode el) return s; } +# ifdef DEADCODE /*@only@*/ cstring typeNameNodeList_unparse (typeNameNodeList s) { @@ -97,6 +101,7 @@ typeNameNodeList_unparse (typeNameNodeList s) } end_typeNameNodeList_elements; return (st); } +# endif /* DEADCODE */ void typeNameNodeList_free (typeNameNodeList s) diff --git a/src/uentry.c b/src/uentry.c index 8c5b8be..6d6b644 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -1495,6 +1495,7 @@ static void uentry_addStateClause (/*@notnull@*/ uentry ue, stateClause sc) /* Will call checkAll to check later... */ } +# ifdef DEADCODE void uentry_setStateClauseList (uentry ue, stateClauseList clauses) { llassert (uentry_isFunction (ue)); @@ -1505,6 +1506,7 @@ void uentry_setStateClauseList (uentry ue, stateClauseList clauses) stateClauseList_checkAll (ue); DPRINTF (("checked clauses: %s", uentry_unparseFull (ue))); } +# endif /* DEADCODE */ /* ** Used for @modifies@ @endmodifies@ syntax. @@ -4121,6 +4123,7 @@ uentry_equiv (uentry p1, uentry p2) } } +# if 0 int uentry_xcomparealpha (uentry *p1, uentry *p2) { @@ -4135,6 +4138,7 @@ uentry_xcomparealpha (uentry *p1, uentry *p2) return res; } +# endif int uentry_xcompareuses (uentry *p1, uentry *p2) @@ -4759,13 +4763,6 @@ static uentry return (e); } -void uentry_markFree (/*@unused@*/ /*@owned@*/ uentry u) -{ - /* should save u */ -/*@-mustfree@*/ -} -/*@=mustfree@*/ - /*@only@*/ uentry uentry_undump (ekind kind, fileloc loc, char **s) { @@ -5054,6 +5051,7 @@ uentry_undump (ekind kind, fileloc loc, char **s) llcontbuglit ("uentry_undump: elips marker"); ue = uentry_undefined; break; + BADDEFAULT; } } @@ -5391,7 +5389,9 @@ uentry_unparseFull (uentry v) (int) v->used); DPRINTF (("sref: [%p]", v->sref)); DPRINTF (("sref: %s", sRef_unparseDebug (v->sref))); - /* DPRINTF (("sref: %s", sRef_unparseDeep (v->sref))); */ +#if 0 + DPRINTF (("sref: %s", sRef_unparseDeep (v->sref))); +#endif } else if (uentry_isConstant (v)) { @@ -5809,6 +5809,7 @@ uentry_getMods (uentry l) else { BADBRANCH; + return sRefSet_undefined; } } @@ -7505,6 +7506,7 @@ static cstring fcnErrName (uentry ue) return (cstring_makeLiteralTemp (uentry_isFunction (ue) ? "to return" : "as")); } +# ifdef DEADCODE extern /*@observer@*/ cstring uentry_checkedName (uentry ue) { if (uentry_isVar (ue)) @@ -7516,6 +7518,7 @@ extern /*@observer@*/ cstring uentry_checkedName (uentry ue) return (cstring_makeLiteralTemp ("")); } } +# endif /* DEADCODE */ static cstring checkedName (chkind checked) { @@ -11417,6 +11420,7 @@ bool uentry_hasBufStateInfo (uentry ue) return (ue->info->var->bufinfo != NULL); } +# ifdef DEADCODE bool uentry_isNullTerminated (uentry ue) { llassert (uentry_hasBufStateInfo (ue)); @@ -11437,6 +11441,7 @@ bool uentry_isNotNullTerminated (uentry ue) llassert (ue->info->var->bufinfo != NULL); return (ue->info->var->bufinfo->bufstate == BB_NOTNULLTERMINATED); } +# endif /* DEADCODE */ # ifdef DEBUGSPLINT diff --git a/src/usymtab.c b/src/usymtab.c index 50a20b5..c990888 100644 --- a/src/usymtab.c +++ b/src/usymtab.c @@ -111,10 +111,12 @@ static void usymtab_freeAux (/*@only@*/ usymtab p_u) /*@globals globtab, utab, filetab@*/ /*@modifies p_u@*/ ; +# if 0 extern int usymtab_getCurrentDepth (void) /*@globals utab@*/ { return utab->lexlevel; } +# endif static void usymtab_freeLevel (/*@notnull@*/ /*@only@*/ usymtab p_u) @@ -1711,18 +1713,18 @@ usymtab_prepareDump (void) oldtab = usymtab_shallowCopy (utab); +# if 0 /* ** alpha compare - make sure order is same on different platforms ** error messages appear in same order */ - /* qsort (utab->entries, (size_t)utab->nentries, sizeof (*utab->entries), (int (*)(const void *, const void *)) uentry_xcomparealpha); usymtab_rehash (utab); - */ +# endif /* DPRINTF (("After rehash:")); @@ -2011,7 +2013,7 @@ void usymtab_load (FILE *f) while ((c = *s) != '\0' && (c !='\n')) { - if (c != ' ' || c != '\t') + if (!(c == ' ' || c == '\t')) { llbuglit ("Junk in load file"); } @@ -5433,6 +5435,7 @@ usymtab_freeAux (/*@only@*/ usymtab u) /*@=branchstate@*/ } +# if 0 void usymtab_free (void) /*@globals killed utab, globtab, filetab@*/ /*@modifies utab@*/ @@ -5442,6 +5445,7 @@ void usymtab_free (void) utab = usymtab_undefined; /*@-globstate@*/ } /*@=globstate@*/ /* Splint cannot tell that utab is killed */ +# endif static int usymtab_lexicalLevel (void) /*@globals utab@*/ { @@ -5774,11 +5778,13 @@ void usymtab_addForceMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al) } } +# ifdef DEADCODE void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef s, /*@exposed@*/ sRef al) /*@modifies utab@*/ { utab->aliases = aliasTable_addMustAlias (utab->aliases, s, al); } +# endif /* DEADCODE */ void usymtab_clearAlias (sRef s) /*@modifies utab, s@*/ diff --git a/src/usymtab_interface.c b/src/usymtab_interface.c index 16a4269..549c5a9 100644 --- a/src/usymtab_interface.c +++ b/src/usymtab_interface.c @@ -33,9 +33,6 @@ # include "splintMacros.nf" # include "basic.h" -# include "lslparse.h" -# include "lclscan.h" -# include "lclsyntable.h" # include "llgrammar.h" # include "usymtab_interface.h" # include "structNames.h" diff --git a/src/varDeclarationNodeList.c b/src/varDeclarationNodeList.c index b88276c..68e1b00 100644 --- a/src/varDeclarationNodeList.c +++ b/src/varDeclarationNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int varDeclarationNodeListBASESIZE;@*/ +# define varDeclarationNodeListBASESIZE SMALLBASESIZE + varDeclarationNodeList varDeclarationNodeList_new (void) { varDeclarationNodeList s = (varDeclarationNodeList) dmalloc (sizeof (*s)); @@ -75,6 +78,7 @@ varDeclarationNodeList_addh (varDeclarationNodeList s, /*@keep@*/ varDeclaration s->nelements++; } +# ifdef DEADCODE /*@only@*/ cstring varDeclarationNodeList_unparse (varDeclarationNodeList s) { @@ -91,6 +95,7 @@ varDeclarationNodeList_unparse (varDeclarationNodeList s) return st; } +# endif /* DEADCODE */ void diff --git a/src/varNodeList.c b/src/varNodeList.c index b1b35ef..b116b54 100644 --- a/src/varNodeList.c +++ b/src/varNodeList.c @@ -32,6 +32,9 @@ # include "splintMacros.nf" # include "basic.h" +/*@constant int varNodeListBASESIZE;@*/ +# define varNodeListBASESIZE SMALLBASESIZE + varNodeList varNodeList_new (void) { varNodeList s = (varNodeList) dmalloc (sizeof (*s)); @@ -111,6 +114,7 @@ varNodeList_unparse (varNodeList s) return st; } +# ifdef DEADCODE void varNodeList_free (varNodeList s) { @@ -123,6 +127,7 @@ varNodeList_free (varNodeList s) sfree (s->elements); sfree (s); } +# endif /* DEADCODE */ varNodeList varNodeList_copy (varNodeList s) -- 2.11.4.GIT