1 /* 2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. 3 ** See ../LICENSE for license information. 4 */ 5 /* 6 ** stateInfo.h 7 */ 8 9 # ifndef STATEINFO_H 10 # define STATEINFO_H 11 12 typedef /*@null@*/ struct s_stateInfo *stateInfo ; 13 14 typedef enum { 15 SA_UNKNOWN, 16 17 /* Any type of action */ 18 SA_CREATED, 19 SA_DECLARED, 20 SA_CHANGED, 21 22 /* Definition actions */ 23 SA_UNDEFINED, 24 SA_MUNDEFINED, 25 SA_PDEFINED, 26 SA_DEFINED, 27 SA_RELEASED, 28 SA_ALLOCATED, 29 SA_KILLED, 30 SA_PKILLED, 31 SA_MERGED, 32 33 /* sharing actions */ 34 SA_SHARED, 35 SA_ONLY, 36 SA_IMPONLY, 37 SA_OWNED, 38 SA_DEPENDENT, 39 SA_IMPDEPENDENT, 40 SA_KEPT, 41 SA_KEEP, 42 SA_FRESH, 43 SA_XSTACK, /* SA_STACK is defined in some Linux headers (but ISO does not reserve this namespace) */ 44 SA_TEMP, 45 SA_IMPTEMP, 46 SA_STATIC, 47 SA_LOCAL, 48 49 SA_REFCOUNTED, 50 SA_REFS, 51 SA_NEWREF, 52 SA_KILLREF, 53 54 /* exposure */ 55 SA_EXPOSED, 56 SA_OBSERVER, 57 58 /* nullity actions */ 59 SA_BECOMESNULL, 60 SA_BECOMESNONNULL, 61 SA_BECOMESPOSSIBLYNULL, 62 63 } stateAction; 64 65 /*@null@*/ struct s_stateInfo 66 { 67 /*@only@*/ fileloc loc; 68 stateAction action; 69 /*@observer@*/ sRef ref; 70 /*@null@*/ stateInfo previous; 71 } ; 72 73 /*@constant null stateInfo stateInfo_undefined@*/ 74 # define stateInfo_undefined (NULL) 75 76 extern /*@falsewhennull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ; 77 # define stateInfo_isDefined(p_s) ((p_s) != stateInfo_undefined) 78 79 extern void stateInfo_free (/*@only@*/ stateInfo p_a); 80 81 extern /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo p_old, stateInfo p_newinfo); 82 83 extern /*@only@*/ stateInfo stateInfo_updateLoc (/*@only@*/ stateInfo p_old, 84 stateAction p_action, 85 fileloc p_loc) ; 86 87 extern /*@only@*/ stateInfo 88 stateInfo_updateRefLoc (/*@only@*/ stateInfo p_old, /*@exposed@*/ sRef p_ref, 89 stateAction p_action, 90 fileloc p_loc) ; 91 92 extern /*@only@*/ stateInfo stateInfo_copy (stateInfo p_a); 93 94 extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) ; 95 96 extern /*@only@*/ /*@notnull@*/ stateInfo 97 stateInfo_makeLoc (fileloc p_loc, stateAction p_action) /*@*/ ; 98 99 extern /*@only@*/ /*@notnull@*/ stateInfo 100 stateInfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc, stateAction p_action) /*@*/ ; 101 102 extern /*@observer@*/ fileloc stateInfo_getLoc (stateInfo p_info) ; 103 extern /*@only@*/ cstring stateInfo_unparse (stateInfo p_s) /*@*/ ; 104 105 extern stateAction stateAction_fromSState (sstate p_ss) /*@*/ ; 106 extern stateAction stateAction_fromNState (nstate p_ns) /*@*/ ; 107 extern stateAction stateAction_fromExkind (exkind p_ex) /*@*/ ; 108 extern stateAction stateAction_fromAlkind (alkind p_ak) /*@*/ ; 109 110 extern void stateInfo_display (stateInfo p_s, /*@only@*/ cstring p_sname) 111 /*@modifies g_errorstream@*/ ; 112 113 # else 114 # error "Multiple include" 115 # endif 116