]>
Commit | Line | Data |
---|---|---|
d1eb43aa | 1 | #ifndef __constraintExpr_h__ |
2 | ||
3 | #define __constraintExpr_h__ | |
4 | ||
d1eb43aa | 5 | typedef enum |
6 | { | |
7 | binaryexpr, | |
8 | unaryExpr, | |
90bc41f7 | 9 | term |
d1eb43aa | 10 | } |
11 | constraintExprKind; | |
12 | ||
28bf4b0b | 13 | struct s_constraintExpr { |
6e88de2d | 14 | constraintExprKind kind; |
86d93ed3 | 15 | bool ct; /*changed type */ |
16 | ctype origType; | |
6e88de2d | 17 | constraintExprData data; |
18 | }; | |
d1eb43aa | 19 | |
20 | ||
d46ce6a4 | 21 | |
6e88de2d | 22 | /*@constant null constraintExpr constraintExpr_undefined; @*/ |
23 | # define constraintExpr_undefined ((constraintExpr)NULL) | |
d1eb43aa | 24 | |
0e41eb0e | 25 | extern /*@falsewhennull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ; |
26 | extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ; | |
27 | extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ; | |
d1eb43aa | 28 | |
6e88de2d | 29 | # define constraintExpr_isDefined(e) ((e) != constraintExpr_undefined) |
30 | # define constraintExpr_isUndefined(e) ((e) == constraintExpr_undefined) | |
31 | # define constraintExpr_isError(e) ((e) == constraintExpr_undefined) | |
d1eb43aa | 32 | |
33 | ||
28bf4b0b | 34 | void constraintExpr_free ( /*@only@*/ constraintExpr p_expr); |
d1eb43aa | 35 | |
28bf4b0b | 36 | constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr p_c, fileloc p_loc) /*@modifies p_c@*/; |
d1eb43aa | 37 | |
28bf4b0b | 38 | constraintExpr constraintExpr_copy (constraintExpr p_expr) /*@*/; |
d1eb43aa | 39 | |
28bf4b0b | 40 | /*@only@*/ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr p_ex) /*@*/; |
41 | extern cstring constraintExpr_print (constraintExpr p_expr) /*@*/; | |
d1eb43aa | 42 | |
43 | ||
28bf4b0b | 44 | bool constraintExpr_similar (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; |
45 | bool constraintExpr_same (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; | |
46 | /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr p_c, /*@temp@*/ /*@observer@*/ constraintExpr p_old, /*@temp@*/ /*@observer@*/ constraintExpr p_newExpr ) /*@modifies p_c@*/; | |
b9904f57 | 47 | |
28bf4b0b | 48 | bool constraintExpr_canGetValue (constraintExpr p_expr) /*@*/; |
b9904f57 | 49 | long constraintExpr_getValue (constraintExpr p_expr) /*@*/; |
d1eb43aa | 50 | |
28bf4b0b | 51 | int constraintExpr_compare (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; |
d1eb43aa | 52 | |
b7b694d6 | 53 | /* constraintExpr constraintExpr_makeValueInt (int i); */ |
d1eb43aa | 54 | |
b9904f57 | 55 | /*@only@*/ constraintExpr constraintExpr_makeIntLiteral (long p_i); |
d1eb43aa | 56 | |
28bf4b0b | 57 | /*@only@*/ constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 58 | |
28bf4b0b | 59 | /*@only@*/ constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 60 | |
28bf4b0b | 61 | /*@only@*/ constraintExpr constraintExpr_makeMaxReadExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 62 | |
28bf4b0b | 63 | /*@only@*/ constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr p_expr); |
d1eb43aa | 64 | |
28bf4b0b | 65 | /*@only@*/ constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/ constraintExpr p_expr); |
d1eb43aa | 66 | |
28bf4b0b | 67 | /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr p_c); |
d1eb43aa | 68 | |
28bf4b0b | 69 | /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr p_lexpr, /*@only@*/ constraintExpr p_expr) /*@modifies p_lexpr, p_expr @*/; |
d1eb43aa | 70 | |
28bf4b0b | 71 | bool constraintExpr_search (/*@observer@*/ /*@temp@*/ constraintExpr p_c, /*@observer@*/ /*@temp@*/ constraintExpr p_old); |
d1eb43aa | 72 | |
28bf4b0b | 73 | /*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr p_expr); |
d1eb43aa | 74 | |
d46ce6a4 | 75 | |
03d670b6 | 76 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@temp@*/ /*@observer@*/ sRef p_s); |
d1eb43aa | 77 | |
28bf4b0b | 78 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxRead(/*@temp@*/ /*@observer@*/ sRef p_s); |
d1eb43aa | 79 | |
28bf4b0b | 80 | /*@only@*/ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef p_s); |
d46ce6a4 | 81 | |
28bf4b0b | 82 | constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr p_expr, exprNodeList p_arglist); |
d1eb43aa | 83 | |
28bf4b0b | 84 | /*@only@*/ constraintExpr constraintExpr_makeExprNode (/*@dependent@*/ exprNode p_e); |
d46ce6a4 | 85 | |
28bf4b0b | 86 | /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr p_expr, /*@observer@*/ exprNode p_fcnCall); |
d1eb43aa | 87 | |
0e41eb0e | 88 | /*@falsewhennull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ; |
2934b455 | 89 | |
28bf4b0b | 90 | /*@only@*/ constraintExpr constraintExpr_makeAddExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent); |
d46ce6a4 | 91 | |
28bf4b0b | 92 | /*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent); |
d1eb43aa | 93 | |
28bf4b0b | 94 | /*@only@*/ constraintExpr constraintExpr_parseMakeUnaryOp (lltok p_op,/*@only@*/ constraintExpr p_cexpr); |
d1eb43aa | 95 | |
28bf4b0b | 96 | constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr p_expr1, lltok p_op, /*@only@*/ constraintExpr p_expr2); |
d1eb43aa | 97 | |
28bf4b0b | 98 | bool constraintExpr_hasMaxSet (/*@observer@*/ /*@temp@*/ constraintExpr p_expr); |
470b7798 | 99 | |
90bc41f7 | 100 | |
28bf4b0b | 101 | |
102 | /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@returned@*/ /*@only@*/ constraintExpr p_expr, exprNodeList p_arglist) /*@modifies p_expr@*/; | |
6e88de2d | 103 | |
d46ce6a4 | 104 | /*@only@*/ |
28bf4b0b | 105 | constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr p_expr, |
106 | /*@out@*/ bool * p_propagate, | |
107 | /*@out@*/ int *p_literal); | |
6e88de2d | 108 | |
0e41eb0e | 109 | /*@falsewhennull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ; |
920a3797 | 110 | |
28bf4b0b | 111 | extern void constraintExpr_dump (/*@observer@*/ /*@temp@*/ constraintExpr p_expr, FILE *p_f); |
920a3797 | 112 | |
28bf4b0b | 113 | extern /*@only@*/ constraintExpr constraintExpr_undump (FILE *p_f); |
920a3797 | 114 | |
12f2ffe9 | 115 | extern /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode p_e) ; |
6e88de2d | 116 | |
a779b61e | 117 | /* drl added 8/8/001*/ |
118 | bool constraintExpr_isTerm (/*@observer@*/ /*@temp@*/ constraintExpr p_c); | |
119 | ||
120 | /* drl added 8/8/001*/ | |
121 | /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr p_c); | |
122 | ||
123 | /* drl added 8/8/001*/ | |
124 | int constraintExpr_getDepth (/*@observer@*/ /*@temp@*/ constraintExpr p_ex); | |
125 | ||
920a3797 | 126 | |
86d93ed3 | 127 | /*drl 1/6/2001: I didn't think these functions were solid enough to include in the stable release of splint.*/ |
128 | /* drl added 12/30/001*/ | |
129 | /* extern / *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr p_expr, sRef p_s, ctype p_ct); */ | |
130 | ||
fba0ed37 | 131 | |
132 | ||
133 | /*drl added 12/19 */ | |
134 | bool constraintExpr_isConstantOnly ( constraintExpr p_e ); | |
135 | ||
12f2ffe9 | 136 | #else |
6e88de2d | 137 | # error "Multiple include" |
d1eb43aa | 138 | #endif |