1 #ifndef __constraintExprData_h__
3 #define __constraintExprData_h__
12 constraintExprBinaryOpKind;
17 MAXSET, MINSET, MAXREAD, MINREAD
19 constraintExprUnaryOpKind;
22 typedef struct constraintExprBinaryOp_
25 constraintExprBinaryOpKind binaryOp;
27 } constraintExprBinaryOp;
30 typedef struct constraintExprUnaryOp_
33 constraintExprUnaryOpKind unaryOp;
34 } constraintExprUnaryOp;
37 typedef union constraintExprData
39 constraintExprBinaryOp binaryOp;
40 constraintExprUnaryOp unaryOp;
42 } *constraintExprData;
44 extern /*@falsenull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ;
45 # define constraintExprData_isDefined(e) ((e) != NULL)
47 extern void constraintExprData_freeBinaryExpr (/*@only@*/ constraintExprData) ;
48 extern void constraintExprData_freeUnaryExpr (/*@only@*/ constraintExprData) ;
49 extern void constraintExprData_freeTerm (/*@only@*/ constraintExprData) ;
51 constraintExprData constraintExprData_termSetTerm ( /*@returned@*/ /*@partial@*/ constraintExprData p_data, /*@only@*/ constraintTerm p_term);
53 /*@observer@*/ constraintTerm constraintExprData_termGetTerm (/*@observer@*/ constraintExprData p_data) /*@*/;
55 constraintExprUnaryOpKind constraintExprData_unaryExprGetOp (/*@observer@*//*@reldef@*/constraintExprData p_data) /*@*/;
57 /*@observer@*/ constraintExpr constraintExprData_unaryExprGetExpr (/*@observer@*/ /*@reldef@*/constraintExprData p_data) /*@*/;
60 // special constraintExprData constraintExprData_unaryExprSetOp ( /out special@*/ @returned@ constraintExprData p_data, constraintExprUnaryOpKind op) /sets result->unaryOp.unaryOp;
63 constraintExprData constraintExprData_unaryExprSetOp (/*@partial@*/ /*@returned@*/ constraintExprData p_data, constraintExprUnaryOpKind p_op);
65 constraintExprData constraintExprData_unaryExprSetExpr (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr);
68 constraintExprBinaryOpKind constraintExprData_binaryExprGetOp (/*@partial@*/constraintExprData p_data) /*@*/;
70 /*@observer@*/ constraintExpr constraintExprData_binaryExprGetExpr1 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/;
72 /*@observer@*/ constraintExpr constraintExprData_binaryExprGetExpr2 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/;
74 constraintExprData constraintExprData_binaryExprSetExpr1 (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr) ;
76 constraintExprData constraintExprData_binaryExprSetExpr2 (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr);
78 constraintExprData constraintExprData_binaryExprSetOp (/*@partial@*/ /*@returned@*/ /*@out@*/constraintExprData p_data, constraintExprBinaryOpKind p_op);
80 /*@only@*/ constraintExprData constraintExprData_copyBinaryExpr(/*@observer@*/ constraintExprData p_data);
82 /*@only@*/ constraintExprData constraintExprData_copyUnaryExpr(/*@observer@*/ constraintExprData p_data);
84 /*@only@*/ constraintExprData constraintExprData_copyTerm (/*@observer@*/ constraintExprData p_data);
88 #error "Multiple Include"