]>
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 | ||
a8e557d3 | 13 | struct _constraintExpr { |
6e88de2d | 14 | constraintExprKind kind; |
15 | constraintExprData data; | |
16 | }; | |
d1eb43aa | 17 | |
18 | ||
d46ce6a4 | 19 | |
6e88de2d | 20 | /*@constant null constraintExpr constraintExpr_undefined; @*/ |
21 | # define constraintExpr_undefined ((constraintExpr)NULL) | |
d1eb43aa | 22 | |
6e88de2d | 23 | extern /*@falsenull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ; |
24 | extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ; | |
84c9ffbf | 25 | extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ; |
d1eb43aa | 26 | |
6e88de2d | 27 | # define constraintExpr_isDefined(e) ((e) != constraintExpr_undefined) |
28 | # define constraintExpr_isUndefined(e) ((e) == constraintExpr_undefined) | |
29 | # define constraintExpr_isError(e) ((e) == constraintExpr_undefined) | |
d1eb43aa | 30 | |
31 | ||
d46ce6a4 | 32 | void constraintExpr_free ( /*@only@*/ constraintExpr expr); |
d1eb43aa | 33 | |
dc92450f | 34 | int constraintExpr_getValue (constraintExpr expr) /*@*/; |
d1eb43aa | 35 | |
d46ce6a4 | 36 | constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c@*/; |
d1eb43aa | 37 | |
6e88de2d | 38 | constraintExpr constraintExpr_copy (constraintExpr expr) /*@*/; |
d1eb43aa | 39 | |
4ab867d6 | 40 | /*@only@*/ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/; |
dc92450f | 41 | extern cstring constraintExpr_print (constraintExpr expr) /*@*/; |
d1eb43aa | 42 | |
43 | ||
6e88de2d | 44 | bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2) /*@*/; |
45 | bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2) /*@*/; | |
bb25bea6 | 46 | /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@observer@*/ constraintExpr old, /*@observer@*/ constraintExpr new ) /*@modifies c@*/; |
6e88de2d | 47 | bool constraintExpr_canGetValue (constraintExpr expr) /*@*/; |
d1eb43aa | 48 | |
6e88de2d | 49 | int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2) /*@*/; |
d1eb43aa | 50 | |
6e88de2d | 51 | //constraintExpr constraintExpr_makeValueInt (int i); |
d1eb43aa | 52 | |
d46ce6a4 | 53 | /*@only@*/ constraintExpr constraintExpr_makeIntLiteral (int i); |
d1eb43aa | 54 | |
4ab867d6 | 55 | /*@only@*/ constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr); |
d1eb43aa | 56 | |
4ab867d6 | 57 | /*@only@*/ constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr); |
d1eb43aa | 58 | |
4ab867d6 | 59 | /*@only@*/ constraintExpr constraintExpr_makeMaxReadExpr (/*@exposed@*/ exprNode expr); |
d1eb43aa | 60 | |
d46ce6a4 | 61 | /*@only@*/ constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr); |
d1eb43aa | 62 | |
d46ce6a4 | 63 | /*@only@*/ constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/ constraintExpr expr); |
d1eb43aa | 64 | |
bb25bea6 | 65 | /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c); |
d1eb43aa | 66 | |
bb25bea6 | 67 | /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr) /*@modifies lexpr, expr @*/; |
d1eb43aa | 68 | |
bb25bea6 | 69 | bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old); |
d1eb43aa | 70 | |
4ab867d6 | 71 | /*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr expr); |
d1eb43aa | 72 | |
d46ce6a4 | 73 | |
4ab867d6 | 74 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@exposed@*/ sRef s); |
d1eb43aa | 75 | |
4ab867d6 | 76 | /*@only@*/ constraintExpr constraintExpr_makeTermsRef (/*@exposed@*/ sRef s); |
d1eb43aa | 77 | |
d1eb43aa | 78 | constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr expr, exprNodeList arglist); |
d46ce6a4 | 79 | |
4ab867d6 | 80 | /*@only@*/ constraintExpr constraintExpr_makeExprNode (/*@exposed@*/ exprNode e); |
d1eb43aa | 81 | |
4ab867d6 | 82 | /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr expr, /*@exposed@*/ exprNode fcnCall); |
d46ce6a4 | 83 | |
d1eb43aa | 84 | bool constraintExpr_isLit (constraintExpr expr); |
d1eb43aa | 85 | |
d46ce6a4 | 86 | /*@only@*/ constraintExpr constraintExpr_makeAddConstraintExpr (/*@only@*/constraintExpr expr, /*@only@*/ constraintExpr add); |
87 | ||
88 | /*@only@*/ constraintExpr constraintExpr_parseMakeUnaryOp (lltok op,/*@only@*/ constraintExpr cexpr); | |
d1eb43aa | 89 | |
d46ce6a4 | 90 | constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op, /*@only@*/ constraintExpr expr2); |
d1eb43aa | 91 | |
4ab867d6 | 92 | bool constraintExpr_hasMaxSet (/*@observer@*/ constraintExpr expr); |
d1eb43aa | 93 | |
470b7798 | 94 | |
4ab867d6 | 95 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxRead(/*@exposed@*/ sRef s); |
90bc41f7 | 96 | |
d46ce6a4 | 97 | /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@returned@*/ /*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/; |
6e88de2d | 98 | |
d46ce6a4 | 99 | /*@only@*/ |
100 | constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr, | |
101 | /*@out@*/ bool * propagate, | |
102 | /*@out@*/ int *literal); | |
6e88de2d | 103 | |
bb25bea6 | 104 | bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c); |
6e88de2d | 105 | #else |
106 | ||
107 | # error "Multiple include" | |
108 | ||
d1eb43aa | 109 | #endif |