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