/***** spin: spin.h *****/
-/* Copyright (c) 1989-2003 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 */
+/*
+ * This file is part of the public release of Spin. It is subject to the
+ * terms in the LICENSE file that is included in this source directory.
+ * Tool documentation is available at http://spinroot.com
+ */
#ifndef SEEN_SPIN_H
#define SEEN_SPIN_H
#include <stdio.h>
#include <string.h>
#include <ctype.h>
+#if !defined(WIN32) && !defined(WIN64)
+ #include <unistd.h>
+#endif
+#if !defined(PC) && !defined(_PLAN9)
+ #include <memory.h>
+#endif
+
+enum { INIV, PUTV, LOGV }; /* used in pangen1.c */
+enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };
typedef struct Lextok {
unsigned short ntyp; /* node type */
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 */
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 sc; /* scope seq no -- set only for proctypes */
int nbits; /* optional width specifier */
int nel; /* 1 if scalar, >1 if array */
int setat; /* last depth value changed */
int merge_single;
short merge_in; /* nr of incoming edges */
short merge_mark; /* state was generated in merge sequence */
- unsigned char status; /* used by analyzer generator */
+ 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 */
Element *frst;
Element *last; /* links onto continuations */
Element *extent; /* last element in original */
+ int minel; /* minimum Seqno, set and used only in guided.c */
int maxel; /* 1+largest id in sequence */
} Sequence;
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;
struct Lbreak *nxt;
} Lbreak;
+typedef struct L_List {
+ Lextok *n;
+ struct L_List *nxt;
+} L_List;
+
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 */
Lextok *p; /* parameters */
Sequence *s; /* body */
Lextok *prov; /* provided clause */
+ enum btypes b; /* e.g., claim, trace, proc */
short tn; /* ordinal number */
- short det; /* deterministic */
+ unsigned char det; /* deterministic */
+ unsigned char unsafe; /* contains global var inits */
+ unsigned char priority; /* process priority, if any */
struct ProcList *nxt; /* linked list */
} ProcList;
+typedef struct QH {
+ int n;
+ struct QH *nxt;
+} QH;
+
typedef Lextok *Lexptr;
#define YYSTYPE Lexptr
#define DONE2 16 /* used in putcode and main*/
#define D_ATOM 32 /* deterministic atomic */
#define ENDSTATE 64 /* normal endstate */
-#define CHECK2 128
+#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 SOMETHINGBIG 65536
#define RATHERSMALL 512
+#define MAXSCOPESZ 1024
#ifndef max
-#define max(a,b) (((a)<(b)) ? (b) : (a))
+ #define max(a,b) (((a)<(b)) ? (b) : (a))
#endif
-enum { INIV, PUTV, LOGV }; /* for pangen[14].c */
+#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 *huntele(Element *, unsigned int, int);
Element *huntstart(Element *);
+Element *mk_skip(void);
Element *target(Element *);
Lextok *do_unless(Lextok *, Lextok *);
Lextok *rem_lab(Symbol *, Lextok *, Symbol *);
Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
Lextok *tail_add(Lextok *, Lextok *);
+Lextok *return_statement(Lextok *);
-ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *);
+ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);
SeqList *seqlist(Sequence *, SeqList *);
Sequence *close_seq(int);
Symbol *lookup(char *);
Symbol *prep_inline(Symbol *, Lextok *);
-char *emalloc(int);
+char *put_inline(FILE *, char *);
+char *emalloc(size_t);
long Rand(void);
int any_oper(Lextok *, int);
int c_add_sv(FILE *);
int cast_val(int, int, int);
int checkvar(Symbol *, int);
+int check_track(Lextok *);
int Cnt_flds(Lextok *);
int cnt_mpars(Lextok *);
int complete_rendez(void);
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 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 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 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 ini_struct(Symbol *);
void loose_ends(void);
void make_atomic(Sequence *, int);
+void mark_last(void);
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 ntimes(FILE *, int, int, const char *c[]);
void open_seq(int);
void p_talk(Element *, int);
-void pickup_inline(Symbol *, Lextok *);
+void pickup_inline(Symbol *, Lextok *, Lextok *);
void plunk_c_decls(FILE *);
void plunk_c_fcts(FILE *);
void plunk_expr(FILE *, char *);
-void plunk_inline(FILE *, char *, int);
+void plunk_inline(FILE *, char *, int, int);
void prehint(Symbol *);
void preruse(FILE *, Lextok *);
+void pretty_print(void);
void prune_opts(Lextok *);
void pstext(int, char *);
void pushbreak(void);
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 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 *, ...);
+
+extern int unlink(const char *);
+
+#define TMP_FILE1 "._s_p_i_n_"
+#define TMP_FILE2 "._n_i_p_s_"
+
#endif
projects / plan9front.git / blobdiff