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