src/Headers/constraint.h

   1 #ifndef __constraint_h__
   2
   3 #define __constraint_h__
   4
   5 typedef enum
   6 {
   7   LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
   8 }
   9 arithType;
  10
  11 //abst_typedef struct constr_ * constr;
  12
  13
  14 struct _constraint {
  15   constraint     orig;
  16   constraintExpr lexpr;
  17   arithType       ar;
  18   constraintExpr  expr;
  19   bool post;
  20 } ;
  21
  22 abst_typedef struct _constraintTerm * constraintTerm;
  23
  24 //constraint constraint_create (exprNode e1, exprNode e2,  arithType restriction, constraintType kind);
  25
  26
  27 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant);
  28
  29
  30 constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2);
  31
  32 constraint constraint_makeInc_Op (exprNode p_e1);
  33
  34 /*@i22*/
  35 /*@-czechfcns*/
  36 bool constraint_resolve (/*@unused@*/ constraint c);
  37
  38 /*@out@*/ constraintTerm new_constraintTermExpr (void);
  39 constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
  40
  41 constraintTerm intLit_makeConstraintTerm (int p_i);
  42
  43 /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
  44  /*@post:isnull result->expr@*/
  45      /*@post:notnull result->t1@*/
  46      /*@defines result->expr, result->t1, result->c1@, result->op*/;
  47
  48 constraintExpr makeConstraintExprIntlit (int p_i);
  49
  50 /*@relnull@*/ constraint constraint_makeReadSafeExprNode ( exprNode p_po, exprNode p_ind);
  51
  52 constraint constraint_makeWriteSafeExprNode (exprNode p_po, exprNode p_ind);
  53
  54 constraint constraint_makeReadSafeInt (exprNode p_t1, int p_index);
  55
  56 constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fileloc p_sequencePoint);
  57
  58 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
  59
  60 constraint constraint_makeSideEffectPostIncrement (exprNode t1,  fileloc p_sequencePoint);
  61 void constraint_overWrite (constraint c1, constraint c2);
  62 constraint constraint_copy (constraint c);
  63
  64 constraintExpr makePostOpInc (exprNode t1);
  65
  66
  67 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3);
  68 cstring constraintTerm_print (constraintTerm term);
  69
  70 cstring arithType_print (arithType ar);
  71
  72 cstring constraintExpr_print (constraintExpr ex);
  73 fileloc constraint_getFileloc (constraint c);
  74 cstring constraint_print (constraint c);
  75 constraint constraint_makeWriteSafeInt (exprNode po, int ind);
  76
  77 exprNode exprNode_copyConstraints (exprNode dst, exprNode src);
  78
  79 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint);
  80
  81 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint);
  82
  83 constraint constraint_preserveOrig (constraint c);
  84 constraint constraint_doSRefFixBaseParam (constraint precondition,
  85                                                    exprNodeList arglist);
  86
  87 cstring  constraint_printDetailed (constraint c);
  88
  89 /*@=czechfcns*/
  90 #warning take this out
  91 #include "constraintList.h"
  92
  93 #include "constraintExpr.h"
  94 #include "constraintTerm.h"
  95 #include "constraintResolve.h"
  96 #endif
  97