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