X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/6e88de2d1b326c7ad00227131afb5c2a002735bb..920a3797c23377bfb7332b0c11bda1d708cabb72:/src/Headers/constraint.h diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 22b9500..9addd22 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -11,11 +11,12 @@ arithType; struct _constraint { constraint orig; constraint or; + bool fcnPre; constraintExpr lexpr; arithType ar; constraintExpr expr; bool post; - exprNode generatingExpr; + /*@kept@*/ exprNode generatingExpr; } ; /*@constant null constraint constraint_undefined; @*/ @@ -24,106 +25,113 @@ struct _constraint { extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ; extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ; -extern /*@truenull@*/ bool constraint_isError (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 makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); +extern void constraint_free (/*@only@*/ constraint c); -constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); - -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*/; -constraintExpr makeConstraintExprIntlit (int p_i); +extern /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); -/*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); +extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); -constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); +extern /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); -constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); +extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); -constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); +extern void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/; -constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c); -constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint); -void constraint_overWrite (constraint c1, constraint c2); -constraint constraint_copy (constraint c); +extern bool fileloc_closer (/*@observer@*/ fileloc loc1, /*@observer@*/ fileloc loc2, /*@observer@*/ fileloc loc3) /*@*/; -constraintExpr makePostOpInc (exprNode t1); +extern /*@only@*/ cstring arithType_print (arithType ar) /*@*/; +extern /*@only@*/ fileloc constraint_getFileloc (constraint c); +extern /*@only@*/ cstring constraint_print (constraint c) /*@*/; -bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3); +extern /*@only@*/ constraint constraint_makeWriteSafeInt (exprNode po, int ind); +extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/; -cstring arithType_print (arithType ar) /*@*/; +extern /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint); -fileloc constraint_getFileloc (constraint c); -cstring constraint_print (constraint c) /*@*/; -constraint constraint_makeWriteSafeInt (exprNode po, int 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); -exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src); +extern /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc 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); -/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/; -/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, - exprNodeList arglist); +extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition, + exprNodeList arglist); -cstring constraint_printDetailed (constraint c); +extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size); -constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall); -constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); -constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer); -/*drl add 11/28/2000 */ -constraint constraint_makeSRefWriteSafeInt (sRef s, int ind); -constraint constraint_makeSRefReadSafeInt (sRef s, int ind); -/*drl add 11/26/2000 */ -void constraint_printError (constraint c, fileloc loc); -constraint constraint_doSRefFixConstraintParam (constraint precondition, - exprNodeList arglist); +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint); -constraint constraint_makeSRefSetBufferSize (sRef s, int size); +extern bool constraint_search (constraint c, constraintExpr old); -constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall); +extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r); -constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer); +extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e); -constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint); -bool constraint_search (constraint c, constraintExpr old); +extern bool constraint_hasMaxSet(constraint c); -constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r); +/*from constraintGenreation.c*/ +extern void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint); -constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e); +extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e); +extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e); -bool constraint_hasMaxSet(constraint c); +extern constraint constraint_togglePost (/*@returned@*/ constraint c); +extern bool constraint_same (constraint c1, constraint c2) ; -/*from constraintGenreation.c*/ -bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint); +/*@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); -constraintList exprNode_traversRequiresConstraints (exprNode e); -constraintList exprNode_traversEnsuresConstraints (exprNode e); +constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint); -/*@notnull@*/ constraint constraint_makeNew (void) /*@*/; +/*@only@*/ constraint constraint_undump (FILE *f); +void constraint_dump (/*@observer@*/ constraint c, FILE *f); /*@=czechfcns*/ //#warning take this out