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