]>
Commit | Line | Data |
---|---|---|
1 | #ifndef __constraintExprData_h__ | |
2 | ||
3 | #define __constraintExprData_h__ | |
4 | ||
5 | ||
6 | typedef enum | |
7 | { | |
8 | BINARYOP_UNDEFINED, | |
9 | PLUS, | |
10 | MINUS | |
11 | } | |
12 | constraintExprBinaryOpKind; | |
13 | ||
14 | typedef enum | |
15 | { | |
16 | UNARYOP_UNDEFINED, | |
17 | MAXSET, MINSET, MAXREAD, MINREAD | |
18 | } | |
19 | constraintExprUnaryOpKind; | |
20 | ||
21 | ||
22 | typedef struct constraintExprBinaryOp_ | |
23 | { | |
24 | constraintExpr expr1; | |
25 | constraintExprBinaryOpKind binaryOp; | |
26 | constraintExpr expr2; | |
27 | } constraintExprBinaryOp; | |
28 | ||
29 | ||
30 | typedef struct constraintExprUnaryOp_ | |
31 | { | |
32 | constraintExpr expr; | |
33 | constraintExprUnaryOpKind unaryOp; | |
34 | } constraintExprUnaryOp; | |
35 | ||
36 | ||
37 | typedef union constraintExprData | |
38 | { | |
39 | constraintExprBinaryOp binaryOp; | |
40 | constraintExprUnaryOp unaryOp; | |
41 | constraintTerm term; | |
42 | } *constraintExprData; | |
43 | ||
44 | extern /*@falsenull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ; | |
45 | # define constraintExprData_isDefined(e) ((e) != NULL) | |
46 | ||
47 | extern void constraintExprData_freeBinaryExpr (/*@only@*/ constraintExprData) ; | |
48 | extern void constraintExprData_freeUnaryExpr (/*@only@*/ constraintExprData) ; | |
49 | extern void constraintExprData_freeTerm (/*@only@*/ constraintExprData) ; | |
50 | ||
51 | constraintExprData constraintExprData_termSetTerm ( /*@returned@*/ /*@partial@*/ constraintExprData p_data, /*@only@*/ constraintTerm p_term); | |
52 | ||
53 | /*@observer@*/ constraintTerm constraintExprData_termGetTerm (/*@observer@*/ constraintExprData p_data) /*@*/; | |
54 | ||
55 | constraintExprUnaryOpKind constraintExprData_unaryExprGetOp (/*@observer@*//*@reldef@*/constraintExprData p_data) /*@*/; | |
56 | ||
57 | /*@observer@*/ constraintExpr constraintExprData_unaryExprGetExpr (/*@observer@*/ /*@reldef@*/constraintExprData p_data) /*@*/; | |
58 | ||
59 | ||
60 | // special constraintExprData constraintExprData_unaryExprSetOp ( /out special@*/ @returned@ constraintExprData p_data, constraintExprUnaryOpKind op) /sets result->unaryOp.unaryOp; | |
61 | ||
62 | ||
63 | constraintExprData constraintExprData_unaryExprSetOp (/*@partial@*/ /*@returned@*/ constraintExprData p_data, constraintExprUnaryOpKind p_op); | |
64 | ||
65 | constraintExprData constraintExprData_unaryExprSetExpr (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr); | |
66 | ||
67 | ||
68 | constraintExprBinaryOpKind constraintExprData_binaryExprGetOp (/*@partial@*/constraintExprData p_data) /*@*/; | |
69 | ||
70 | /*@observer@*/ constraintExpr constraintExprData_binaryExprGetExpr1 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/; | |
71 | ||
72 | /*@observer@*/ constraintExpr constraintExprData_binaryExprGetExpr2 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/; | |
73 | ||
74 | constraintExprData constraintExprData_binaryExprSetExpr1 (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr) ; | |
75 | ||
76 | constraintExprData constraintExprData_binaryExprSetExpr2 (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr); | |
77 | ||
78 | constraintExprData constraintExprData_binaryExprSetOp (/*@partial@*/ /*@returned@*/ /*@out@*/constraintExprData p_data, constraintExprBinaryOpKind p_op); | |
79 | ||
80 | /*@only@*/ constraintExprData constraintExprData_copyBinaryExpr(/*@observer@*/ constraintExprData p_data); | |
81 | ||
82 | /*@only@*/ constraintExprData constraintExprData_copyUnaryExpr(/*@observer@*/ constraintExprData p_data); | |
83 | ||
84 | /*@only@*/ constraintExprData constraintExprData_copyTerm (/*@observer@*/ constraintExprData p_data); | |
85 | ||
86 | #else | |
87 | ||
88 | #error "Multiple Include" | |
89 | ||
90 | #endif |