X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/bf92e32cf4958be7a9035826b51d0ea8bba57ded..920a3797c23377bfb7332b0c11bda1d708cabb72:/src/Headers/constraint.h diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 12a52a6..9addd22 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -1,19 +1,6 @@ -typedef union constraintTermValue_ -{ - constraintExpr constrExpr; - exprNode expr; - sRef sref; - int intlit; -} constraintTermValue; - - -typedef enum -{ - EXPRNODE, SREF, - CONSTRAINTEXPR, - INTLITERAL -} constraintTermType; +#ifndef __constraint_h__ +#define __constraint_h__ typedef enum { @@ -21,106 +8,140 @@ typedef enum } arithType; -typedef enum -{ - //BUFFSIZE, STRINGLEN, - VALUE, CALLSAFE, - MAXSET, MINSET, MAXREAD, MINREAD, - NULLTERMINATED, - UNDEFINED -} -constraintType; - -typedef enum -{ - PLUS, - MINUS -} -constraintExprOp; - - -struct _constraintTerm { - constraintType constrType; - fileloc loc; - constraintTermValue value; - constraintTermType kind; -}; - -abst_typedef struct _constraintTerm * constraintTerm; - -struct constraintExpr_ { - - constraintTerm term; - constraintExprOp op; - struct constraintExpr_ * expr; -}; -# define constraintExpr_undefined ((constraintExpr)NULL) - - -//abst_typedef struct constr_ * constr; - - struct _constraint { constraint orig; + constraint or; + bool fcnPre; constraintExpr lexpr; arithType ar; constraintExpr expr; bool post; + /*@kept@*/ exprNode generatingExpr; } ; -//constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind); +/*@constant null constraint constraint_undefined; @*/ + +# define constraint_undefined ((constraint)NULL) + +extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ; +extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ; +extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ; + +# define constraint_isDefined(e) ((e) != constraint_undefined) +# define constraint_isUndefined(e) ((e) == constraint_undefined) +# define constraint_isError(e) ((e) == constraint_undefined) -constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); +extern void constraint_free (/*@only@*/ constraint c); -constraint constraint_makeInc_Op (exprNode p_e1); +//constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); /*@i22*/ /*@-czechfcns*/ -bool constraint_resolve (/*@unused@*/ constraint c); + +///*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) +// /*@post:isnull result->expr@*/ +// /*@post:notnull result->t1@*/ +// /*@defines result->expr, result->t1, result->c1@, result->op*/; -/*@out@*/ constraintTerm new_constraintTermExpr (void); -constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e); +extern /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); -constraintTerm intLit_makeConstraintTerm (int p_i); +extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); -/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) - /*@post:isnull result->expr@*/ - /*@post:notnull result->t1@*/ - /*@defines result->expr, result->t1, result->c1@, result->op*/; - -constraintExpr makeConstraintExprIntlit (int p_i); +extern /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); + +extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); + +extern void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/; + +extern /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c); + +extern bool fileloc_closer (/*@observer@*/ fileloc loc1, /*@observer@*/ fileloc loc2, /*@observer@*/ fileloc loc3) /*@*/; + +extern /*@only@*/ cstring arithType_print (arithType ar) /*@*/; + +extern /*@only@*/ fileloc constraint_getFileloc (constraint c); +extern /*@only@*/ cstring constraint_print (constraint c) /*@*/; + +extern /*@only@*/ constraint constraint_makeWriteSafeInt (exprNode po, int ind); + +extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/; + +extern /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint); + +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint); -/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); +extern constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/; +extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, + exprNodeList arglist); +extern /*@only@*/ cstring constraint_printDetailed (constraint c); -constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); +extern /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); +/*drl add 11/28/2000 */ +extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind); +extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef s, int ind); +/*drl add 11/26/2000 */ +extern void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc); -constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition, + exprNodeList arglist); -constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint); -cstring constraintType_print (constraintType c1); +extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size); -constraint constraint_copy (constraint c); +extern /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall); -constraintExpr makePostOpInc (exprNode t1); +extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer); +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint); +extern bool constraint_search (constraint c, constraintExpr old); -cstring constraintTerm_print (constraintTerm term); +extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r); -cstring arithType_print (arithType ar); +extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e); -cstring constraintExpr_print (constraintExpr ex); +extern bool constraint_hasMaxSet(constraint c); + +/*from constraintGenreation.c*/ +extern void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint); + +extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e); +extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e); + +extern constraint constraint_togglePost (/*@returned@*/ constraint c); +extern bool constraint_same (constraint c1, constraint c2) ; + +/*@only@*/ cstring constraint_printOr (constraint c) /*@*/; +extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ; +extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ; +extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, exprNode p_e) ; + +extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ; +constraint constraint_togglePostOrig (/*@returned@*/ constraint c); + +bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c); + +constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint); + +constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint); + +/*@only@*/ constraint constraint_undump (FILE *f); + +void constraint_dump (/*@observer@*/ constraint c, FILE *f); -cstring constraint_print (constraint c); /*@=czechfcns*/ -#warning take this out -#include "constraintList.h" +//#warning take this out + +#include "constraintResolve.h" +#include "constraintOutput.h" -#include "constraintTerm.h" +#else +#error Multiple include +#endif