move everything out of trunk
[lttv.git] / trunk / verif / Spin / Src5.1.6 / sym.c
diff --git a/trunk/verif/Spin/Src5.1.6/sym.c b/trunk/verif/Spin/Src5.1.6/sym.c
deleted file mode 100755 (executable)
index 823dbf0..0000000
+++ /dev/null
@@ -1,533 +0,0 @@
-/***** spin: sym.c *****/
-
-/* 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            */
-
-#include "spin.h"
-#include "y.tab.h"
-
-extern Symbol  *Fname, *owner;
-extern int     lineno, depth, verbose, NamesNotAdded, deadvar, has_hidden;
-extern short   has_xu;
-
-Symbol *context = ZS;
-Ordered        *all_names = (Ordered *)0;
-int    Nid = 0;
-
-Lextok *Mtype = (Lextok *) 0;
-
-static Ordered *last_name = (Ordered *)0;
-static Symbol  *symtab[Nhash+1];
-static Lextok *runstmnts = ZN;
-
-static int
-samename(Symbol *a, Symbol *b)
-{
-       if (!a && !b) return 1;
-       if (!a || !b) return 0;
-       return !strcmp(a->name, b->name);
-}
-
-int
-hash(char *s)
-{      int h=0;
-
-       while (*s)
-       {       h += *s++;
-               h <<= 1;
-               if (h&(Nhash+1))
-                       h |= 1;
-       }
-       return h&Nhash;
-}
-
-Symbol *
-lookup(char *s)
-{      Symbol *sp; Ordered *no;
-       int h = hash(s);
-
-       for (sp = symtab[h]; sp; sp = sp->next)
-               if (strcmp(sp->name, s) == 0
-               &&  samename(sp->context, context)
-               &&  samename(sp->owner, owner))
-                       return sp;              /* found */
-
-       if (context)                            /* in proctype */
-       for (sp = symtab[h]; sp; sp = sp->next)
-               if (strcmp(sp->name, s) == 0
-               && !sp->context
-               &&  samename(sp->owner, owner))
-                       return sp;              /* global */
-
-       sp = (Symbol *) emalloc(sizeof(Symbol));
-       sp->name = (char *) emalloc(strlen(s) + 1);
-       strcpy(sp->name, s);
-       sp->nel = 1;
-       sp->setat = depth;
-       sp->context = context;
-       sp->owner = owner;                      /* if fld in struct */
-
-       if (NamesNotAdded == 0)
-       {       sp->next = symtab[h];
-               symtab[h] = sp;
-               no = (Ordered *) emalloc(sizeof(Ordered));
-               no->entry = sp;
-               if (!last_name)
-                       last_name = all_names = no;
-               else
-               {       last_name->next = no;
-                       last_name = no;
-       }       }
-
-       return sp;
-}
-
-void
-trackvar(Lextok *n, Lextok *m)
-{      Symbol *sp = n->sym;
-
-       if (!sp) return;        /* a structure list */
-       switch (m->ntyp) {
-       case NAME:
-               if (m->sym->type != BIT)
-               {       sp->hidden |= 4;
-                       if (m->sym->type != BYTE)
-                               sp->hidden |= 8;
-               }
-               break;
-       case CONST:
-               if (m->val != 0 && m->val != 1)
-                       sp->hidden |= 4;
-               if (m->val < 0 || m->val > 256)
-                       sp->hidden |= 8; /* ditto byte-equiv */
-               break;
-       default:        /* unknown */
-               sp->hidden |= (4|8); /* not known bit-equiv */
-       }
-}
-
-void
-trackrun(Lextok *n)
-{
-       runstmnts = nn(ZN, 0, n, runstmnts);
-}
-
-void
-checkrun(Symbol *parnm, int posno)
-{      Lextok *n, *now, *v; int i, m;
-       int res = 0; char buf[16], buf2[16];
-
-       for (n = runstmnts; n; n = n->rgt)
-       {       now = n->lft;
-               if (now->sym != parnm->context)
-                       continue;
-               for (v = now->lft, i = 0; v; v = v->rgt, i++)
-                       if (i == posno)
-                       {       m = v->lft->ntyp;
-                               if (m == CONST)
-                               {       m = v->lft->val;
-                                       if (m != 0 && m != 1)
-                                               res |= 4;
-                                       if (m < 0 || m > 256)
-                                               res |= 8;
-                               } else if (m == NAME)
-                               {       m = v->lft->sym->type;
-                                       if (m != BIT)
-                                       {       res |= 4;
-                                               if (m != BYTE)
-                                                       res |= 8;
-                                       }
-                               } else
-                                       res |= (4|8); /* unknown */
-                               break;
-       }               }
-       if (!(res&4) || !(res&8))
-       {       if (!(verbose&32)) return;
-               strcpy(buf2, (!(res&4))?"bit":"byte");
-               sputtype(buf, parnm->type);
-               i = (int) strlen(buf);
-               while (i > 0 && buf[--i] == ' ') buf[i] = '\0';
-               if (i == 0 || strcmp(buf, buf2) == 0) return;
-               prehint(parnm);
-               printf("proctype %s, '%s %s' could be declared",
-                       parnm->context?parnm->context->name:"", buf, parnm->name);
-               printf(" '%s %s'\n", buf2, parnm->name);
-       }
-}
-
-void
-trackchanuse(Lextok *m, Lextok *w, int t)
-{      Lextok *n = m; int cnt = 1;
-       while (n)
-       {       if (n->lft
-               &&  n->lft->sym
-               &&  n->lft->sym->type == CHAN)
-                       setaccess(n->lft->sym, w?w->sym:ZS, cnt, t);
-               n = n->rgt; cnt++;
-       }
-}
-
-void
-setptype(Lextok *n, int t, Lextok *vis)        /* predefined types */
-{      int oln = lineno, cnt = 1; extern int Expand_Ok;
-
-       while (n)
-       {       if (n->sym->type && !(n->sym->hidden&32))
-               { lineno = n->ln; Fname = n->fn;
-                 non_fatal("redeclaration of '%s'", n->sym->name);
-                 lineno = oln;
-               }
-               n->sym->type = (short) t;
-
-               if (Expand_Ok)
-               {       n->sym->hidden |= (4|8|16); /* formal par */
-                       if (t == CHAN)
-                       setaccess(n->sym, ZS, cnt, 'F');
-               }
-               if (t == UNSIGNED)
-               {       if (n->sym->nbits < 0 || n->sym->nbits >= 32)
-                       fatal("(%s) has invalid width-field", n->sym->name);
-                       if (n->sym->nbits == 0)
-                       {       n->sym->nbits = 16;
-                               non_fatal("unsigned without width-field", 0);
-                       }
-               } else if (n->sym->nbits > 0)
-               {       non_fatal("(%s) only an unsigned can have width-field",
-                               n->sym->name);
-               }
-               if (vis)
-               {       if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
-                       {       n->sym->hidden |= 1;
-                               has_hidden++;
-                               if (t == BIT)
-                               fatal("bit variable (%s) cannot be hidden",
-                                       n->sym->name);
-                       } else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
-                       {       n->sym->hidden |= 2;
-                       } else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
-                       {       n->sym->hidden |= 64;
-                       }
-               }
-               if (t == CHAN)
-                       n->sym->Nid = ++Nid;
-               else
-               {       n->sym->Nid = 0;
-                       if (n->sym->ini
-                       &&  n->sym->ini->ntyp == CHAN)
-                       {       Fname = n->fn;
-                               lineno = n->ln;
-                               fatal("chan initializer for non-channel %s",
-                               n->sym->name);
-                       }
-               }
-               if (n->sym->nel <= 0)
-               { lineno = n->ln; Fname = n->fn;
-                 non_fatal("bad array size for '%s'", n->sym->name);
-                 lineno = oln;
-               }
-               n = n->rgt; cnt++;
-       }
-}
-
-static void
-setonexu(Symbol *sp, int t)
-{
-       sp->xu |= t;
-       if (t == XR || t == XS)
-       {       if (sp->xup[t-1]
-               &&  strcmp(sp->xup[t-1]->name, context->name))
-               {       printf("error: x[rs] claims from %s and %s\n",
-                               sp->xup[t-1]->name, context->name);
-                       non_fatal("conflicting claims on chan '%s'",
-                               sp->name);
-               }
-               sp->xup[t-1] = context;
-       }
-}
-
-static void
-setallxu(Lextok *n, int t)
-{      Lextok *fp, *tl;
-
-       for (fp = n; fp; fp = fp->rgt)
-       for (tl = fp->lft; tl; tl = tl->rgt)
-       {       if (tl->sym->type == STRUCT)
-                       setallxu(tl->sym->Slst, t);
-               else if (tl->sym->type == CHAN)
-                       setonexu(tl->sym, t);
-       }
-}
-
-Lextok *Xu_List = (Lextok *) 0;
-
-void
-setxus(Lextok *p, int t)
-{      Lextok *m, *n;
-
-       has_xu = 1; 
-       if (!context)
-       {       lineno = p->ln;
-               Fname = p->fn;
-               fatal("non-local x[rs] assertion", (char *)0);
-       }
-       for (m = p; m; m = m->rgt)
-       {       Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
-               Xu_new->val = t;
-               Xu_new->lft = m->lft;
-               Xu_new->sym = context;
-               Xu_new->rgt = Xu_List;
-               Xu_List = Xu_new;
-
-               n = m->lft;
-               if (n->sym->type == STRUCT)
-                       setallxu(n->sym->Slst, t);
-               else if (n->sym->type == CHAN)
-                       setonexu(n->sym, t);
-               else
-               {       int oln = lineno;
-                       lineno = n->ln; Fname = n->fn;
-                       non_fatal("xr or xs of non-chan '%s'",
-                               n->sym->name);
-                       lineno = oln;
-               }
-       }
-}
-
-void
-setmtype(Lextok *m)
-{      Lextok *n;
-       int cnt, oln = lineno;
-
-       if (m) { lineno = m->ln; Fname = m->fn; }
-
-       if (!Mtype)
-               Mtype = m;
-       else
-       {       for (n = Mtype; n->rgt; n = n->rgt)
-                       ;
-               n->rgt = m;     /* concatenate */
-       }
-
-       for (n = Mtype, cnt = 1; n; n = n->rgt, cnt++)  /* syntax check */
-       {       if (!n->lft || !n->lft->sym
-               ||   n->lft->ntyp != NAME
-               ||   n->lft->lft)       /* indexed variable */
-                       fatal("bad mtype definition", (char *)0);
-
-               /* label the name */
-               if (n->lft->sym->type != MTYPE)
-               {       n->lft->sym->hidden |= 128;     /* is used */
-                       n->lft->sym->type = MTYPE;
-                       n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
-                       n->lft->sym->ini->val = cnt;
-               } else if (n->lft->sym->ini->val != cnt)
-                       non_fatal("name %s appears twice in mtype declaration",
-                               n->lft->sym->name);
-       }
-       lineno = oln;
-       if (cnt > 256)
-       fatal("too many mtype elements (>255)", (char *)0);
-}
-
-int
-ismtype(char *str)     /* name to number */
-{      Lextok *n;
-       int cnt = 1;
-
-       for (n = Mtype; n; n = n->rgt)
-       {       if (strcmp(str, n->lft->sym->name) == 0)
-                       return cnt;
-               cnt++;
-       }
-       return 0;
-}
-
-int
-sputtype(char *foo, int m)
-{
-       switch (m) {
-       case UNSIGNED:  strcpy(foo, "unsigned "); break;
-       case BIT:       strcpy(foo, "bit   "); break;
-       case BYTE:      strcpy(foo, "byte  "); break;
-       case CHAN:      strcpy(foo, "chan  "); break;
-       case SHORT:     strcpy(foo, "short "); break;
-       case INT:       strcpy(foo, "int   "); break;
-       case MTYPE:     strcpy(foo, "mtype "); break;
-       case STRUCT:    strcpy(foo, "struct"); break;
-       case PROCTYPE:  strcpy(foo, "proctype"); break;
-       case LABEL:     strcpy(foo, "label "); return 0;
-       default:        strcpy(foo, "value "); return 0;
-       }
-       return 1;
-}
-
-
-static int
-puttype(int m)
-{      char buf[128];
-
-       if (sputtype(buf, m))
-       {       printf("%s", buf);
-               return 1;
-       }
-       return 0;
-}
-
-void
-symvar(Symbol *sp)
-{      Lextok *m;
-
-       if (!puttype(sp->type))
-               return;
-
-       printf("\t");
-       if (sp->owner) printf("%s.", sp->owner->name);
-       printf("%s", sp->name);
-       if (sp->nel > 1) printf("[%d]", sp->nel);
-
-       if (sp->type == CHAN)
-               printf("\t%d", (sp->ini)?sp->ini->val:0);
-       else if (sp->type == STRUCT) /* Frank Weil, 2.9.8 */
-               printf("\t%s", sp->Snm->name);
-       else
-               printf("\t%d", eval(sp->ini));
-
-       if (sp->owner)
-               printf("\t<:struct-field:>");
-       else
-       if (!sp->context)
-               printf("\t<:global:>");
-       else
-               printf("\t<%s>", sp->context->name);
-
-       if (sp->Nid < 0)        /* formal parameter */
-               printf("\t<parameter %d>", -(sp->Nid));
-       else
-               printf("\t<variable>");
-       if (sp->type == CHAN && sp->ini)
-       {       int i;
-               for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
-                       i++;
-               printf("\t%d\t", i);
-               for (m = sp->ini->rgt; m; m = m->rgt)
-               {       if (m->ntyp == STRUCT)
-                               printf("struct %s", m->sym->name);
-                       else
-                               (void) puttype(m->ntyp);
-                       if (m->rgt) printf("\t");
-               }
-       }
-       printf("\n");
-}
-
-void
-symdump(void)
-{      Ordered *walk;
-
-       for (walk = all_names; walk; walk = walk->next)
-               symvar(walk->entry);
-}
-
-void
-chname(Symbol *sp)
-{      printf("chan ");
-       if (sp->context) printf("%s-", sp->context->name);
-       if (sp->owner) printf("%s.", sp->owner->name);
-       printf("%s", sp->name);
-       if (sp->nel > 1) printf("[%d]", sp->nel);
-       printf("\t");
-}
-
-static struct X {
-       int typ; char *nm;
-} xx[] = {
-       { 'A', "exported as run parameter" },
-       { 'F', "imported as proctype parameter" },
-       { 'L', "used as l-value in asgnmnt" },
-       { 'V', "used as r-value in asgnmnt" },
-       { 'P', "polled in receive stmnt" },
-       { 'R', "used as parameter in receive stmnt" },
-       { 'S', "used as parameter in send stmnt" },
-       { 'r', "received from" },
-       { 's', "sent to" },
-};
-
-static void
-chan_check(Symbol *sp)
-{      Access *a; int i, b=0, d;
-
-       if (verbose&1) goto report;     /* -C -g */
-
-       for (a = sp->access; a; a = a->lnk)
-               if (a->typ == 'r')
-                       b |= 1;
-               else if (a->typ == 's')
-                       b |= 2;
-       if (b == 3 || (sp->hidden&16))  /* balanced or formal par */
-               return;
-report:
-       chname(sp);
-       for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++)
-       {       b = 0;
-               for (a = sp->access; a; a = a->lnk)
-                       if (a->typ == xx[i].typ) b++;
-               if (b == 0) continue; d++;
-               printf("\n\t%s by: ", xx[i].nm);
-               for (a = sp->access; a; a = a->lnk)
-                 if (a->typ == xx[i].typ)
-                 {     printf("%s", a->who->name);
-                       if (a->what) printf(" to %s", a->what->name);
-                       if (a->cnt)  printf(" par %d", a->cnt);
-                       if (--b > 0) printf(", ");
-                 }
-       }
-       printf("%s\n", (!d)?"\n\tnever used under this name":"");
-}
-
-void
-chanaccess(void)
-{      Ordered *walk;
-       char buf[128];
-       extern int Caccess, separate;
-       extern short has_code;
-
-       for (walk = all_names; walk; walk = walk->next)
-       {       if (!walk->entry->owner)
-               switch (walk->entry->type) {
-               case CHAN:
-                       if (Caccess) chan_check(walk->entry);
-                       break;
-               case MTYPE:
-               case BIT:
-               case BYTE:
-               case SHORT:
-               case INT:
-               case UNSIGNED:
-                       if ((walk->entry->hidden&128))  /* was: 32 */
-                               continue;
-
-                       if (!separate
-                       &&  !walk->entry->context
-                       &&  !has_code
-                       &&   deadvar)
-                               walk->entry->hidden |= 1; /* auto-hide */
-
-                       if (!(verbose&32) || has_code) continue;
-
-                       printf("spin: warning, %s, ", Fname->name);
-                       sputtype(buf, walk->entry->type);
-                       if (walk->entry->context)
-                               printf("proctype %s",
-                                       walk->entry->context->name);
-                       else
-                               printf("global");
-                       printf(", '%s%s' variable is never used\n",
-                               buf, walk->entry->name);
-       }       }
-}
This page took 0.027174 seconds and 4 git commands to generate.