]>
Commit | Line | Data |
---|---|---|
92c4a786 | 1 | #ifndef __constraintTerm_h__ |
2 | ||
3 | #define __constraintTerm_h__ | |
4 | ||
6e88de2d | 5 | typedef union |
6 | { | |
7 | exprNode expr; | |
8 | sRef sref; | |
9 | int intlit; | |
10 | } constraintTermValue; | |
dc92450f | 11 | |
6e88de2d | 12 | void constraintTermValue_copy (/*@out@*/ constraintTermValue src, constraintTermValue dst); |
92c4a786 | 13 | |
84c9ffbf | 14 | /*@-macroassign*/ |
15 | ||
6e88de2d | 16 | #define constraintTermValue_copy(dst, src) ((dst) = (src)) |
92c4a786 | 17 | |
84c9ffbf | 18 | /*@=macroassign*/ |
19 | ||
6e88de2d | 20 | typedef enum |
21 | { | |
22 | ERRORBADCONSTRAINTTERMTYPE, | |
23 | EXPRNODE, SREF, | |
24 | INTLITERAL | |
25 | } constraintTermType; | |
361091cc | 26 | |
6e88de2d | 27 | struct _constraintTerm { |
28 | fileloc loc; | |
29 | constraintTermValue value; | |
30 | constraintTermType kind; | |
31 | }; | |
92c4a786 | 32 | |
33 | ||
6e88de2d | 34 | abst_typedef struct _constraintTerm * constraintTerm; |
92c4a786 | 35 | |
92c4a786 | 36 | |
92c4a786 | 37 | |
a8e557d3 | 38 | extern /*@falsenull@*/ bool constraintTerm_isDefined (constraintTerm p_e) /*@*/; |
39 | extern /*@unused@*/ /*@truenull@*/ bool constraintTerm_isUndefined (constraintTerm p_e) /*@*/ ; | |
84c9ffbf | 40 | extern /*@unused@*/ /*@truenull@*/ bool constraintTerm_isError (constraintTerm p_e) /*@*/ ; |
a8e557d3 | 41 | |
84c9ffbf | 42 | /*@constant null constraintTerm constraintTerm_undefined; @*/ |
a8e557d3 | 43 | |
44 | # define constraintTerm_undefined ((constraintTerm)NULL) | |
45 | ||
46 | # define constraintTerm_isDefined(e) ((e) != constraintTerm_undefined) | |
47 | # define constraintTerm_isUndefined(e) ((e) == constraintTerm_undefined) | |
48 | # define constraintTerm_isError(e) ((e) == constraintTerm_undefined) | |
49 | ||
50 | ||
51 | ||
52 | ||
53 | ||
6e88de2d | 54 | constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/ ; |
361091cc | 55 | |
6e88de2d | 56 | constraintTerm constraintTerm_makeExprNode (/*@only@*/ exprNode e) /*@*/; |
361091cc | 57 | |
6e88de2d | 58 | constraintTerm constraintTerm_copy (constraintTerm term) /*@*/; |
361091cc | 59 | |
84c9ffbf | 60 | //constraintTerm exprNode_makeConstraintTerm ( exprNode e) /*@*/; |
361091cc | 61 | |
6e88de2d | 62 | bool constraintTerm_same (constraintTerm term1, constraintTerm term2) /*@*/; |
361091cc | 63 | |
6e88de2d | 64 | bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) /*@*/; |
361091cc | 65 | |
6e88de2d | 66 | bool constraintTerm_canGetValue (constraintTerm term)/*@*/; |
67 | int constraintTerm_getValue (constraintTerm term) /*@*/; | |
361091cc | 68 | |
6e88de2d | 69 | fileloc constraintTerm_getFileloc (constraintTerm t) /*@*/; |
361091cc | 70 | |
84c9ffbf | 71 | //constraintTerm constraintTerm_makeMaxSetexpr (exprNode e) /*@*/; |
361091cc | 72 | |
84c9ffbf | 73 | //constraintTerm constraintTerm_makeMinSetexpr (exprNode e) /*@*/; |
361091cc | 74 | |
84c9ffbf | 75 | //constraintTerm constraintTerm_makeMaxReadexpr (exprNode e) /*@*/; |
93307a76 | 76 | |
84c9ffbf | 77 | //constraintTerm constraintTerm_makeMinReadexpr (exprNode e) /*@*/; |
93307a76 | 78 | |
84c9ffbf | 79 | //constraintTerm constraintTerm_makeValueexpr (exprNode e) /*@*/; |
93307a76 | 80 | |
84c9ffbf | 81 | //constraintTerm intLit_makeConstraintTerm (int i) /*@*/; |
ef2aa32a | 82 | |
84c9ffbf | 83 | //constraintTerm constraintTerm_makeIntLitValue (int i) /*@*/; |
ef2aa32a | 84 | |
6e88de2d | 85 | bool constraintTerm_isIntLiteral (constraintTerm term) /*@*/; |
dc92450f | 86 | |
6e88de2d | 87 | cstring constraintTerm_print (constraintTerm term) /*@*/; |
ef2aa32a | 88 | |
6e88de2d | 89 | constraintTerm constraintTerm_makesRef (/*@only@*/ sRef s) /*@*/; |
ef2aa32a | 90 | |
6e88de2d | 91 | bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) /*@*/; |
ef2aa32a | 92 | |
6e88de2d | 93 | constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc) /*@modifies term@*/; |
92c4a786 | 94 | |
6e88de2d | 95 | constraintTerm constraintTerm_makeIntLiteral (int i) /*@*/; |
92c4a786 | 96 | |
6e88de2d | 97 | bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/; |
98 | cstring constraintTerm_getStringLiteral (constraintTerm c) /*@*/; | |
92c4a786 | 99 | |
a8e557d3 | 100 | |
101 | constraintTerm | |
102 | constraintTerm_doSRefFixBaseParam (constraintTerm term, exprNodeList arglist) /*@modifies term@*/; | |
92c4a786 | 103 | |
6e88de2d | 104 | #else |
92c4a786 | 105 | |
6e88de2d | 106 | #error Multiple Include |
361091cc | 107 | |
6e88de2d | 108 | #endif |