1 #ifndef __constraint_h__
3 #define __constraint_h__
7 LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
19 /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
22 /*@constant null constraint constraint_undefined; @*/
24 # define constraint_undefined ((constraint)NULL)
26 extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
27 extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
28 extern /*@nullwhentrue@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
30 # define constraint_isDefined(e) ((e) != constraint_undefined)
31 # define constraint_isUndefined(e) ((e) == constraint_undefined)
32 # define constraint_isError(e) ((e) == constraint_undefined)
34 extern void constraint_free (/*@only@*/ constraint p_c);
36 /* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); */
42 constraint_makeReadSafeExprNode (/*@observer@*/ exprNode p_po,
43 /*@observer@*/ exprNode p_ind);
45 extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@observer@*/ exprNode p_po,
46 /*@observer@*/ exprNode p_ind);
48 extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@observer@*/ exprNode p_t1, int p_index);
50 extern /*@only@*/ constraint
51 constraint_makeEnsureMaxReadAtLeast (/*@observer@*/ exprNode p_t1,
52 /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint);
54 extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2)
57 extern /*@only@*/ constraint constraint_copy (/*@temp@*/ constraint p_c);
59 extern bool fileloc_closer (/*@observer@*/ fileloc p_loc1,
60 /*@observer@*/ fileloc p_loc2,
61 /*@observer@*/ fileloc p_loc3) /*@*/;
63 extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/;
65 extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c);
67 extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
68 # define constraint_unparse constraint_print
70 extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/;
72 extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind);
74 extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/;
76 extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
78 extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
80 extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/;
81 extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition,
82 exprNodeList p_arglist);
83 extern /*@only@*/ cstring constraint_printDetailed (constraint p_c);
85 extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
86 extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
88 extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
89 extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint);
91 /*drl add 11/28/2000 */
92 extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind);
93 extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef p_s, int p_ind);
94 /*drl add 11/26/2000 */
95 extern void constraint_printError (/*@observer@*/ /*@temp@*/ constraint p_c, /*@temp@*/ /*@observer@*/ fileloc p_loc);
97 extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint p_precondition,
98 /*@temp@*/ /*@observer@*/ exprNodeList p_arglist);
100 extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long int p_size);
102 extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall);
104 extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@observer@*/ exprNode p_index, /*@dependent@*/ /*@observer@*/ exprNode p_buffer);
106 extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint);
108 extern bool constraint_search (constraint p_c, constraintExpr p_old);
110 extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr p_l, lltok p_relOp, constraintExpr p_r);
112 extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@exposed@*/ exprNode p_e);
114 extern bool constraint_hasMaxSet(constraint p_c);
116 /*from constraintGenreation.c*/
117 extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
119 extern /*@only@*/ constraintList
120 exprNode_traversRequiresConstraints (exprNode p_e);
122 extern /*@only@*/ constraintList
123 exprNode_traversEnsuresConstraints (exprNode p_e);
125 extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
126 extern bool constraint_same (constraint p_c1, constraint p_c2) ;
128 /*@only@*/ cstring constraint_printOr (constraint p_c) /*@*/;
129 extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ;
131 extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/
133 extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ;
134 extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ;
136 extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ;
137 constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c);
139 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c);
141 constraint constraint_makeAddAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
143 constraint constraint_makeSubtractAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint);
145 /*@only@*/ constraint constraint_undump (FILE * p_f);
147 void constraint_dump (/*@observer@*/ constraint p_c, FILE * p_f);
149 extern void exprNode_forLoopHeuristics( /*@dependent@*/ exprNode p_e, /*@dependent@*/ exprNode p_forPred, /*@dependent@*/ exprNode p_forBody);
151 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * p_c1, /*@observer@*/ /*@temp@*/ const constraint * p_c2) /*@*/;
153 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint p_c);
155 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint p_c);
157 void exprNode_findValue( exprNode p_e);
159 /*drl 1/6/2001: I didn't think these functions were solid enough to include in the stable release of splint.*/
160 /*drl added 12/30/01 */
161 /* extern / *@only@* / constraint constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */
164 bool constraint_isConstantOnly (constraint p_c);
166 /* drl possible problem : warning take this out */
168 #include "constraintResolve.h"
169 #include "constraintOutput.h"
173 #error Multiple include