src/Headers/constraintExprData.h

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