X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/920a3797c23377bfb7332b0c11bda1d708cabb72..b37cf05e81a9ef7fc429327a75dfad628f86c809:/src/Headers/constraint.h diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 9addd22..a39add5 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -8,7 +8,7 @@ typedef enum } arithType; -struct _constraint { +struct s_constraint { constraint orig; constraint or; bool fcnPre; @@ -16,7 +16,7 @@ struct _constraint { arithType ar; constraintExpr expr; bool post; - /*@kept@*/ exprNode generatingExpr; + /*@observer@*/ /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr; } ; /*@constant null constraint constraint_undefined; @*/ @@ -31,110 +31,107 @@ extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@* # define constraint_isUndefined(e) ((e) == constraint_undefined) # define constraint_isError(e) ((e) == constraint_undefined) -extern void constraint_free (/*@only@*/ constraint c); +extern void constraint_free (/*@only@*/ constraint p_c); //constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); /*@i22*/ /*@-czechfcns*/ -///*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) -// /*@post:isnull result->expr@*/ -// /*@post:notnull result->t1@*/ -// /*@defines result->expr, result->t1, result->c1@, result->op*/; - -extern /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); +extern constraint constraint_makeReadSafeExprNode ( /*@dependent@*/ /*@oberserver@*/ exprNode p_po, /*@dependent@*/ /*@oberserver@*/ exprNode p_ind); -extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); +extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@dependent@*/ /*@oberserver@*/ exprNode p_po, /*@dependent@*/ /*@oberserver@*/ exprNode p_ind); -extern /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); +extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@dependent@*/ /*@oberserver@*/ exprNode p_t1, int p_index); -extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (/*@dependent@*/ /*@oberserver@*/ exprNode p_t1, /*@dependent@*/ /*@oberserver@*/ exprNode p_t2, fileloc p_sequencePoint); -extern void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/; +extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) /*@modifies p_c1 @*/; -extern /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c); +extern /*@only@*/ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint p_c); -extern bool fileloc_closer (/*@observer@*/ fileloc loc1, /*@observer@*/ fileloc loc2, /*@observer@*/ fileloc loc3) /*@*/; +extern bool fileloc_closer (/*@observer@*/ fileloc p_loc1, /*@observer@*/ fileloc p_loc2, /*@observer@*/ fileloc p_loc3) /*@*/; -extern /*@only@*/ cstring arithType_print (arithType ar) /*@*/; +extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/; -extern /*@only@*/ fileloc constraint_getFileloc (constraint c); -extern /*@only@*/ cstring constraint_print (constraint c) /*@*/; +extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c); +extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/; -extern /*@only@*/ constraint constraint_makeWriteSafeInt (exprNode po, int ind); +extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@oberserver@*/ exprNode p_po, int p_ind); -extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/; +extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/; -extern /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint); -extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@oberserver@*/ exprNode p_e, fileloc p_sequencePoint); -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); +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@*/ cstring constraint_printDetailed (constraint p_c); -extern /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); -extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); -extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); -extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, fileloc p_sequencePoint); +extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@oberserver@*/ exprNode p_e1, /*@dependent@*/ /*@oberserver@*/ exprNode p_e2, 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); +extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind); +extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef p_s, int p_ind); /*drl add 11/26/2000 */ -extern void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc); +extern void constraint_printError (/*@observer@*/ /*@temp@*/ constraint p_c, /*@temp@*/ /*@observer@*/ fileloc p_loc); -extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition, - exprNodeList arglist); +extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint p_precondition, + /*@temp@*/ /*@observer@*/ exprNodeList p_arglist); -extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size); +extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long int p_size); -extern /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall); +extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall); -extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer); +extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@oberserver@*/ exprNode p_index, /*@dependent@*/ /*@oberserver@*/ exprNode p_buffer); -extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint); +extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@oberserver@*/ exprNode p_e, fileloc p_sequencePoint); -extern bool constraint_search (constraint c, constraintExpr old); +extern bool constraint_search (constraint p_c, constraintExpr p_old); -extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r); +extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr p_l, lltok p_relOp, constraintExpr p_r); -extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e); +extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@exposed@*/ exprNode p_e); -extern bool constraint_hasMaxSet(constraint c); +extern bool constraint_hasMaxSet(constraint p_c); /*from constraintGenreation.c*/ -extern void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint); +extern void exprNode_exprTraverse (/*@dependent@*/ exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint); -extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e); -extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e); +extern /*@only@*/ constraintList exprNode_traversRequiresConstraints (/*@dependent@*/ exprNode p_e); +extern /*@only@*/ constraintList exprNode_traversEnsuresConstraints (/*@dependent@*/ exprNode p_e); -extern constraint constraint_togglePost (/*@returned@*/ constraint c); -extern bool constraint_same (constraint c1, constraint c2) ; +extern constraint constraint_togglePost (/*@returned@*/ constraint p_c); +extern bool constraint_same (constraint p_c1, constraint p_c2) ; -/*@only@*/ cstring constraint_printOr (constraint c) /*@*/; +/*@only@*/ cstring constraint_printOr (constraint p_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 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@oberserver@*/ exprNode p_e) ; -extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ; -constraint constraint_togglePostOrig (/*@returned@*/ constraint c); +extern bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode p_e) ; +constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c); -bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c); +bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c); -constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint); +constraint constraint_makeAddAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint); -constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint); +constraint constraint_makeSubtractAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint); -/*@only@*/ constraint constraint_undump (FILE *f); +/*@only@*/ constraint constraint_undump (FILE * p_f); -void constraint_dump (/*@observer@*/ constraint c, FILE *f); +void constraint_dump (/*@observer@*/ constraint p_c, FILE * p_f); + +extern void exprNode_forLoopHeuristics( /*@dependent@*/ exprNode p_e, /*@dependent@*/ exprNode p_forPred, /*@dependent@*/ exprNode p_forBody); /*@=czechfcns*/ -//#warning take this out +////drl possible problem : warning take this out #include "constraintResolve.h" #include "constraintOutput.h"