src/Headers/constraintTerm.h

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