]>
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 | ||
6e88de2d | 28 | extern /*@only@*/ constraintList constraintList_makeNew(void) /*@*/; |
29 | extern constraintList constraintList_add (/*@returned@*/ constraintList p_s, /*@only@*/ constraint p_el) /*@modifies p_s@*/ ; | |
4cccc6ad | 30 | |
6e88de2d | 31 | extern constraintList constraintList_addList (/*@returned@*/ constraintList p_s, /*@only@*/constraintList new) /*@modifies p_s@*/ ; |
361091cc | 32 | |
33 | ||
103db890 | 34 | extern constraintList constraintList_copy (constraintList p_s) /*@*/ ; |
4cccc6ad | 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 | |
6e88de2d | 42 | extern cstring constraintList_print (constraintList s) /*@*/; |
754746a0 | 43 | |
44 | extern cstring | |
6e88de2d | 45 | constraintList_printDetailed (constraintList s) /*@*/; |
754746a0 | 46 | |
47 | ||
48 | extern constraintList | |
49 | constraintList_logicalOr (constraintList l1, constraintList l2); | |
50 | ||
6e88de2d | 51 | extern constraintList constraintList_preserveOrig (/*@returned@*/ constraintList c); |
754746a0 | 52 | |
4cccc6ad | 53 | /*@constant int constraintListBASESIZE;@*/ |
754746a0 | 54 | |
6e88de2d | 55 | extern constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, exprNodeList arglist) /*@modifies preconditions@*/; |
754746a0 | 56 | |
6e88de2d | 57 | extern constraintList constraintList_togglePost (/*@returned@*/ constraintList c) /*@modifies c@*/; |
ef2aa32a | 58 | |
6e88de2d | 59 | extern constraintList constraintList_doSRefFixConstraintParam (/*@returned@*/ constraintList preconditions, exprNodeList arglist) /*@modifies preconditions@*/; |
ef2aa32a | 60 | |
6e88de2d | 61 | extern constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) /*@*/; |
ef2aa32a | 62 | |
6e88de2d | 63 | constraintList constraintList_doFixResult (/*@returned@*/ constraintList postconditions, exprNode fcnCall) /*@modifies postconditions@*/; |
103db890 | 64 | |
6e88de2d | 65 | constraintList constraintList_addGeneratingExpr (/*@returned@*/ constraintList c, exprNode e) /*@modifies c@*/; |
4cccc6ad | 66 | # define constraintListBASESIZE SMALLBASESIZE |
67 | ||
68 | # else | |
69 | # error "Multiple include" | |
70 | # endif | |
71 | ||
72 | ||
73 | ||
74 |