]>
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 | ||
4cccc6ad | 11 | struct _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; |
d46ce6a4 | 19 | /*@kept@*/ exprNode generatingExpr; |
d0e5b01f | 20 | } ; |
21 | ||
6e88de2d | 22 | /*@constant null constraint constraint_undefined; @*/ |
92c4a786 | 23 | |
6e88de2d | 24 | # define constraint_undefined ((constraint)NULL) |
4cccc6ad | 25 | |
6e88de2d | 26 | extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ; |
27 | extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ; | |
84c9ffbf | 28 | extern /*@truenull@*/ /*@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 | |
d46ce6a4 | 34 | void constraint_free (/*@only@*/ /*@notnull@*/ constraint c); |
4cccc6ad | 35 | |
bb25bea6 | 36 | //constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant); |
4cccc6ad | 37 | |
38 | /*@i22*/ | |
39 | /*@-czechfcns*/ | |
4cccc6ad | 40 | |
6e88de2d | 41 | ///*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term) |
42 | // /*@post:isnull result->expr@*/ | |
43 | // /*@post:notnull result->t1@*/ | |
44 | // /*@defines result->expr, result->t1, result->c1@, result->op*/; | |
4cccc6ad | 45 | |
84c9ffbf | 46 | //constraintExpr makeConstraintExprIntlit (int p_i); |
4cccc6ad | 47 | |
48 | /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind); | |
49 | ||
d46ce6a4 | 50 | /*@only@*/ constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind); |
4cccc6ad | 51 | |
d46ce6a4 | 52 | /*@only@*/ constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index); |
4cccc6ad | 53 | |
d46ce6a4 | 54 | /*@only@*/ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint); |
4cccc6ad | 55 | |
d46ce6a4 | 56 | void constraint_overWrite (constraint c1, /*@observer@*/ constraint c2) /*@modifies c1 @*/; |
4cccc6ad | 57 | |
d46ce6a4 | 58 | /*@only@*/ constraint constraint_copy (/*@observer@*/ constraint c); |
4cccc6ad | 59 | |
84c9ffbf | 60 | //constraintExpr makePostOpInc (exprNode t1); |
4cccc6ad | 61 | |
62 | ||
d46ce6a4 | 63 | bool fileloc_closer (/*@observer@*/ fileloc loc1,/*@observer@*/ fileloc loc2,/*@observer@*/ fileloc loc3) /*@*/; |
64 | ||
ef2aa32a | 65 | |
d46ce6a4 | 66 | /*@only@*/ cstring arithType_print (arithType ar) /*@*/; |
4cccc6ad | 67 | |
4cccc6ad | 68 | |
d46ce6a4 | 69 | /*@only@*/fileloc constraint_getFileloc (constraint c); |
70 | /*@only@*/ cstring constraint_print (constraint c) /*@*/; | |
ef2aa32a | 71 | |
d46ce6a4 | 72 | /*@only@*/constraint constraint_makeWriteSafeInt (exprNode po, int ind); |
754746a0 | 73 | |
d46ce6a4 | 74 | exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) /*@modifies dst @*/; |
754746a0 | 75 | |
d46ce6a4 | 76 | /*@only@*/ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint); |
754746a0 | 77 | |
d46ce6a4 | 78 | /*@only@*/ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint); |
754746a0 | 79 | |
d46ce6a4 | 80 | constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/; |
dc92450f | 81 | /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, |
d46ce6a4 | 82 | exprNodeList arglist); |
93307a76 | 83 | |
d46ce6a4 | 84 | /*@only@*/ cstring constraint_printDetailed (constraint c); |
93307a76 | 85 | |
d46ce6a4 | 86 | /*@only@*/ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint); |
34f0c5e7 | 87 | |
d46ce6a4 | 88 | /*@only@*/ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); |
89 | ||
90 | /*@only@*/ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint); | |
91 | /*@only@*/ constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint); | |
34f0c5e7 | 92 | |
93 | /*drl add 11/28/2000 */ | |
d46ce6a4 | 94 | /*@only@*/ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind); |
95 | /*@unused@*/ /*@only@*/ constraint constraint_makeSRefReadSafeInt (sRef s, int ind); | |
ef2aa32a | 96 | /*drl add 11/26/2000 */ |
d46ce6a4 | 97 | void constraint_printError (/*@observer@*/ constraint c, /*@observer@*/ fileloc loc); |
98 | ||
99 | /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition, | |
ef2aa32a | 100 | exprNodeList arglist); |
101 | ||
d46ce6a4 | 102 | /*@only@*/ constraint constraint_makeSRefSetBufferSize (sRef s, long int size); |
103 | ||
104 | /*@only@*/ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall); | |
ef2aa32a | 105 | |
d46ce6a4 | 106 | /*@only@*/ constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer); |
ef2aa32a | 107 | |
d46ce6a4 | 108 | /*@only@*/ constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint); |
ef2aa32a | 109 | |
97e4a647 | 110 | bool constraint_search (constraint c, constraintExpr old); |
103db890 | 111 | |
d46ce6a4 | 112 | /*@only@*/ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r); |
103db890 | 113 | |
114 | constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e); | |
115 | ||
116 | bool constraint_hasMaxSet(constraint c); | |
117 | ||
470b7798 | 118 | /*from constraintGenreation.c*/ |
bb25bea6 | 119 | void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ fileloc sequencePoint); |
470b7798 | 120 | |
d46ce6a4 | 121 | /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e); |
122 | /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e); | |
470b7798 | 123 | |
84c9ffbf | 124 | constraint constraint_togglePost (/*@returned@*/ constraint c); |
470b7798 | 125 | |
d46ce6a4 | 126 | /*@only@*/ cstring constraint_printOr (constraint c) /*@*/; |
127 | ||
4cccc6ad | 128 | /*@=czechfcns*/ |
ef2aa32a | 129 | //#warning take this out |
d0e5b01f | 130 | |
754746a0 | 131 | #include "constraintResolve.h" |
dc92450f | 132 | #include "constraintOutput.h" |
133 | ||
6e88de2d | 134 | #else |
135 | ||
136 | #error Multiple include | |
137 | ||
92c4a786 | 138 | #endif |
d0e5b01f | 139 |