src/Headers/constraint.h

   1 typedef union constraintTermValue_
   2 {
   3   exprNode expr;
   4   sRef     sref;
   5   int      intlit;
   6 } constraintTermValue;
   7
   8 typedef enum
   9 {
  10   LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
  11 }
  12 arithType;
  13
  14 typedef enum
  15 {
  16  BUFFSIZE, STRINGLEN, VALUE, CALLSAFE,
  17  MAXSET, MINSET, MAXREAD, MINREAD,
  18  NULLTERMINATED,
  19  INCOP,
  20  UNDEFINED
  21 }
  22 constraintType;
  23
  24 typedef enum
  25 {
  26   PLUS,
  27   MINUS
  28 }
  29 constraintExprOp;
  30
  31
  32 typedef enum
  33 {
  34 EXPRNODE, SREF,
  35 INTLITERAL
  36 } constraintTermType;
  37
  38
  39 struct _constraintTerm {
  40   constraintType constrType;
  41   fileloc loc;
  42   constraintTermValue value;
  43   constraintTermType kind;
  44 };
  45
  46 abst_typedef struct _constraintTerm * constraintTerm;
  47
  48 struct constraintExpr_ {
  49
  50   constraintTerm term;
  51   constraintExprOp op;
  52   struct constraintExpr_ * expr;
  53 };
  54 # define constraintExpr_undefined ((constraintExpr)NULL)
  55
  56 typedef struct constraintExpr_ * constraintExpr;
  57 abst_typedef struct constr_ * constr;
  58
  59
  60 struct _constraint {
  61   constraintExpr lexpr;
  62   arithType       ar;
  63   constraintExpr  expr;
  64   bool post;
  65 } ;
  66
  67 #define max_constraints 100
  68
  69 //constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
  70
  71 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
  72
  73 constraint constraint_makeInc_Op (exprNode p_e1);
  74
  75 /*@i22*/
  76 /*@-czechfcns*/
  77 bool constraint_resolve (/*@unused@*/ constraint c);
  78
  79 /*@out@*/ constraintTerm new_constraintTermExpr (void);
  80 constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
  81
  82 constraintTerm intLit_makeConstraintTerm (int p_i);
  83
  84 /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
  85  /*@post:isnull result->expr@*/
  86      /*@post:notnull result->t1@*/
  87      /*@defines result->expr, result->t1, result->c1@, result->op*/;
  88
  89 constraintExpr makeConstraintExprIntlit (int p_i);
  90
  91 /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
  92
  93 constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
  94
  95 constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
  96
  97 constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
  98
  99 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
 100
 101 constraint constraint_makeSideEffectPostIncrement (exprNode t1,  fileloc p_sequencePoint);
 102 cstring constraintType_print (constraintType c1);
 103
 104 constraint constraint_copy (constraint c);
 105
 106 constraintExpr makePostOpInc (exprNode t1);
 107
 108
 109
 110 cstring constraintTerm_print (constraintTerm term);
 111
 112 cstring arithType_print (arithType ar);
 113
 114 cstring constraintExpr_print (constraintExpr ex);
 115
 116 cstring constraint_print (constraint c);
 117 /*@=czechfcns*/
 118 #warning take this out
 119 #include "constraintList.h"
 120
 121 #include "constraintTerm.h"
 122
 123
 124