]>
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; |
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 | ||
28bf4b0b | 32 | void constraintExpr_free ( /*@only@*/ constraintExpr p_expr); |
d1eb43aa | 33 | |
28bf4b0b | 34 | constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr p_c, fileloc p_loc) /*@modifies p_c@*/; |
d1eb43aa | 35 | |
28bf4b0b | 36 | constraintExpr constraintExpr_copy (constraintExpr p_expr) /*@*/; |
d1eb43aa | 37 | |
28bf4b0b | 38 | /*@only@*/ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr p_ex) /*@*/; |
39 | extern cstring constraintExpr_print (constraintExpr p_expr) /*@*/; | |
d1eb43aa | 40 | |
41 | ||
28bf4b0b | 42 | bool constraintExpr_similar (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; |
43 | bool constraintExpr_same (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; | |
44 | /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr p_c, /*@temp@*/ /*@observer@*/ constraintExpr p_old, /*@temp@*/ /*@observer@*/ constraintExpr p_newExpr ) /*@modifies p_c@*/; | |
b9904f57 | 45 | |
28bf4b0b | 46 | bool constraintExpr_canGetValue (constraintExpr p_expr) /*@*/; |
b9904f57 | 47 | long constraintExpr_getValue (constraintExpr p_expr) /*@*/; |
d1eb43aa | 48 | |
28bf4b0b | 49 | int constraintExpr_compare (constraintExpr p_expr1, constraintExpr p_expr2) /*@*/; |
d1eb43aa | 50 | |
6e88de2d | 51 | //constraintExpr constraintExpr_makeValueInt (int i); |
d1eb43aa | 52 | |
b9904f57 | 53 | /*@only@*/ constraintExpr constraintExpr_makeIntLiteral (long p_i); |
d1eb43aa | 54 | |
28bf4b0b | 55 | /*@only@*/ constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 56 | |
28bf4b0b | 57 | /*@only@*/ constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 58 | |
28bf4b0b | 59 | /*@only@*/ constraintExpr constraintExpr_makeMaxReadExpr (/*@exposed@*/ exprNode p_expr); |
d1eb43aa | 60 | |
28bf4b0b | 61 | /*@only@*/ constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr p_expr); |
d1eb43aa | 62 | |
28bf4b0b | 63 | /*@only@*/ constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/ constraintExpr p_expr); |
d1eb43aa | 64 | |
28bf4b0b | 65 | /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr p_c); |
d1eb43aa | 66 | |
28bf4b0b | 67 | /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr p_lexpr, /*@only@*/ constraintExpr p_expr) /*@modifies p_lexpr, p_expr @*/; |
d1eb43aa | 68 | |
28bf4b0b | 69 | bool constraintExpr_search (/*@observer@*/ /*@temp@*/ constraintExpr p_c, /*@observer@*/ /*@temp@*/ constraintExpr p_old); |
d1eb43aa | 70 | |
28bf4b0b | 71 | /*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr p_expr); |
d1eb43aa | 72 | |
d46ce6a4 | 73 | |
03d670b6 | 74 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@temp@*/ /*@observer@*/ sRef p_s); |
d1eb43aa | 75 | |
28bf4b0b | 76 | /*@only@*/ constraintExpr constraintExpr_makeSRefMaxRead(/*@temp@*/ /*@observer@*/ sRef p_s); |
d1eb43aa | 77 | |
28bf4b0b | 78 | /*@only@*/ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef p_s); |
d46ce6a4 | 79 | |
28bf4b0b | 80 | constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr p_expr, exprNodeList p_arglist); |
d1eb43aa | 81 | |
28bf4b0b | 82 | /*@only@*/ constraintExpr constraintExpr_makeExprNode (/*@dependent@*/ exprNode p_e); |
d46ce6a4 | 83 | |
28bf4b0b | 84 | /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr p_expr, /*@observer@*/ exprNode p_fcnCall); |
d1eb43aa | 85 | |
7272a1c1 | 86 | /*@falsenull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ; |
2934b455 | 87 | |
28bf4b0b | 88 | /*@only@*/ constraintExpr constraintExpr_makeAddExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent); |
d46ce6a4 | 89 | |
28bf4b0b | 90 | /*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent); |
d1eb43aa | 91 | |
28bf4b0b | 92 | /*@only@*/ constraintExpr constraintExpr_parseMakeUnaryOp (lltok p_op,/*@only@*/ constraintExpr p_cexpr); |
d1eb43aa | 93 | |
28bf4b0b | 94 | constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr p_expr1, lltok p_op, /*@only@*/ constraintExpr p_expr2); |
d1eb43aa | 95 | |
28bf4b0b | 96 | bool constraintExpr_hasMaxSet (/*@observer@*/ /*@temp@*/ constraintExpr p_expr); |
470b7798 | 97 | |
90bc41f7 | 98 | |
28bf4b0b | 99 | |
100 | /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@returned@*/ /*@only@*/ constraintExpr p_expr, exprNodeList p_arglist) /*@modifies p_expr@*/; | |
6e88de2d | 101 | |
d46ce6a4 | 102 | /*@only@*/ |
28bf4b0b | 103 | constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr p_expr, |
104 | /*@out@*/ bool * p_propagate, | |
105 | /*@out@*/ int *p_literal); | |
6e88de2d | 106 | |
7272a1c1 | 107 | /*@falsenull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ; |
920a3797 | 108 | |
28bf4b0b | 109 | extern void constraintExpr_dump (/*@observer@*/ /*@temp@*/ constraintExpr p_expr, FILE *p_f); |
920a3797 | 110 | |
28bf4b0b | 111 | extern /*@only@*/ constraintExpr constraintExpr_undump (FILE *p_f); |
920a3797 | 112 | |
12f2ffe9 | 113 | extern /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode p_e) ; |
6e88de2d | 114 | |
920a3797 | 115 | |
12f2ffe9 | 116 | #else |
6e88de2d | 117 | # error "Multiple include" |
d1eb43aa | 118 | #endif |