]>
Commit | Line | Data |
---|---|---|
4cccc6ad | 1 | /* |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000. | |
3 | ** See ../LICENSE for license information. | |
4 | */ | |
5 | # ifndef constraintLIST_H | |
6 | # define constraintLIST_H | |
7 | ||
8 | typedef /*@only@*/ constraint o_constraint; | |
9 | ||
93307a76 | 10 | struct _constraintList |
4cccc6ad | 11 | { |
12 | int nelements; | |
13 | int nspace; | |
14 | /*@reldef@*/ /*@relnull@*/ o_constraint *elements; | |
93307a76 | 15 | } ; |
16 | ||
17 | /*@constant null constraintList constraintList_undefined;@*/ | |
18 | # define constraintList_undefined ((constraintList) 0) | |
4cccc6ad | 19 | |
20 | /*@iter constraintList_elements (sef constraintList x, yield exposed constraint el); @*/ | |
21 | # define constraintList_elements(x, m_el) \ | |
22 | { int m_ind; constraint *m_elements = &((x)->elements[0]); \ | |
23 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
24 | { constraint m_el = *(m_elements++); | |
25 | ||
26 | # define end_constraintList_elements }} | |
27 | ||
28 | extern /*@only@*/ constraintList constraintList_new(void); | |
29 | extern constraintList constraintList_add (/*@returned@*/ constraintList p_s, /*@only@*/ constraint p_el) ; | |
30 | ||
361091cc | 31 | extern constraintList constraintList_addList (/*@returned@*/ constraintList s, /*@only@*/constraintList new); |
32 | ||
33 | ||
4cccc6ad | 34 | extern constraintList constraintList_copy (constraintList p_s); |
35 | ||
36 | //extern /*@only@*/ cstring constraintList_unparse (constraintList p_s) ; | |
37 | extern void constraintList_free (/*@only@*/ constraintList p_s) ; | |
38 | ||
361091cc | 39 | |
ef2aa32a | 40 | |
361091cc | 41 | |
42 | extern cstring constraintList_print (constraintList s); | |
754746a0 | 43 | |
44 | extern cstring | |
45 | constraintList_printDetailed (constraintList s); | |
46 | ||
47 | ||
48 | extern constraintList | |
49 | constraintList_logicalOr (constraintList l1, constraintList l2); | |
50 | ||
51 | extern constraintList constraintList_preserveOrig (constraintList c); | |
52 | ||
4cccc6ad | 53 | /*@constant int constraintListBASESIZE;@*/ |
754746a0 | 54 | |
93307a76 | 55 | extern constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, exprNodeList arglist); |
754746a0 | 56 | |
ef2aa32a | 57 | extern constraintList constraintList_togglePost (constraintList c); |
58 | ||
59 | extern constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist); | |
60 | ||
61 | extern constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall); | |
62 | ||
63 | constraintList constraintList_doFixResult (constraintList postconditions, exprNode fcnCall); | |
4cccc6ad | 64 | # define constraintListBASESIZE SMALLBASESIZE |
65 | ||
66 | # else | |
67 | # error "Multiple include" | |
68 | # endif | |
69 | ||
70 | ||
71 | ||
72 |