/***** spin: spin.h *****/ /* Copyright (c) 1989-2009 by Lucent Technologies, Bell Laboratories. *//* All Rights Reserved. This software is for educational purposes only. *//* No guarantee whatsoever is expressed or implied by the distribution of *//* this code. Permission is given to distribute this code provided that *//* this introductory message is not removed and no monies are exchanged. *//* Software written by Gerard J. Holzmann. For tool documentation see: *//* http://spinroot.com/ *//* Send all bug-reports and/or questions to: bugs@spinroot.com */ #ifndef SEEN_SPIN_H#define SEEN_SPIN_H #include <stdio.h>#include <string.h>#include <ctype.h> enum { INIV, PUTV, LOGV }; /* for pangen[14].c */enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE }; typedef struct Lextok { unsigned short ntyp; /* node type */ short ismtyp; /* CONST derived from MTYP */ int val; /* value attribute */ int ln; /* line number */ int indstep; /* part of d_step sequence */ int uiid; /* inline id, if non-zero */ struct Symbol *fn; /* file name */ struct Symbol *sym; /* symbol reference */ struct Sequence *sq; /* sequence */ struct SeqList *sl; /* sequence list */ struct Lextok *lft, *rgt; /* children in parse tree */} Lextok; typedef struct Slicer { Lextok *n; /* global var, usable as slice criterion */ short code; /* type of use: DEREF_USE or normal USE */ short used; /* set when handled */ struct Slicer *nxt; /* linked list */} Slicer; typedef struct Access { struct Symbol *who; /* proctype name of accessor */ struct Symbol *what; /* proctype name of accessed */ int cnt, typ; /* parameter nr and, e.g., 's' or 'r' */ struct Access *lnk; /* linked list */} Access; typedef struct Symbol { char *name; int Nid; /* unique number for the name */ unsigned short type; /* bit,short,.., chan,struct */ unsigned char hidden; /* bit-flags: 1=hide, 2=show, 4=bit-equiv, 8=byte-equiv, 16=formal par, 32=inline par, 64=treat as if local; 128=read at least once */ unsigned char colnr; /* for use with xspin during simulation */ unsigned char isarray; /* set if decl specifies array bound */ unsigned char *bscp; /* block scope */ int nbits; /* optional width specifier */ int nel; /* 1 if scalar, >1 if array */ int setat; /* last depth value changed */ int *val; /* runtime value(s), initl 0 */ Lextok **Sval; /* values for structures */ int xu; /* exclusive r or w by 1 pid */ struct Symbol *xup[2]; /* xr or xs proctype */ struct Access *access;/* e.g., senders and receives of chan */ Lextok *ini; /* initial value, or chan-def */ Lextok *Slst; /* template for structure if struct */ struct Symbol *Snm; /* name of the defining struct */ struct Symbol *owner; /* set for names of subfields in typedefs */ struct Symbol *context; /* 0 if global, or procname */ struct Symbol *next; /* linked list */} Symbol; typedef struct Ordered { /* links all names in Symbol table */ struct Symbol *entry; struct Ordered *next;} Ordered; typedef struct Queue { short qid; /* runtime q index */ int qlen; /* nr messages stored */ int nslots, nflds; /* capacity, flds/slot */ int setat; /* last depth value changed */ int *fld_width; /* type of each field */ int *contents; /* the values stored */ int *stepnr; /* depth when each msg was sent */ struct Queue *nxt; /* linked list */} Queue; typedef struct FSM_state { /* used in pangen5.c - dataflow */ int from; /* state number */ int seen; /* used for dfs */ int in; /* nr of incoming edges */ int cr; /* has reachable 1-relevant successor */ int scratch; unsigned long *dom, *mod; /* to mark dominant nodes */ struct FSM_trans *t; /* outgoing edges */ struct FSM_trans *p; /* incoming edges, predecessors */ struct FSM_state *nxt; /* linked list of all states */} FSM_state; typedef struct FSM_trans { /* used in pangen5.c - dataflow */ int to; short relevant; /* when sliced */ short round; /* ditto: iteration when marked */ struct FSM_use *Val[2]; /* 0=reads, 1=writes */ struct Element *step; struct FSM_trans *nxt;} FSM_trans; typedef struct FSM_use { /* used in pangen5.c - dataflow */ Lextok *n; Symbol *var; int special; struct FSM_use *nxt;} FSM_use; typedef struct Element { Lextok *n; /* defines the type & contents */ int Seqno; /* identifies this el within system */ int seqno; /* identifies this el within a proc */ int merge; /* set by -O if step can be merged */ int merge_start; int merge_single; short merge_in; /* nr of incoming edges */ short merge_mark; /* state was generated in merge sequence */ unsigned int status; /* used by analyzer generator */ struct FSM_use *dead; /* optional dead variable list */ struct SeqList *sub; /* subsequences, for compounds */ struct SeqList *esc; /* zero or more escape sequences */ struct Element *Nxt; /* linked list - for global lookup */ struct Element *nxt; /* linked list - program structure */} Element; typedef struct Sequence { Element *frst; Element *last; /* links onto continuations */ Element *extent; /* last element in original */ int maxel; /* 1+largest id in sequence */} Sequence; typedef struct SeqList { Sequence *this; /* one sequence */ struct SeqList *nxt; /* linked list */} SeqList; typedef struct Label { Symbol *s; Symbol *c; Element *e; int uiid; /* non-zero if label appears in an inline */ int visible; /* label referenced in claim (slice relevant) */ struct Label *nxt;} Label; typedef struct Lbreak { Symbol *l; struct Lbreak *nxt;} Lbreak; typedef struct RunList { Symbol *n; /* name */ int tn; /* ordinal of type */ int pid; /* process id */ int priority; /* for simulations only */ enum btypes b; /* the type of process */ Element *pc; /* current stmnt */ Sequence *ps; /* used by analyzer generator */ Lextok *prov; /* provided clause */ Symbol *symtab; /* local variables */ struct RunList *nxt; /* linked list */} RunList; typedef struct ProcList { Symbol *n; /* name */ Lextok *p; /* parameters */ Sequence *s; /* body */ Lextok *prov; /* provided clause */ enum btypes b; /* e.g., claim, trace, proc */ short tn; /* ordinal number */ unsigned char det; /* deterministic */ unsigned char unsafe; /* contains global var inits */ struct ProcList *nxt; /* linked list */} ProcList; typedef Lextok *Lexptr; #define YYSTYPE Lexptr #define ZN (Lextok *)0#define ZS (Symbol *)0#define ZE (Element *)0 #define DONE 1 /* status bits of elements */#define ATOM 2 /* part of an atomic chain */#define L_ATOM 4 /* last element in a chain */#define I_GLOB 8 /* inherited global ref */#define DONE2 16 /* used in putcode and main*/#define D_ATOM 32 /* deterministic atomic */#define ENDSTATE 64 /* normal endstate */#define CHECK2 128 /* status bits for remote ref check */#define CHECK3 256 /* status bits for atomic jump check */ #define Nhash 255 /* slots in symbol hash-table */ #define XR 1 /* non-shared receive-only */#define XS 2 /* non-shared send-only */#define XX 4 /* overrides XR or XS tag */ #define CODE_FRAG 2 /* auto-numbered code-fragment */#define CODE_DECL 4 /* auto-numbered c_decl */#define PREDEF 3 /* predefined name: _p, _last */ #define UNSIGNED 5 /* val defines width in bits */#define BIT 1 /* also equal to width in bits */#define BYTE 8 /* ditto */#define SHORT 16 /* ditto */#define INT 32 /* ditto */#define CHAN 64 /* not */#define STRUCT 128 /* user defined structure name */ #define SOMETHINGBIG 65536#define RATHERSMALL 512#define MAXSCOPESZ 1024 #ifndef max#define max(a,b) (((a)<(b)) ? (b) : (a))#endif #ifdef PC #define MFLAGS "wb"#else #define MFLAGS "w"#endif /***** prototype definitions *****/Element *eval_sub(Element *);Element *get_lab(Lextok *, int);Element *huntele(Element *, int, int);Element *huntstart(Element *);Element *target(Element *); Lextok *do_unless(Lextok *, Lextok *);Lextok *expand(Lextok *, int);Lextok *getuname(Symbol *);Lextok *mk_explicit(Lextok *, int, int);Lextok *nn(Lextok *, int, Lextok *, Lextok *);Lextok *rem_lab(Symbol *, Lextok *, Symbol *);Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);Lextok *tail_add(Lextok *, Lextok *); ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes); SeqList *seqlist(Sequence *, SeqList *);Sequence *close_seq(int); Symbol *break_dest(void);Symbol *findloc(Symbol *);Symbol *has_lab(Element *, int);Symbol *lookup(char *);Symbol *prep_inline(Symbol *, Lextok *); char *emalloc(size_t);long Rand(void); int any_oper(Lextok *, int);int any_undo(Lextok *);int c_add_sv(FILE *);int cast_val(int, int, int);int checkvar(Symbol *, int);int Cnt_flds(Lextok *);int cnt_mpars(Lextok *);int complete_rendez(void);int enable(Lextok *);int Enabled0(Element *);int eval(Lextok *);int find_lab(Symbol *, Symbol *, int);int find_maxel(Symbol *);int full_name(FILE *, Lextok *, Symbol *, int);int getlocal(Lextok *);int getval(Lextok *);int glob_inline(char *);int has_typ(Lextok *, int);int in_bound(Symbol *, int);int interprint(FILE *, Lextok *);int printm(FILE *, Lextok *);int is_inline(void);int ismtype(char *);int isproctype(char *);int isutype(char *);int Lval_struct(Lextok *, Symbol *, int, int);int main(int, char **);int pc_value(Lextok *);int pid_is_claim(int);int proper_enabler(Lextok *);int putcode(FILE *, Sequence *, Element *, int, int, int);int q_is_sync(Lextok *);int qlen(Lextok *);int qfull(Lextok *);int qmake(Symbol *);int qrecv(Lextok *, int);int qsend(Lextok *);int remotelab(Lextok *);int remotevar(Lextok *);int Rval_struct(Lextok *, Symbol *, int);int setlocal(Lextok *, int);int setval(Lextok *, int);int sputtype(char *, int);int Sym_typ(Lextok *);int tl_main(int, char *[]);int Width_set(int *, int, Lextok *);int yyparse(void);int yywrap(void);int yylex(void); void AST_track(Lextok *, int);void add_seq(Lextok *);void alldone(int);void announce(char *);void c_state(Symbol *, Symbol *, Symbol *);void c_add_def(FILE *);void c_add_loc(FILE *, char *);void c_add_locinit(FILE *, int, char *);void c_add_use(FILE *);void c_chandump(FILE *);void c_preview(void);void c_struct(FILE *, char *, Symbol *);void c_track(Symbol *, Symbol *, Symbol *);void c_var(FILE *, char *, Symbol *);void c_wrapper(FILE *);void chanaccess(void);void check_param_count(int, Lextok *);void checkrun(Symbol *, int);void comment(FILE *, Lextok *, int);void cross_dsteps(Lextok *, Lextok *);void disambiguate(void);void doq(Symbol *, int, RunList *);void dotag(FILE *, char *);void do_locinits(FILE *);void do_var(FILE *, int, char *, Symbol *, char *, char *, char *);void dump_struct(Symbol *, char *, RunList *);void dumpclaims(FILE *, int, char *);void dumpglobals(void);void dumplabels(void);void dumplocal(RunList *);void dumpsrc(int, int);void fatal(char *, char *);void fix_dest(Symbol *, Symbol *);void genaddproc(void);void genaddqueue(void);void gencodetable(FILE *);void genheader(void);void genother(void);void gensrc(void);void gensvmap(void);void genunio(void);void ini_struct(Symbol *);void loose_ends(void);void make_atomic(Sequence *, int);void match_trail(void);void no_side_effects(char *);void nochan_manip(Lextok *, Lextok *, int);void non_fatal(char *, char *);void ntimes(FILE *, int, int, char *c[]);void open_seq(int);void p_talk(Element *, int);void pickup_inline(Symbol *, Lextok *);void plunk_c_decls(FILE *);void plunk_c_fcts(FILE *);void plunk_expr(FILE *, char *);void plunk_inline(FILE *, char *, int, int);void prehint(Symbol *);void preruse(FILE *, Lextok *);void prune_opts(Lextok *);void pstext(int, char *);void pushbreak(void);void putname(FILE *, char *, Lextok *, int, char *);void putremote(FILE *, Lextok *, int);void putskip(int);void putsrc(Element *);void putstmnt(FILE *, Lextok *, int);void putunames(FILE *);void rem_Seq(void);void runnable(ProcList *, int, int);void sched(void);void setaccess(Symbol *, Symbol *, int, int);void set_lab(Symbol *, Element *);void setmtype(Lextok *);void setpname(Lextok *);void setptype(Lextok *, int, Lextok *);void setuname(Lextok *);void setutype(Lextok *, Symbol *, Lextok *);void setxus(Lextok *, int);void show_lab(void);void Srand(unsigned);void start_claim(int);void struct_name(Lextok *, Symbol *, int, char *);void symdump(void);void symvar(Symbol *);void sync_product(void);void trackchanuse(Lextok *, Lextok *, int);void trackvar(Lextok *, Lextok *);void trackrun(Lextok *);void trapwonly(Lextok * /* , char * */); /* spin.y and main.c */void typ2c(Symbol *);void typ_ck(int, int, char *);void undostmnt(Lextok *, int);void unrem_Seq(void);void unskip(int);void varcheck(Element *, Element *);void whoruns(int);void wrapup(int);void yyerror(char *, ...);#endif
/***** spin: spin.h *****/
/* Copyright (c) 1989-2009 by Lucent Technologies, Bell Laboratories. */
/* All Rights Reserved. This software is for educational purposes only. */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code. Permission is given to distribute this code provided that */
/* this introductory message is not removed and no monies are exchanged. */
/* Software written by Gerard J. Holzmann. For tool documentation see: */
/* http://spinroot.com/ */
/* Send all bug-reports and/or questions to: bugs@spinroot.com */
#ifndef SEEN_SPIN_H
#define SEEN_SPIN_H
#include <stdio.h>
#include <string.h>
#include <ctype.h>
enum { INIV, PUTV, LOGV }; /* for pangen[14].c */
enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };
typedef struct Lextok {
unsigned short ntyp; /* node type */
short ismtyp; /* CONST derived from MTYP */
int val; /* value attribute */
int ln; /* line number */
int indstep; /* part of d_step sequence */
int uiid; /* inline id, if non-zero */
struct Symbol *fn; /* file name */
struct Symbol *sym; /* symbol reference */
struct Sequence *sq; /* sequence */
struct SeqList *sl; /* sequence list */
struct Lextok *lft, *rgt; /* children in parse tree */
} Lextok;
typedef struct Slicer {
Lextok *n; /* global var, usable as slice criterion */
short code; /* type of use: DEREF_USE or normal USE */
short used; /* set when handled */
struct Slicer *nxt; /* linked list */
} Slicer;
typedef struct Access {
struct Symbol *who; /* proctype name of accessor */
struct Symbol *what; /* proctype name of accessed */
int cnt, typ; /* parameter nr and, e.g., 's' or 'r' */
struct Access *lnk; /* linked list */
} Access;
typedef struct Symbol {
char *name;
int Nid; /* unique number for the name */
unsigned short type; /* bit,short,.., chan,struct */
unsigned char hidden; /* bit-flags:
1=hide, 2=show,
4=bit-equiv, 8=byte-equiv,
16=formal par, 32=inline par,
64=treat as if local; 128=read at least once
*/
unsigned char colnr; /* for use with xspin during simulation */
unsigned char isarray; /* set if decl specifies array bound */
unsigned char *bscp; /* block scope */
int nbits; /* optional width specifier */
int nel; /* 1 if scalar, >1 if array */
int setat; /* last depth value changed */
int *val; /* runtime value(s), initl 0 */
Lextok **Sval; /* values for structures */
int xu; /* exclusive r or w by 1 pid */
struct Symbol *xup[2]; /* xr or xs proctype */
struct Access *access;/* e.g., senders and receives of chan */
Lextok *ini; /* initial value, or chan-def */
Lextok *Slst; /* template for structure if struct */
struct Symbol *Snm; /* name of the defining struct */
struct Symbol *owner; /* set for names of subfields in typedefs */
struct Symbol *context; /* 0 if global, or procname */
struct Symbol *next; /* linked list */
} Symbol;
typedef struct Ordered { /* links all names in Symbol table */
struct Symbol *entry;
struct Ordered *next;
} Ordered;
typedef struct Queue {
short qid; /* runtime q index */
int qlen; /* nr messages stored */
int nslots, nflds; /* capacity, flds/slot */
int setat; /* last depth value changed */
int *fld_width; /* type of each field */
int *contents; /* the values stored */
int *stepnr; /* depth when each msg was sent */
struct Queue *nxt; /* linked list */
} Queue;
typedef struct FSM_state { /* used in pangen5.c - dataflow */
int from; /* state number */
int seen; /* used for dfs */
int in; /* nr of incoming edges */
int cr; /* has reachable 1-relevant successor */
int scratch;
unsigned long *dom, *mod; /* to mark dominant nodes */
struct FSM_trans *t; /* outgoing edges */
struct FSM_trans *p; /* incoming edges, predecessors */
struct FSM_state *nxt; /* linked list of all states */
} FSM_state;
typedef struct FSM_trans { /* used in pangen5.c - dataflow */
int to;
short relevant; /* when sliced */
short round; /* ditto: iteration when marked */
struct FSM_use *Val[2]; /* 0=reads, 1=writes */
struct Element *step;
struct FSM_trans *nxt;
} FSM_trans;
typedef struct FSM_use { /* used in pangen5.c - dataflow */
Lextok *n;
Symbol *var;
int special;
struct FSM_use *nxt;
} FSM_use;
typedef struct Element {
Lextok *n; /* defines the type & contents */
int Seqno; /* identifies this el within system */
int seqno; /* identifies this el within a proc */
int merge; /* set by -O if step can be merged */
int merge_start;
int merge_single;
short merge_in; /* nr of incoming edges */
short merge_mark; /* state was generated in merge sequence */
unsigned int status; /* used by analyzer generator */
struct FSM_use *dead; /* optional dead variable list */
struct SeqList *sub; /* subsequences, for compounds */
struct SeqList *esc; /* zero or more escape sequences */
struct Element *Nxt; /* linked list - for global lookup */
struct Element *nxt; /* linked list - program structure */
} Element;
typedef struct Sequence {
Element *frst;
Element *last; /* links onto continuations */
Element *extent; /* last element in original */
int maxel; /* 1+largest id in sequence */
} Sequence;
typedef struct SeqList {
Sequence *this; /* one sequence */
struct SeqList *nxt; /* linked list */
} SeqList;
typedef struct Label {
Symbol *s;
Symbol *c;
Element *e;
int uiid; /* non-zero if label appears in an inline */
int visible; /* label referenced in claim (slice relevant) */
struct Label *nxt;
} Label;
typedef struct Lbreak {
Symbol *l;
struct Lbreak *nxt;
} Lbreak;
typedef struct RunList {
Symbol *n; /* name */
int tn; /* ordinal of type */
int pid; /* process id */
int priority; /* for simulations only */
enum btypes b; /* the type of process */
Element *pc; /* current stmnt */
Sequence *ps; /* used by analyzer generator */
Lextok *prov; /* provided clause */
Symbol *symtab; /* local variables */
struct RunList *nxt; /* linked list */
} RunList;
typedef struct ProcList {
Symbol *n; /* name */
Lextok *p; /* parameters */
Sequence *s; /* body */
Lextok *prov; /* provided clause */
enum btypes b; /* e.g., claim, trace, proc */
short tn; /* ordinal number */
unsigned char det; /* deterministic */
unsigned char unsafe; /* contains global var inits */
struct ProcList *nxt; /* linked list */
} ProcList;
typedef Lextok *Lexptr;
#define YYSTYPE Lexptr
#define ZN (Lextok *)0
#define ZS (Symbol *)0
#define ZE (Element *)0
#define DONE 1 /* status bits of elements */
#define ATOM 2 /* part of an atomic chain */
#define L_ATOM 4 /* last element in a chain */
#define I_GLOB 8 /* inherited global ref */
#define DONE2 16 /* used in putcode and main*/
#define D_ATOM 32 /* deterministic atomic */
#define ENDSTATE 64 /* normal endstate */
#define CHECK2 128 /* status bits for remote ref check */
#define CHECK3 256 /* status bits for atomic jump check */
#define Nhash 255 /* slots in symbol hash-table */
#define XR 1 /* non-shared receive-only */
#define XS 2 /* non-shared send-only */
#define XX 4 /* overrides XR or XS tag */
#define CODE_FRAG 2 /* auto-numbered code-fragment */
#define CODE_DECL 4 /* auto-numbered c_decl */
#define PREDEF 3 /* predefined name: _p, _last */
#define UNSIGNED 5 /* val defines width in bits */
#define BIT 1 /* also equal to width in bits */
#define BYTE 8 /* ditto */
#define SHORT 16 /* ditto */
#define INT 32 /* ditto */
#define CHAN 64 /* not */
#define STRUCT 128 /* user defined structure name */
#define SOMETHINGBIG 65536
#define RATHERSMALL 512
#define MAXSCOPESZ 1024
#ifndef max
#define max(a,b) (((a)<(b)) ? (b) : (a))
#endif
#ifdef PC
#define MFLAGS "wb"
#else
#define MFLAGS "w"
#endif
/***** prototype definitions *****/
Element *eval_sub(Element *);
Element *get_lab(Lextok *, int);
Element *huntele(Element *, int, int);
Element *huntstart(Element *);
Element *target(Element *);
Lextok *do_unless(Lextok *, Lextok *);
Lextok *expand(Lextok *, int);
Lextok *getuname(Symbol *);
Lextok *mk_explicit(Lextok *, int, int);
Lextok *nn(Lextok *, int, Lextok *, Lextok *);
Lextok *rem_lab(Symbol *, Lextok *, Symbol *);
Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
Lextok *tail_add(Lextok *, Lextok *);
ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);
SeqList *seqlist(Sequence *, SeqList *);
Sequence *close_seq(int);
Symbol *break_dest(void);
Symbol *findloc(Symbol *);
Symbol *has_lab(Element *, int);
Symbol *lookup(char *);
Symbol *prep_inline(Symbol *, Lextok *);
char *emalloc(size_t);
long Rand(void);
int any_oper(Lextok *, int);
int any_undo(Lextok *);
int c_add_sv(FILE *);
int cast_val(int, int, int);
int checkvar(Symbol *, int);
int Cnt_flds(Lextok *);
int cnt_mpars(Lextok *);
int complete_rendez(void);
int enable(Lextok *);
int Enabled0(Element *);
int eval(Lextok *);
int find_lab(Symbol *, Symbol *, int);
int find_maxel(Symbol *);
int full_name(FILE *, Lextok *, Symbol *, int);
int getlocal(Lextok *);
int getval(Lextok *);
int glob_inline(char *);
int has_typ(Lextok *, int);
int in_bound(Symbol *, int);
int interprint(FILE *, Lextok *);
int printm(FILE *, Lextok *);
int is_inline(void);
int ismtype(char *);
int isproctype(char *);
int isutype(char *);
int Lval_struct(Lextok *, Symbol *, int, int);
int main(int, char **);
int pc_value(Lextok *);
int pid_is_claim(int);
int proper_enabler(Lextok *);
int putcode(FILE *, Sequence *, Element *, int, int, int);
int q_is_sync(Lextok *);
int qlen(Lextok *);
int qfull(Lextok *);
int qmake(Symbol *);
int qrecv(Lextok *, int);
int qsend(Lextok *);
int remotelab(Lextok *);
int remotevar(Lextok *);
int Rval_struct(Lextok *, Symbol *, int);
int setlocal(Lextok *, int);
int setval(Lextok *, int);
int sputtype(char *, int);
int Sym_typ(Lextok *);
int tl_main(int, char *[]);
int Width_set(int *, int, Lextok *);
int yyparse(void);
int yywrap(void);
int yylex(void);
void AST_track(Lextok *, int);
void add_seq(Lextok *);
void alldone(int);
void announce(char *);
void c_state(Symbol *, Symbol *, Symbol *);
void c_add_def(FILE *);
void c_add_loc(FILE *, char *);
void c_add_locinit(FILE *, int, char *);
void c_add_use(FILE *);
void c_chandump(FILE *);
void c_preview(void);
void c_struct(FILE *, char *, Symbol *);
void c_track(Symbol *, Symbol *, Symbol *);
void c_var(FILE *, char *, Symbol *);
void c_wrapper(FILE *);
void chanaccess(void);
void check_param_count(int, Lextok *);
void checkrun(Symbol *, int);
void comment(FILE *, Lextok *, int);
void cross_dsteps(Lextok *, Lextok *);
void disambiguate(void);
void doq(Symbol *, int, RunList *);
void dotag(FILE *, char *);
void do_locinits(FILE *);
void do_var(FILE *, int, char *, Symbol *, char *, char *, char *);
void dump_struct(Symbol *, char *, RunList *);
void dumpclaims(FILE *, int, char *);
void dumpglobals(void);
void dumplabels(void);
void dumplocal(RunList *);
void dumpsrc(int, int);
void fatal(char *, char *);
void fix_dest(Symbol *, Symbol *);
void genaddproc(void);
void genaddqueue(void);
void gencodetable(FILE *);
void genheader(void);
void genother(void);
void gensrc(void);
void gensvmap(void);
void genunio(void);
void ini_struct(Symbol *);
void loose_ends(void);
void make_atomic(Sequence *, int);
void match_trail(void);
void no_side_effects(char *);
void nochan_manip(Lextok *, Lextok *, int);
void non_fatal(char *, char *);
void ntimes(FILE *, int, int, char *c[]);
void open_seq(int);
void p_talk(Element *, int);
void pickup_inline(Symbol *, Lextok *);
void plunk_c_decls(FILE *);
void plunk_c_fcts(FILE *);
void plunk_expr(FILE *, char *);
void plunk_inline(FILE *, char *, int, int);
void prehint(Symbol *);
void preruse(FILE *, Lextok *);
void prune_opts(Lextok *);
void pstext(int, char *);
void pushbreak(void);
void putname(FILE *, char *, Lextok *, int, char *);
void putremote(FILE *, Lextok *, int);
void putskip(int);
void putsrc(Element *);
void putstmnt(FILE *, Lextok *, int);
void putunames(FILE *);
void rem_Seq(void);
void runnable(ProcList *, int, int);
void sched(void);
void setaccess(Symbol *, Symbol *, int, int);
void set_lab(Symbol *, Element *);
void setmtype(Lextok *);
void setpname(Lextok *);
void setptype(Lextok *, int, Lextok *);
void setuname(Lextok *);
void setutype(Lextok *, Symbol *, Lextok *);
void setxus(Lextok *, int);
void show_lab(void);
void Srand(unsigned);
void start_claim(int);
void struct_name(Lextok *, Symbol *, int, char *);
void symdump(void);
void symvar(Symbol *);
void sync_product(void);
void trackchanuse(Lextok *, Lextok *, int);
void trackvar(Lextok *, Lextok *);
void trackrun(Lextok *);
void trapwonly(Lextok * /* , char * */); /* spin.y and main.c */
void typ2c(Symbol *);
void typ_ck(int, int, char *);
void undostmnt(Lextok *, int);
void unrem_Seq(void);
void unskip(int);
void varcheck(Element *, Element *);
void whoruns(int);
void wrapup(int);
void yyerror(char *, ...);
#endif