[splint.git] / src / Headers / stateInfo.h

/*
** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
*/
/*
** stateInfo.h
*/

# ifndef STATEINFO_H
# define STATEINFO_H

typedef /*@null@*/ struct s_stateInfo *stateInfo ;

typedef enum {
  SA_UNKNOWN,

  /* Any type of action */
  SA_CREATED,
  SA_DECLARED,
  SA_CHANGED,

  /* Definition actions */
  SA_UNDEFINED,
  SA_MUNDEFINED,
  SA_PDEFINED,
  SA_DEFINED,
  SA_RELEASED,
  SA_ALLOCATED,
  SA_KILLED,
  SA_PKILLED,
  SA_MERGED,

  /* sharing actions */
  SA_SHARED,
  SA_ONLY,
  SA_IMPONLY,
  SA_OWNED,
  SA_DEPENDENT,
  SA_IMPDEPENDENT,
  SA_KEPT,
  SA_KEEP,
  SA_FRESH,
  SA_XSTACK, /* SA_STACK is defined in some Linux headers (but ISO does not reserve this namespace) */
  SA_TEMP,
  SA_IMPTEMP,
  SA_STATIC,
  SA_LOCAL,

  SA_REFCOUNTED,
  SA_REFS,
  SA_NEWREF,
  SA_KILLREF,

  /* exposure */
  SA_EXPOSED,
  SA_OBSERVER,

  /* nullity actions */
  SA_BECOMESNULL,
  SA_BECOMESNONNULL,
  SA_BECOMESPOSSIBLYNULL,

} stateAction;

/*@null@*/ struct s_stateInfo
{
  /*@only@*/ fileloc loc;
  stateAction action;
  /*@observer@*/ sRef ref;
  /*@null@*/ stateInfo previous;
} ;

/*@constant null stateInfo stateInfo_undefined@*/
# define stateInfo_undefined (NULL)

extern /*@falsewhennull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ;
# define stateInfo_isDefined(p_s) ((p_s) != stateInfo_undefined)

extern void stateInfo_free (/*@only@*/ stateInfo p_a);

extern /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo p_old, stateInfo p_newinfo);

extern /*@only@*/ stateInfo stateInfo_updateLoc (/*@only@*/ stateInfo p_old, 
						 stateAction p_action,
						 fileloc p_loc) ;

extern /*@only@*/ stateInfo 
    stateInfo_updateRefLoc (/*@only@*/ stateInfo p_old, /*@exposed@*/ sRef p_ref, 
			    stateAction p_action,
			    fileloc p_loc) ;

extern /*@only@*/ stateInfo stateInfo_copy (stateInfo p_a); 

extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) ;

extern /*@only@*/ /*@notnull@*/ stateInfo
stateInfo_makeLoc (fileloc p_loc, stateAction p_action) /*@*/ ;

extern /*@only@*/ /*@notnull@*/ stateInfo 
stateInfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc, stateAction p_action) /*@*/ ; 

extern /*@observer@*/ fileloc stateInfo_getLoc (stateInfo p_info) ;
extern /*@only@*/ cstring stateInfo_unparse (stateInfo p_s) /*@*/ ;

extern stateAction stateAction_fromSState (sstate p_ss) /*@*/ ;
extern stateAction stateAction_fromNState (nstate p_ns) /*@*/ ;
extern stateAction stateAction_fromExkind (exkind p_ex) /*@*/ ;
extern stateAction stateAction_fromAlkind (alkind p_ak) /*@*/ ;

extern void stateInfo_display (stateInfo p_s, /*@only@*/ cstring p_sname) 
  /*@modifies g_errorstream@*/ ;

# else
# error "Multiple include"
# endif
Commit	Line	Data
28bf4b0b	1	/*
c0de361f	2	** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
28bf4b0b	3	** See ../LICENSE for license information.
	4	*/
	5	/*
	6	** stateInfo.h
	7	*/
	8
	9	# ifndef STATEINFO_H
	10	# define STATEINFO_H
	11
6fcd0b1e	12	typedef /@null@/ struct s_stateInfo *stateInfo ;
6fcd0b1e	13
16c024b5	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;
6fcd0b1e	64
6fcd0b1e	65	/@null@/ struct s_stateInfo
28bf4b0b	66	{
16c024b5	67	/@only@/ fileloc loc;
16c024b5	68	stateAction action;
28bf4b0b	69	/@observer@/ sRef ref;
6fcd0b1e	70	/@null@/ stateInfo previous;
6fcd0b1e	71	} ;
28bf4b0b	72
	73	/@constant null stateInfo stateInfo_undefined@/
	74	# define stateInfo_undefined (NULL)
	75
0e41eb0e	76	extern /@falsewhennull@/ bool stateInfo_isDefined (stateInfo p_s) /@/ ;
28bf4b0b	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
16c024b5	83	extern /@only@/ stateInfo stateInfo_updateLoc (/@only@/ stateInfo p_old,
	84	stateAction p_action,
	85	fileloc p_loc) ;
28bf4b0b	86
28bf4b0b	87	extern /@only@/ stateInfo
16c024b5	88	stateInfo_updateRefLoc (/@only@/ stateInfo p_old, /@exposed@/ sRef p_ref,
	89	stateAction p_action,
	90	fileloc p_loc) ;
28bf4b0b	91
	92	extern /@only@/ stateInfo stateInfo_copy (stateInfo p_a);
	93
6970c11b	94	extern /@only@/ /@notnull@/ stateInfo stateInfo_currentLoc (void) ;
16c024b5	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) /@/ ;
28bf4b0b	101
	102	extern /@observer@/ fileloc stateInfo_getLoc (stateInfo p_info) ;
	103	extern /@only@/ cstring stateInfo_unparse (stateInfo p_s) /@/ ;
	104
16c024b5	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@/ ;
6fcd0b1e	112
28bf4b0b	113	# else
	114	# error "Multiple include"
	115	# endif