]>
Commit | Line | Data |
---|---|---|
92c4a786 | 1 | #ifndef __constraint_h__ |
bf92e32c | 2 | |
92c4a786 | 3 | #define __constraint_h__ |
bf92e32c | 4 | |
d0e5b01f | 5 | typedef enum |
6 | { | |
7 | LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE | |
8 | } | |
9 | arithType; | |
10 | ||
28bf4b0b | 11 | struct s_constraint { |
bf92e32c | 12 | constraint orig; |
90bc41f7 | 13 | constraint or; |
4ab867d6 | 14 | bool fcnPre; |
361091cc | 15 | constraintExpr lexpr; |
4cccc6ad | 16 | arithType ar; |
361091cc | 17 | constraintExpr expr; |
4cccc6ad | 18 | bool post; |
abd7f895 | 19 | /*@exposed@*/ /*@dependent@*/ exprNode generatingExpr; |
d0e5b01f | 20 | } ; |
21 | ||
6e88de2d | 22 | /*@constant null constraint constraint_undefined; @*/ |
92c4a786 | 23 | |
6e88de2d | 24 | # define constraint_undefined ((constraint)NULL) |
4cccc6ad | 25 | |
0e41eb0e | 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) /*@*/ ; | |
93307a76 | 29 | |
6e88de2d | 30 | # define constraint_isDefined(e) ((e) != constraint_undefined) |
31 | # define constraint_isUndefined(e) ((e) == constraint_undefined) | |
32 | # define constraint_isError(e) ((e) == constraint_undefined) | |
93307a76 | 33 | |
28bf4b0b | 34 | extern void constraint_free (/*@only@*/ constraint p_c); |
4cccc6ad | 35 | |
b7b694d6 | 36 | /* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); */ |
4cccc6ad | 37 | |
4cccc6ad | 38 | /*@-czechfcns*/ |
4cccc6ad | 39 | |
abd7f895 | 40 | extern constraint |
41 | constraint_makeReadSafeExprNode (/*@observer@*/ exprNode p_po, | |
42 | /*@observer@*/ exprNode p_ind); | |
4cccc6ad | 43 | |
abd7f895 | 44 | extern /*@only@*/ constraint constraint_makeWriteSafeExprNode (/*@observer@*/ exprNode p_po, |
45 | /*@observer@*/ exprNode p_ind); | |
4cccc6ad | 46 | |
abd7f895 | 47 | extern /*@only@*/ constraint constraint_makeReadSafeInt (/*@observer@*/ exprNode p_t1, int p_index); |
4cccc6ad | 48 | |
abd7f895 | 49 | extern /*@only@*/ constraint |
50 | constraint_makeEnsureMaxReadAtLeast (/*@observer@*/ exprNode p_t1, | |
51 | /*@observer@*/ exprNode p_t2, fileloc p_sequencePoint); | |
4cccc6ad | 52 | |
abd7f895 | 53 | extern void constraint_overWrite (constraint p_c1, /*@observer@*/ constraint p_c2) |
54 | /*@modifies p_c1 @*/; | |
4cccc6ad | 55 | |
abd7f895 | 56 | extern /*@only@*/ constraint constraint_copy (/*@temp@*/ constraint p_c); |
4cccc6ad | 57 | |
abd7f895 | 58 | extern bool fileloc_closer (/*@observer@*/ fileloc p_loc1, |
59 | /*@observer@*/ fileloc p_loc2, | |
60 | /*@observer@*/ fileloc p_loc3) /*@*/; | |
4cccc6ad | 61 | |
28bf4b0b | 62 | extern /*@only@*/ cstring arithType_print (arithType p_ar) /*@*/; |
4cccc6ad | 63 | |
28bf4b0b | 64 | extern /*@only@*/ fileloc constraint_getFileloc (constraint p_c); |
3814599d | 65 | |
66 | extern /*@only@*/ cstring constraint_unparse (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/; | |
67 | # define constraint_unparse constraint_print | |
68 | ||
28bf4b0b | 69 | extern /*@only@*/ cstring constraint_print (/*@temp@*/ /*@observer@*/ constraint p_c) /*@*/; |
d46ce6a4 | 70 | |
03d670b6 | 71 | extern /*@only@*/ constraint constraint_makeWriteSafeInt (/*@dependent@*/ /*@observer@*/ exprNode p_po, int p_ind); |
ef2aa32a | 72 | |
28bf4b0b | 73 | extern exprNode exprNode_copyConstraints (/*@returned@*/ exprNode p_dst, exprNode p_src) /*@modifies p_dst @*/; |
4cccc6ad | 74 | |
03d670b6 | 75 | extern /*@only@*/ constraint constraint_makeEnsureEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); |
4cccc6ad | 76 | |
03d670b6 | 77 | extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint); |
ef2aa32a | 78 | |
28bf4b0b | 79 | extern constraint constraint_preserveOrig (/*@returned@*/ constraint p_c) /*@modifies p_c @*/; |
80 | extern /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint p_precondition, | |
81 | exprNodeList p_arglist); | |
82 | extern /*@only@*/ cstring constraint_printDetailed (constraint p_c); | |
754746a0 | 83 | |
03d670b6 | 84 | extern /*@only@*/ constraint constraint_makeEnsureLessThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); |
85 | extern /*@only@*/ constraint constraint_makeEnsureLessThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); | |
754746a0 | 86 | |
03d670b6 | 87 | extern /*@only@*/ constraint constraint_makeEnsureGreaterThan (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); |
88 | extern /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (/*@dependent@*/ /*@observer@*/ exprNode p_e1, /*@dependent@*/ /*@observer@*/ exprNode p_e2, fileloc p_sequencePoint); | |
34f0c5e7 | 89 | |
90 | /*drl add 11/28/2000 */ | |
28bf4b0b | 91 | extern /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef p_s, int p_ind); |
92 | extern /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef p_s, int p_ind); | |
ef2aa32a | 93 | /*drl add 11/26/2000 */ |
28bf4b0b | 94 | extern void constraint_printError (/*@observer@*/ /*@temp@*/ constraint p_c, /*@temp@*/ /*@observer@*/ fileloc p_loc); |
d46ce6a4 | 95 | |
28bf4b0b | 96 | extern /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint p_precondition, |
97 | /*@temp@*/ /*@observer@*/ exprNodeList p_arglist); | |
ef2aa32a | 98 | |
28bf4b0b | 99 | extern /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef p_s, long int p_size); |
d46ce6a4 | 100 | |
28bf4b0b | 101 | extern /*@only@*/ constraint constraint_doFixResult (constraint p_postcondition, /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall); |
ef2aa32a | 102 | |
03d670b6 | 103 | extern /*@only@*/ constraint constraint_makeEnsureLteMaxRead(/*@dependent@*/ /*@observer@*/ exprNode p_index, /*@dependent@*/ /*@observer@*/ exprNode p_buffer); |
ef2aa32a | 104 | |
03d670b6 | 105 | extern /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (/*@dependent@*/ /*@observer@*/ exprNode p_e, fileloc p_sequencePoint); |
ef2aa32a | 106 | |
28bf4b0b | 107 | extern bool constraint_search (constraint p_c, constraintExpr p_old); |
103db890 | 108 | |
28bf4b0b | 109 | extern /*@only@*/ constraint makeConstraintParse3 (constraintExpr p_l, lltok p_relOp, constraintExpr p_r); |
103db890 | 110 | |
b37cf05e | 111 | extern constraint constraint_addGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@exposed@*/ exprNode p_e); |
103db890 | 112 | |
28bf4b0b | 113 | extern bool constraint_hasMaxSet(constraint p_c); |
103db890 | 114 | |
470b7798 | 115 | /*from constraintGenreation.c*/ |
abd7f895 | 116 | extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint); |
2934b455 | 117 | |
abd7f895 | 118 | extern /*@only@*/ constraintList |
119 | exprNode_traversRequiresConstraints (exprNode p_e); | |
120 | ||
121 | extern /*@only@*/ constraintList | |
122 | exprNode_traversEnsuresConstraints (exprNode p_e); | |
2934b455 | 123 | |
28bf4b0b | 124 | extern constraint constraint_togglePost (/*@returned@*/ constraint p_c); |
125 | extern bool constraint_same (constraint p_c1, constraint p_c2) ; | |
2934b455 | 126 | |
28bf4b0b | 127 | /*@only@*/ cstring constraint_printOr (constraint p_c) /*@*/; |
2934b455 | 128 | extern void constraint_printErrorPostCondition (constraint p_c, fileloc p_loc) ; |
e60dcce4 | 129 | |
130 | extern cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint p_c) /*@*/; /*drl add 8-11-001*/ | |
131 | ||
2934b455 | 132 | extern constraint constraint_setFcnPre (/*@returned@*/ constraint p_c) ; |
03d670b6 | 133 | extern constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint p_c, /*@dependent@*/ /*@observer@*/ exprNode p_e) ; |
470b7798 | 134 | |
393e573f | 135 | extern bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode p_e) ; |
28bf4b0b | 136 | constraint constraint_togglePostOrig (/*@returned@*/ constraint p_c); |
470b7798 | 137 | |
28bf4b0b | 138 | bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint p_c); |
470b7798 | 139 | |
28bf4b0b | 140 | constraint constraint_makeAddAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint); |
920a3797 | 141 | |
28bf4b0b | 142 | constraint constraint_makeSubtractAssign (/*@dependent@*/ /*@observer@*/ exprNode p_e, /*@dependent@*/ /*@observer@*/ exprNode p_f, fileloc p_sequencePoint); |
920a3797 | 143 | |
28bf4b0b | 144 | /*@only@*/ constraint constraint_undump (FILE * p_f); |
920a3797 | 145 | |
28bf4b0b | 146 | void constraint_dump (/*@observer@*/ constraint p_c, FILE * p_f); |
147 | ||
148 | extern void exprNode_forLoopHeuristics( /*@dependent@*/ exprNode p_e, /*@dependent@*/ exprNode p_forPred, /*@dependent@*/ exprNode p_forBody); | |
d46ce6a4 | 149 | |
e60dcce4 | 150 | int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * p_c1, /*@observer@*/ /*@temp@*/ const constraint * p_c2) /*@*/; |
02984642 | 151 | |
84380658 | 152 | bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint p_c); |
02984642 | 153 | |
a779b61e | 154 | bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint p_c); |
155 | ||
e5f31c00 | 156 | void exprNode_findValue( exprNode p_e); |
a779b61e | 157 | |
86d93ed3 | 158 | /*drl 1/6/2001: I didn't think these functions were solid enough to include in the stable release of splint.*/ |
159 | /*drl added 12/30/01 */ | |
160 | /* extern / *@only@* / constraint constraint_doSRefFixInvarConstraint(constraint p_invar, sRef p_s, ctype p_ct ); */ | |
fba0ed37 | 161 | |
162 | /*drl added 12/19 */ | |
163 | bool constraint_isConstantOnly (constraint p_c); | |
4cccc6ad | 164 | /*@=czechfcns*/ |
b7b694d6 | 165 | /* drl possible problem : warning take this out */ |
d0e5b01f | 166 | |
754746a0 | 167 | #include "constraintResolve.h" |
dc92450f | 168 | #include "constraintOutput.h" |
169 | ||
6e88de2d | 170 | #else |
171 | ||
172 | #error Multiple include | |
173 | ||
92c4a786 | 174 | #endif |
d0e5b01f | 175 |