Various minor fixes for compiler/linter (other then splint itself) warnings.
[splint-patched.git] / src / Headers / stateClauseList.h
blob39e6ccf178459af6a54b7965b8bc7a04437737d4
1 /*
2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
3 ** See ../LICENSE for license information.
4 */
5 /*
6 ** stateClauseList.h
7 */
9 # ifndef STATECLAUSELIST_H
10 # define STATECLAUSELIST_H
12 struct s_stateClauseList
14 int nelements;
15 int nspace;
16 /*@relnull@*/ /*@reldef@*/ o_stateClause *elements;
17 } ;
19 extern void stateClauseList_checkAll (uentry p_ue)
20 /*@modifies p_ue, g_warningstream@*/ ;
22 /*@constant null stateClauseList stateClauseList_undefined@*/
23 # define stateClauseList_undefined ((stateClauseList) 0)
25 extern /*@falsewhennull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ;
26 # define stateClauseList_isDefined(s) ((s) != stateClauseList_undefined)
28 extern /*@nullwhentrue@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ;
29 # define stateClauseList_isUndefined(s) ((s) == stateClauseList_undefined)
31 extern /*@unused@*/ int
32 stateClauseList_size (/*@sef@*/ stateClauseList p_s) /*@*/ ;
33 # define stateClauseList_size(s) (stateClauseList_isDefined (s) ? (s)->nelements : 0)
35 extern cstring stateClause_unparseKind (stateClause p_s) /*@*/ ;
37 extern stateClauseList
38 stateClauseList_add (/*@returned@*/ stateClauseList p_s,
39 /*@only@*/ stateClause p_el)
40 /*@modifies p_s@*/ ;
42 extern /*@unused@*/ cstring stateClauseList_unparse (stateClauseList p_s) /*@*/ ;
43 extern void stateClauseList_free (/*@only@*/ stateClauseList p_s) ;
45 extern /*@only@*/ stateClauseList stateClauseList_copy (stateClauseList p_s) /*@*/ ;
47 extern cstring stateClauseList_dump (stateClauseList p_s) /*@*/ ;
48 extern stateClauseList stateClauseList_undump (char **p_s) /*@modifies *p_s@*/ ;
50 extern void stateClauseList_checkEqual (uentry p_old, uentry p_unew)
51 /*@modifies g_warningstream@*/ ;
53 /*@iter stateClauseList_elements (sef stateClauseList x, yield exposed stateClause el); @*/
54 # define stateClauseList_elements(x, m_el) \
55 { if (!stateClauseList_isUndefined(x)) \
56 { int m_ind; stateClause *m_elements = &((x)->elements[0]); \
57 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
58 { stateClause m_el = *(m_elements++);
60 # define end_stateClauseList_elements }}}
62 /*@iter stateClauseList_preElements (sef stateClauseList x, yield exposed stateClause el); @*/
63 # define stateClauseList_preElements(x, m_el) \
64 { if (!stateClauseList_isUndefined(x)) \
65 { int m_ind; stateClause *m_elements = &((x)->elements[0]); \
66 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
67 { stateClause m_el = *(m_elements++); if (stateClause_isBefore (m_el)) { \
69 # define end_stateClauseList_preElements }}}}
71 /*@iter stateClauseList_postElements (sef stateClauseList x, yield exposed stateClause el); @*/
72 # define stateClauseList_postElements(x, m_el) \
73 { if (!stateClauseList_isUndefined(x)) \
74 { int m_ind; stateClause *m_elements = &((x)->elements[0]); \
75 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
76 { stateClause m_el = *(m_elements++); if (stateClause_isAfter (m_el)) { \
78 # define end_stateClauseList_postElements }}}}
80 # else
81 # error "Multiple include"
82 # endif