src/Headers/constraintExprData.h

   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/*@unused@*/ /*@truenull@*/ bool constraintExprData_isError (/*@observer@*/ constraintExprData p_e) /*@*/ ;
  48
  49 extern void constraintExprData_freeBinaryExpr (/*@only@*/ constraintExprData) ;
  50 extern void constraintExprData_freeUnaryExpr (/*@only@*/ constraintExprData) ;
  51 extern void constraintExprData_freeTerm (/*@only@*/ constraintExprData) ;
  52
  53 constraintExprData constraintExprData_termSetTerm ( /*@returned@*/ /*@partial@*/ constraintExprData p_data, /*@only@*/ constraintTerm p_term);
  54
  55 /*@observer@*/ constraintTerm constraintExprData_termGetTerm (/*@observer@*/ constraintExprData p_data) /*@*/;
  56
  57 constraintExprUnaryOpKind constraintExprData_unaryExprGetOp (/*@observer@*//*@reldef@*/constraintExprData p_data) /*@*/;
  58
  59 /*@observer@*/ constraintExpr  constraintExprData_unaryExprGetExpr (/*@observer@*/ /*@reldef@*/constraintExprData p_data) /*@*/;
  60
  61
  62 //  special constraintExprData  constraintExprData_unaryExprSetOp ( /out special@*/ @returned@ constraintExprData p_data, constraintExprUnaryOpKind op) /sets result->unaryOp.unaryOp;
  63
  64
  65 constraintExprData  constraintExprData_unaryExprSetOp (/*@partial@*/ /*@returned@*/ constraintExprData p_data, constraintExprUnaryOpKind p_op);
  66
  67 constraintExprData  constraintExprData_unaryExprSetExpr (/*@partial@*/ /*@returned@*/ constraintExprData p_data,  /*@only@*/ constraintExpr p_expr);
  68
  69
  70 constraintExprBinaryOpKind  constraintExprData_binaryExprGetOp (/*@partial@*/constraintExprData p_data) /*@*/;
  71
  72 /*@observer@*/ constraintExpr  constraintExprData_binaryExprGetExpr1 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/;
  73
  74 /*@observer@*/ constraintExpr  constraintExprData_binaryExprGetExpr2 (/*@observer@*/ /*@reldef@*/constraintExprData p_data)/*@*/;
  75
  76 constraintExprData  constraintExprData_binaryExprSetExpr1 (/*@partial@*/ /*@returned@*/ constraintExprData p_data, /*@only@*/ constraintExpr p_expr) ;
  77
  78 constraintExprData  constraintExprData_binaryExprSetExpr2  (/*@partial@*/ /*@returned@*/  constraintExprData p_data, /*@only@*/ constraintExpr p_expr);
  79
  80 constraintExprData  constraintExprData_binaryExprSetOp (/*@partial@*/ /*@returned@*/ /*@out@*/constraintExprData p_data, constraintExprBinaryOpKind p_op);
  81
  82 /*@only@*/ constraintExprData constraintExprData_copyBinaryExpr(/*@observer@*/ constraintExprData p_data);
  83
  84 /*@only@*/ constraintExprData constraintExprData_copyUnaryExpr(/*@observer@*/ constraintExprData p_data);
  85
  86 /*@only@*/ constraintExprData constraintExprData_copyTerm (/*@observer@*/ constraintExprData p_data);
  87
  88 #else
  89
  90 #error "Multiple Include"
  91
  92 #endif