/***** spin: vars.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 */
+/*
+ * 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
+ */
#include "spin.h"
#include "y.tab.h"
extern Symbol *Fname;
extern char Buf[];
extern int lineno, depth, verbose, xspin, limited_vis;
-extern int analyze, jumpsteps, nproc, nstop, columns;
+extern int analyze, jumpsteps, nproc, nstop, columns, old_priority_rules;
extern short no_arrays, Have_claim;
extern void sr_mesg(FILE *, int, int);
extern void sr_buf(int, int);
{ if (!X) return 0;
return X->pid - Have_claim;
}
+ if (strcmp(s->name, "_priority") == 0)
+ { if (!X) return 0;
+
+ if (old_priority_rules)
+ { non_fatal("cannot refer to _priority with -o6", (char *) 0);
+ return 1;
+ }
+ return X->priority;
+ }
+
if (strcmp(s->name, "_nr_pr") == 0)
- return nproc-nstop; /* new 3.3.10 */
+ { return nproc-nstop; /* new 3.3.10 */
+ }
if (s->context && s->type)
- return getlocal(sn);
+ { return getlocal(sn);
+ }
if (!s->type) /* not declared locally */
{ s = lookup(s->name); /* try global */
sn->sym = s; /* fix it */
}
+
return getglobal(sn);
}
int
setval(Lextok *v, int n)
{
+ if (strcmp(v->sym->name, "_last") == 0
+ || strcmp(v->sym->name, "_p") == 0
+ || strcmp(v->sym->name, "_pid") == 0
+ || strcmp(v->sym->name, "_nr_qs") == 0
+ || strcmp(v->sym->name, "_nr_pr") == 0)
+ { non_fatal("illegal assignment to %s", v->sym->name);
+ }
+ if (strcmp(v->sym->name, "_priority") == 0)
+ { if (old_priority_rules)
+ { non_fatal("cannot refer to _priority with -o6", (char *) 0);
+ return 1;
+ }
+ if (!X)
+ { non_fatal("no context for _priority", (char *) 0);
+ return 1;
+ }
+ X->priority = n;
+ }
+
if (v->sym->context && v->sym->type)
return setlocal(v, n);
if (!v->sym->type)
checkvar(Symbol *s, int n)
{ int i, oln = lineno; /* calls on eval() change it */
Symbol *ofnm = Fname;
+ Lextok *z, *y;
if (!in_bound(s, n))
return 0;
/* not a STRUCT */
if (s->val == (int *) 0) /* uninitialized */
{ s->val = (int *) emalloc(s->nel*sizeof(int));
+ z = s->ini;
for (i = 0; i < s->nel; i++)
- { if (s->type != CHAN)
- { rm_selfrefs(s, s->ini);
- s->val[i] = eval(s->ini);
+ { if (z && z->ntyp == ',')
+ { y = z->lft;
+ z = z->rgt;
+ } else
+ { y = z;
+ }
+ if (s->type != CHAN)
+ { rm_selfrefs(s, y);
+ s->val[i] = eval(y);
} else if (!analyze)
- s->val[i] = qmake(s);
- } }
+ { s->val[i] = qmake(s);
+ } } }
lineno = oln;
Fname = ofnm;
+
return 1;
}
{ Symbol *s = sn->sym;
int i, n = eval(sn->lft);
- if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))
+ if (s->type == 0 && X && (i = find_lab(s, X->n, 0))) /* getglobal */
{ printf("findlab through getglobal on %s\n", s->name);
return i; /* can this happen? */
}
if (s->type == STRUCT)
- return Rval_struct(sn, s, 1); /* 1 = check init */
+ { return Rval_struct(sn, s, 1); /* 1 = check init */
+ }
if (checkvar(s, n))
- return cast_val(s->type, s->val[n], s->nbits);
+ { return cast_val(s->type, s->val[n], s->nbits);
+ }
return 0;
}
}
if (v != i+s+ (int) u)
- { char buf[32]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t);
+ { char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+(int)u, t);
non_fatal("value (%s) truncated in assignment", buf);
}
- return (int)(i+s+u);
+ return (int)(i+s+(int)u);
}
static int
setglobal(Lextok *v, int m)
{
if (v->sym->type == STRUCT)
- (void) Lval_struct(v, v->sym, 1, m);
- else
+ { (void) Lval_struct(v, v->sym, 1, m);
+ } else
{ int n = eval(v->lft);
if (checkvar(v->sym, n))
- { v->sym->val[n] = cast_val(v->sym->type, m, v->sym->nbits);
- v->sym->setat = depth;
- } }
+ { int oval = v->sym->val[n];
+ int nval = cast_val(v->sym->type, m, v->sym->nbits);
+ v->sym->val[n] = nval;
+ if (oval != nval)
+ { v->sym->setat = depth;
+ } } }
return 1;
}
continue;
if (sp->type == STRUCT)
- { dump_struct(sp, sp->name, 0);
+ { if ((verbose&4) && !(verbose&64)
+ && (sp->setat < depth
+ && jumpsteps != depth))
+ { continue;
+ }
+ dump_struct(sp, sp->name, 0);
continue;
}
for (j = 0; j < sp->nel; j++)
if ((verbose&4) && !(verbose&64)
&& (sp->setat < depth
&& jumpsteps != depth))
- continue;
+ { continue;
+ }
+
dummy->sym = sp;
dummy->lft->val = j;
/* in case of cast_val warnings, do this first: */
prefetch = getglobal(dummy);
printf("\t\t%s", sp->name);
- if (sp->nel > 1) printf("[%d]", j);
+ if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
printf(" = ");
sr_mesg(stdout, prefetch,
sp->type == MTYPE);
}
sr_buf(prefetch, sp->type == MTYPE);
if (sp->colnr == 0)
- { sp->colnr = maxcolnr;
+ { sp->colnr = (unsigned char) maxcolnr;
maxcolnr = 1+(maxcolnr%10);
}
colpos = nproc+sp->colnr-1;
depth, colpos);
printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
printf("\t\t%s", sp->name);
- if (sp->nel > 1) printf("[%d]", j);
+ if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
printf(" = %s\n", Buf);
} } }
}
dummy->lft->val = i;
printf("\t\t%s(%d):%s",
- r->n->name, r->pid, z->name);
- if (z->nel > 1) printf("[%d]", i);
+ r->n->name, r->pid - Have_claim, z->name);
+ if (z->nel > 1 || z->isarray) printf("[%d]", i);
printf(" = ");
sr_mesg(stdout, getval(dummy), z->type == MTYPE);
printf("\n");
}
sr_buf(getval(dummy), z->type==MTYPE);
if (z->colnr == 0)
- { z->colnr = maxcolnr;
+ { z->colnr = (unsigned char) maxcolnr;
maxcolnr = 1+(maxcolnr%10);
}
colpos = nproc+z->colnr-1;
printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
printf("\t\t%s(%d):%s",
r->n->name, r->pid, z->name);
- if (z->nel > 1) printf("[%d]", i);
+ if (z->nel > 1 || z->isarray) printf("[%d]", i);
printf(" = %s\n", Buf);
} } }
}