diff --git a/.gitignore b/.gitignore index 9fa04976..3d0c44a3 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,8 @@ Src/spin Src/y.tab.h Src/y.output +compile_commands.json +level1.tasks +PVS-Studio-Report.md +PVS-Studio.log +PVS-Studio.tasks diff --git a/README.md b/README.md index d6f02c02..3dd6f7f1 100644 --- a/README.md +++ b/README.md @@ -1,26 +1,122 @@ # Spin -## An Efficient Logic Model Checker for the Verification of Multi-threaded Code - -Spin is an open-source software verification tool that was originally -developed (starting in 1980) in the Computing Science Research Center of Bell Labs -(the Unix group). It is often considered the most widely used formal verification tool. - -Compilation and installation is trivial (see the makefile) and the only dependencies -are the use of a C compiler, yacc or byacc, and a small number of standard -unix/linux/cygwin-like tools (like make, mv, and rm). With help of a related tool -[Modex](http://spinroot.com/modex) Spin can verify C code directly, but the most -common use of the tool is to write a formal specification of the essence of an -application to be verified in a C-like meta-language called ProMeLa (Process Meta -Language). Annual Symposia and Workshops on the tool have been held since 1995. - -The main site for access to manuals, tutorials, and papers explaining the theory -behind the tool is [http://spinroot.com](http://spinroot.com). - -This repository contains the most recent version of the sources. Updates that are more -recent than the version.h files were made after the most recent release. When a new -release is issued, the version.h file is also updated. - -The tool supports a range of different verification algorithms, including depth-first, -breadth-first, parallel/multi-core, bounded depth, bitstate search (using Bloom filter -theory), partial order reduced, and swarm search (using arbitrarily many cpus). + +> **An Efficient Logic Model Checker for the Formal Verification of Multi-threaded Software** + +Spin is an open-source software verification tool originally developed starting in 1980 by Gerard J. Holzmann in the Computing Science Research Center of Bell Labs (the Unix group). It is widely considered one of the most powerful and popular formal verification tools available. + +--- + +## πŸ“Œ Overview + +Spin is designed for formal verification of multi-threaded, concurrent, and distributed software systems. + +Applications are typically specified in a high-level modeling language called **PROMELA** (*Process Meta Language*). Spin can simulate system executions or generate optimized C source code (`pan.c`) that exhaustively verifies the system for properties such as: +- **Deadlocks** (invalid end states) +- **Data Races & Invariant Violations** (assert failures) +- **Unreachable Code** +- **LTL Properties** (Linear Temporal Logic formulas for safety and liveness) + +Spin can also be used directly with C source code via the companion tool [Modex](http://spinroot.com/modex). + +--- + +## ✨ Features & Verification Algorithms + +Spin supports a broad range of formal verification algorithms and state-space reduction techniques: + +- **Depth-First Search (DFS) & Breadth-First Search (BFS)** +- **Partial Order Reduction (POR)** for state space compression +- **Bitstate Search** (using Bloom filter techniques for extremely large state spaces) +- **Multi-Core / Parallel Verification** +- **Bounded-Depth Search** +- **Swarm Search** (randomized parallel search across CPU cores) +- **LTL to BΓΌchi Automata** conversion for temporal logic checks + +--- + +## πŸ› οΈ Build and Installation + +### Prerequisites + +To compile Spin, you need standard C build tools: +- A **C Compiler** (`gcc` or `clang`) +- **`yacc`** or **`byacc`** (or `bison -y`) +- Standard Unix utilities (`make`, `mv`, `rm`) + +### Compilation + +Clone the repository and build using `make`: + +```bash +git clone https://github.com/nimble-code/Spin.git +cd Spin +make +``` + +To install the `spin` executable into standard PATH (`/usr/local/bin` by default): + +```bash +sudo make install +``` + +--- + +## πŸš€ Quick Start + +### 1. Simulation Mode + +You can run a random simulation of a PROMELA model (e.g. from the [`Examples/`](file:///Volumes/External/Code/Spin/Examples) directory): + +```bash +spin Examples/hello.pml +``` + +### 2. Verification Mode + +To perform an exhaustive verification of a specification: + +```bash +# 1. Generate the verifier source code (pan.c) +spin -a model.pml + +# 2. Compile the verifier +gcc -O2 -o pan pan.c + +# 3. Run the verifier to search for errors +./pan +``` + +If an error (e.g. deadlock or assertion failure) is found, a trace file (`model.pml.trail`) is generated. You can replay the error path with: + +```bash +spin -t -p model.pml +``` + +--- + +## πŸ–₯️ Graphical Interface (iSpin) + +Spin includes an optional Tcl/Tk-based GUI named **iSpin**, located in [`optional_gui/ispin.tcl`](file:///Volumes/External/Code/Spin/optional_gui/ispin.tcl). + +To run iSpin (requires Tcl/Tk installed): + +```bash +wish optional_gui/ispin.tcl +``` + +--- + +## πŸ“– Documentation & Links + +- **Official Website**: [http://spinroot.com](http://spinroot.com) +- **Manuals & Tutorials**: [http://spinroot.com/spin/Man/](http://spinroot.com/spin/Man/) +- **Examples**: See the [`Examples/`](file:///Volumes/External/Code/Spin/Examples) directory. +- **Documentation Papers & Books**: See the [`Doc/`](file:///Volumes/External/Code/Spin/Doc) directory. + +--- + +## πŸ“„ License + +Spin is released under a BSD 3-Clause License. See [`LICENSE`](file:///Volumes/External/Code/Spin/LICENSE) for full details. + diff --git a/Src/flow.c b/Src/flow.c index 7176ebc3..7ebed3e7 100644 --- a/Src/flow.c +++ b/Src/flow.c @@ -68,7 +68,7 @@ Rjumpslocal(Element *q, Element *stop) /* allow no jumps out of a d_step sequence */ for (f = q; f && f != stop; f = f->nxt) - { if (f && f->n && f->n->ntyp == GOTO) + { if (f->n && f->n->ntyp == GOTO) { lb = get_lab(f->n, 0); if (!lb || lb->Seqno < DstepStart) { lineno = f->n->ln; diff --git a/Src/guided.c b/Src/guided.c index b1f597bc..fb29da1a 100644 --- a/Src/guided.c +++ b/Src/guided.c @@ -159,7 +159,7 @@ match_trail(void) } if ((fd = fopen(snap, "r")) == NULL) - { snap[strlen(snap)-2] = '\0'; /* .tra */ + { if (strlen(snap) >= 2) snap[strlen(snap)-2] = '\0'; /* .tra */ if ((fd = fopen(snap, "r")) == NULL) { if ((q = strchr(oFname->name, '.')) != NULL) { *q = '\0'; @@ -174,7 +174,7 @@ match_trail(void) if ((fd = fopen(snap, "r")) != NULL) goto okay; - snap[strlen(snap)-2] = '\0'; /* last try */ + if (strlen(snap) >= 2) snap[strlen(snap)-2] = '\0'; /* last try */ if ((fd = fopen(snap, "r")) != NULL) goto okay; } @@ -414,6 +414,7 @@ lost_trail(void) printf("(state %d) - d %d\n", n, l); } wrapup(1); /* no return */ + alldone(1); } int diff --git a/Src/main.c b/Src/main.c index e307ad0a..a2a2411a 100644 --- a/Src/main.c +++ b/Src/main.c @@ -259,6 +259,10 @@ e_system(int v, const char *s) return system(s); } +#if defined(__GNUC__) || defined(__clang__) +void alldone(int) __attribute__((noreturn)); +#endif + void alldone(int estatus) { char *ptr; @@ -511,7 +515,7 @@ alldone(int estatus) /* increase -w every itsr_n-th run */ if ((itsr_n > 0 && (itsr == 0 || (itsr%itsr_n) != 0)) - || (change_param(tmp, "-w", 36, 18) >= 0)) /* max 4G bit statespace */ + || (change_param(tmp, "-w", 36, 18) > 0)) /* max 4G bit statespace */ { (void) change_param(tmp, "-h", 500, 0); /* hash function 0.499 */ (void) change_param(tmp, "-p_rotate", 256, 0); /* if defined */ (void) change_param(tmp, "-k", 4, 1); /* nr bits per state 0->1,2,3 */ @@ -596,13 +600,13 @@ preprocess(char *a, char *b, int a_tmp) assert(strlen(PreProc) < sizeof(precmd)); strcpy(precmd, PreProc); for (i = 1; i <= PreCnt; i++) - { strcat(precmd, " "); + { if (strlen(precmd) + 1 + strlen(PreArg[i]) >= sizeof(precmd)) + { fprintf(stdout, "spin: too many -D args, aborting\n"); + alldone(1); + } + strcat(precmd, " "); strcat(precmd, PreArg[i]); } - if (strlen(precmd) > sizeof(precmd)) - { fprintf(stdout, "spin: too many -D args, aborting\n"); - alldone(1); - } sprintf(cmd, "%s \"%s\" > \"%s\"", precmd, a, b); if (e_system(2, (const char *)cmd)) /* preprocessing step */ { (void) unlink((const char *) b); diff --git a/Src/mesg.c b/Src/mesg.c index 662f812f..9dd3c2fa 100644 --- a/Src/mesg.c +++ b/Src/mesg.c @@ -163,9 +163,9 @@ qsend(Lextok *n) tcgetattr(0,&initial_settings); new_settings = initial_settings; - new_settings.c_lflag &= ~ICANON; - new_settings.c_lflag &= ~ECHO; - new_settings.c_lflag &= ~ISIG; + new_settings.c_lflag &= ~(tcflag_t)ICANON; + new_settings.c_lflag &= ~(tcflag_t)ECHO; + new_settings.c_lflag &= ~(tcflag_t)ISIG; new_settings.c_cc[VMIN] = 0; new_settings.c_cc[VTIME] = 0; } @@ -438,7 +438,7 @@ a_rcv(Queue *q, Lextok *n, int full) } if (!full) continue; /* test */ - if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL) + if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL) { (void) setval(m->lft, q->contents[i*q->nflds+j]); typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv"); } @@ -791,42 +791,39 @@ nochan_manip(Lextok *p, Lextok *n, int d) /* p=lhs n=rhs */ return; } - if (d == 0 && p->sym && p->sym->type == CHAN) + if (d == 0 && p->sym->type == CHAN) { setaccess(p->sym, ZS, 0, 'L'); - if (n && n->ntyp == CONST) + if (n->ntyp == CONST) fatal("invalid asgn to chan", (char *) 0); - if (n && n->sym && n->sym->type == CHAN) + if (n->sym && n->sym->type == CHAN) { setaccess(n->sym, ZS, 0, 'V'); return; } } - if (!d && n && n->ismtyp) /* rhs is an mtype value (a constant) */ + if (!d && n->ismtyp) /* rhs is an mtype value (a constant) */ { char *lhs = "_unnamed_", *rhs = "_unnamed_"; - if (p->sym) - { lhs = p->sym->mtype_name?p->sym->mtype_name->name:"_unnamed_"; - } + lhs = p->sym->mtype_name?p->sym->mtype_name->name:"_unnamed_"; if (n->sym) { rhs = which_mtype(n->sym->name); /* only for constants */ } - if (p->sym && !p->sym->mtype_name && n->sym) + if (!p->sym->mtype_name && n->sym) { p->sym->mtype_name = (Symbol *) emalloc(sizeof(Symbol)); p->sym->mtype_name->name = rhs; } else if (strcmp(lhs, rhs) != 0) { fprintf(stderr, "spin: %s:%d, Error: '%s' is type '%s' but '%s' is type '%s'\n", p->fn->name, p->ln, - p->sym?p->sym->name:"?", lhs, + p->sym->name, lhs, n->sym?n->sym->name:"?", rhs); non_fatal("type error", (char *) 0); } } /* ok on the rhs of an assignment: */ - if (!n - || n->ntyp == LEN || n->ntyp == RUN + if (n->ntyp == LEN || n->ntyp == RUN || n->ntyp == FULL || n->ntyp == NFULL || n->ntyp == EMPTY || n->ntyp == NEMPTY || n->ntyp == 'R') diff --git a/Src/msc_tcl.c b/Src/msc_tcl.c index 17004fb9..2845958c 100644 --- a/Src/msc_tcl.c +++ b/Src/msc_tcl.c @@ -306,7 +306,7 @@ putprelude(void) else sprintf(snap, "%s.trail", oFname?oFname->name:"msc"); if (!(fd = fopen(snap, "r"))) - { snap[strlen(snap)-2] = '\0'; + { if (strlen(snap) >= 2) snap[strlen(snap)-2] = '\0'; if (!(fd = fopen(snap, "r"))) fatal("cannot open trail file", (char *) 0); } diff --git a/Src/pangen1.c b/Src/pangen1.c index 4516cef2..706e2991 100644 --- a/Src/pangen1.c +++ b/Src/pangen1.c @@ -815,7 +815,7 @@ c_wrapper(FILE *fd) /* allow pan.c to print out global sv entries */ for (lst = Mtypes; lst; lst = lst->nxt) { fprintf(fd, " if (strcmp(s, \"%s\") == 0)\n", lst->nm); fprintf(fd, " switch (x) {\n"); - for (n = lst->mt, j = 1; n && j; n = n->rgt, j++) + for (n = lst->mt, j = 1; n; n = n->rgt, j++) fprintf(fd, "\tcase %d: Printf(\"%s\"); return;\n", j, n->lft->sym->name); fprintf(fd, " default: Printf(\"%%d\", x); return;\n"); diff --git a/Src/pangen2.c b/Src/pangen2.c index c8b7e8f9..bad02295 100644 --- a/Src/pangen2.c +++ b/Src/pangen2.c @@ -1123,10 +1123,10 @@ valTpe(Lextok *n) 7*DELTA = @, process deletion (conditionally safe) */ switch (n->ntyp) { /* a series of fall-thru cases: */ - case FULL: res += DELTA; /* add 3*DELTA + chan nr */ - case EMPTY: res += DELTA; /* add 2*DELTA + chan nr */ + case FULL: res += DELTA; /* add 3*DELTA + chan nr */ /* FALLTHROUGH */ + case EMPTY: res += DELTA; /* add 2*DELTA + chan nr */ /* FALLTHROUGH */ case 'r': - case NEMPTY: res += DELTA; /* add 1*DELTA + chan nr */ + case NEMPTY: res += DELTA; /* add 1*DELTA + chan nr */ /* FALLTHROUGH */ case 's': case NFULL: res += getNid(n->lft); /* add channel nr */ break; @@ -1295,7 +1295,7 @@ static CaseCache *casing[6]; static int identical(Lextok *p, Lextok *q) { - if ((!p && q) || (p && !q)) + if ((!p) != (!q)) return 0; if (!p) return 1; @@ -2299,7 +2299,6 @@ has_global(Lextok *n) { if (old_priority_rules) { if (n_seen != n->sym) fatal("cannot refer to _priority with -o6", (char *) 0); - n_seen = n->sym; } return 0; } @@ -3204,7 +3203,8 @@ putstmnt(FILE *fd, Lextok *now, int m) case PRINTM: { char *s = 0; - if (now->lft->sym + if (now->lft + && now->lft->sym && now->lft->sym->mtype_name) { s = now->lft->sym->mtype_name->name; } diff --git a/Src/pangen3.c b/Src/pangen3.c index 9e2a33e1..c7a732d4 100644 --- a/Src/pangen3.c +++ b/Src/pangen3.c @@ -454,10 +454,7 @@ comwork(FILE *fd, Lextok *now, int m) if (c == '\"') buf[j] = '\''; if (c == '\0') break; } - if (now->ntyp == PRINT) - fprintf(fd, "printf"); - else - fprintf(fd, "annotate"); + fprintf(fd, "printf"); fprintf(fd, "(%s", buf); } for (v = now->lft; v; v = v->rgt) @@ -467,7 +464,8 @@ comwork(FILE *fd, Lextok *now, int m) break; case PRINTM: fprintf(fd, "printm("); { char *s = 0; - if (now->lft->sym + if (now->lft + && now->lft->sym && now->lft->sym->mtype_name) { s = now->lft->sym->mtype_name->name; } diff --git a/Src/pangen5.c b/Src/pangen5.c index 4fd49a10..325d075f 100644 --- a/Src/pangen5.c +++ b/Src/pangen5.c @@ -121,14 +121,15 @@ static int howdeep = 0; static int eligible(FSM_trans *v) -{ Element *el = ZE; - Lextok *lt = ZN; +{ Element *el; + Lextok *lt; - if (v) el = v->step; - if (el) lt = v->step->n; + if (!v || !v->step || !v->step->n) + return 0; + el = v->step; + lt = el->n; - if (!lt /* dead end */ - || v->nxt /* has alternatives */ + if (v->nxt /* has alternatives */ || el->esc /* has an escape */ || (el->status&CHECK2) /* remotely referenced */ || lt->ntyp == ATOMIC diff --git a/Src/pangen6.c b/Src/pangen6.c index df8e08d8..3f2a7b0f 100644 --- a/Src/pangen6.c +++ b/Src/pangen6.c @@ -264,7 +264,7 @@ def_use(Lextok *now, int code) def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) - { if (v->lft->ntyp == ',') + { if (v->lft->lft && v->lft->lft->ntyp == ',') { def_use(v->lft->lft, code); /* will add USE */ } else { def_use(v->lft, code); /* will add USE */ @@ -278,7 +278,7 @@ def_use(Lextok *now, int code) def_use(now->lft, DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) - { if (v->lft->ntyp == ',') + { if (v->lft->lft && v->lft->lft->ntyp == ',') { def_use(v->lft->lft, code); /* will add USE */ } else { def_use(v->lft, code); /* will add USE */ @@ -2001,9 +2001,9 @@ subgraph(AST *a, FSM_state *f, int out) if (verbose&32) printf("possible pair %d %d -- %d\n", - f->from, h->from, (g[i]&(1<from, h->from, (g[i]&(1UL<from); /* record this pair */ } @@ -2036,7 +2036,7 @@ act_dom(AST *a) } i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ - if (!(f->dom[i]&(1<dom[i]&(1UL<t, i = 0; t; t = t->nxt) @@ -2186,20 +2186,20 @@ init_dom(AST *a) if (f->from == a->i_st) { i = a->i_st / BPW; j = a->i_st % BPW; /* assert(j <= 32); */ - f->dom[i] = (1<dom[i] = (1UL<nwords; i++) { f->dom[i] = (ulong) ~0; /* all 1's */ } if (a->nstates % BPW) for (i = (a->nstates % BPW); i < (int) BPW; i++) - { f->dom[a->nwords-1] &= ~(1<< ((ulong) i)); /* clear tail */ + { f->dom[a->nwords-1] &= ~(1UL<< ((ulong) i)); /* clear tail */ } for (cnt = 0; cnt < a->nstates; cnt++) { if (!fsm_tbl[cnt]->seen) { i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ - f->dom[i] &= ~(1<< ((ulong) j)); + f->dom[i] &= ~(1UL<< ((ulong) j)); } } } } } @@ -2229,7 +2229,7 @@ dom_perculate(AST *a, FSM_state *f) i = f->from / BPW; j = f->from % BPW; /* assert(j <= 32); */ - ndom[i] |= (1<nwords; i++) if (f->dom[i] != ndom[i]) diff --git a/Src/pangen7.c b/Src/pangen7.c index b6b492ed..38a4413f 100644 --- a/Src/pangen7.c +++ b/Src/pangen7.c @@ -834,9 +834,7 @@ set_el(int n, Element *e) e->nxt = e; g = e; mk_accepting(n, e); - } else - - if (e->n->ntyp == GOTO) + } else if (e->n->ntyp == GOTO) { g = get_lab(e->n, 1); g = huntele(g, e->status, -1); } else if (e->nxt) diff --git a/Src/run.c b/Src/run.c index ad7c8a4e..f3f56726 100644 --- a/Src/run.c +++ b/Src/run.c @@ -173,7 +173,7 @@ eval_sub(Element *e) { if (e->n && e->n->indstep >= 0) k = 0; /* select 1st executable guard */ else - k = Rand()%j; /* nondeterminism */ + k = (j > 0) ? (Rand()%j) : 0; /* nondeterminism */ } has_else = ZE; @@ -646,7 +646,9 @@ Enabled0(Element *e) if (Rvous) return 0; return 1; case UNLESS: - return Enabled0(e->sub->this->frst); + if (e->sub && e->sub->this) + return Enabled0(e->sub->this->frst); + return 0; case ATOMIC: case D_STEP: case NON_ATOMIC: diff --git a/Src/spinlex.c b/Src/spinlex.c index dc4b3bc1..88851880 100644 --- a/Src/spinlex.c +++ b/Src/spinlex.c @@ -1190,7 +1190,8 @@ prep_inline(Symbol *s, Lextok *nms) for (t = nms; t; t = t->rgt) if (t->lft) { if (t->lft->ntyp != NAME) - fatal("bad param to inline %s", s?s->name:"--"); + { fatal("bad param to inline %s", s?s->name:"--"); + } t->lft->sym->hidden |= 32; } @@ -1972,21 +1973,21 @@ yylex(void) { IArgno = 0; IArg_cont[0][0] = '\0'; } else - { assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont)); + { assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont[IArgno])); strcat(IArg_cont[IArgno], yytext); } } else if (strcmp(yytext, ")") == 0) { if (--IArg_nst > 0) - { assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont)); + { assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont[IArgno])); strcat(IArg_cont[IArgno], yytext); } } else if (c == CONST && yytext[0] == '\'') { sprintf(yytext, "'%c'", yylval->val); - assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont)); + assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont[IArgno])); strcat(IArg_cont[IArgno], yytext); } else if (c == CONST) { sprintf(yytext, "%d", yylval->val); - assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont)); + assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont[IArgno])); strcat(IArg_cont[IArgno], yytext); } else { @@ -2012,7 +2013,7 @@ yylex(void) case AND: strcpy(yytext, "&&"); break; case OR: strcpy(yytext, "||"); break; } - assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont)); + assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont[IArgno])); strcat(IArg_cont[IArgno], yytext); } } diff --git a/Src/structs.c b/Src/structs.c index 6505a8e2..919bf453 100644 --- a/Src/structs.c +++ b/Src/structs.c @@ -456,7 +456,7 @@ walk_struct(FILE *ofd, int dowhat, char *s, Symbol *z, char *a, char *b, char *c void c_struct(FILE *fd, char *ipref, Symbol *z) { Lextok *fp, *tl; - char pref[512], eprefix[300]; + char pref[512], eprefix[512]; int ix; ini_struct(z); @@ -467,7 +467,7 @@ c_struct(FILE *fd, char *ipref, Symbol *z) { strcpy(eprefix, ipref); if (z->nel > 1 || z->isarray == 1) { /* insert index before last '.' */ - eprefix[strlen(eprefix)-1] = '\0'; + if (strlen(eprefix) > 0) eprefix[strlen(eprefix)-1] = '\0'; sprintf(pref, "[ %d ].", ix); strcat(eprefix, pref); } @@ -497,7 +497,7 @@ dump_struct(Symbol *z, char *prefix, RunList *r) for (fp = z->Sval[ix]; fp; fp = fp->rgt) for (tl = fp->lft; tl; tl = tl->rgt) { if (tl->sym->type == STRUCT) - { char pref[300]; + { char pref[512]; strcpy(pref, eprefix); strcat(pref, "."); strcat(pref, tl->sym->name); diff --git a/Src/sym.c b/Src/sym.c index 94c3d613..d5738d5f 100644 --- a/Src/sym.c +++ b/Src/sym.c @@ -237,7 +237,6 @@ setptype(Lextok *mtype_name, Lextok *n, int t, Lextok *vis) /* predefined types { if (n->sym->type && !(n->sym->hidden&32)) { lineno = n->ln; Fname = n->fn; fatal("redeclaration of '%s'", n->sym->name); - lineno = oln; } n->sym->type = (short) t; @@ -245,7 +244,6 @@ setptype(Lextok *mtype_name, Lextok *n, int t, Lextok *vis) /* predefined types { lineno = n->ln; Fname = n->fn; fatal("missing semi-colon after '%s'?", mtype_name->sym->name); - lineno = oln; } if (mtype_name && n->sym->mtype_name diff --git a/Src/tl_mem.c b/Src/tl_mem.c index 9cd36c38..98d96231 100644 --- a/Src/tl_mem.c +++ b/Src/tl_mem.c @@ -55,7 +55,7 @@ tl_emalloc(int U) All_Mem += (unsigned long) u*sizeof(union M); } else { if (!freelist[u]) - { r = req[u] += req[u] ? req[u] : 1; + { r = (req[u] += (req[u] ? req[u] : 1)); if (r >= NOTOOBIG) { r = req[u] = NOTOOBIG; }