From de083bc50c888b469967596333958aa064f3d2b6 Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:07:47 +0300 Subject: [PATCH 1/4] docs: update README.md with comprehensive overview, setup, and usage guides --- README.md | 144 +++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 120 insertions(+), 24 deletions(-) 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. + From fd3f8d0e9437aecb6ab6779cd0fbad940d7f6581 Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:11:38 +0300 Subject: [PATCH 2/4] fix(pvs): resolve all High Level (Level 1) static analyzer warnings - Fix potential buffer overflow and bounds check in main.c (preprocess) - Fix termios c_lflag bitmask truncation on 64-bit platforms in mesg.c - Fix potential null pointer dereferences in pangen2.c, pangen3.c, and run.c - Fix undefined behavior in 64-bit bit shift operations (1UL<= 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..14a6af25 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; } diff --git a/Src/pangen2.c b/Src/pangen2.c index c8b7e8f9..fa487f34 100644 --- a/Src/pangen2.c +++ b/Src/pangen2.c @@ -3204,7 +3204,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/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: From 2deac9ca26723965a7487a39391e4555b03d93d1 Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:15:36 +0300 Subject: [PATCH 3/4] fix(pvs): resolve Medium Level (Level 2) static analyzer warnings - Add array bounds guards for string operations in guided.c, msc_tcl.c, and structs.c - Fix sizeof(IArg_cont[IArgno]) target buffer in spinlex.c - Fix block scope formatting in spinlex.c - Declare alldone(int) with noreturn attribute and fix comparison logic in main.c - Guard NULL pointers in eligible() in pangen5.c - Clean up redundant pointer checks in flow.c and mesg.c - Remove redundant loop condition in pangen1.c - Add fallthrough annotations, simplify boolean logic, and remove dead assignment in pangen2.c - Remove unreachable code after fatal() in sym.c - Parenthesize assignment and ternary operator expression in tl_mem.c --- Src/flow.c | 2 +- Src/guided.c | 5 +++-- Src/main.c | 6 +++++- Src/mesg.c | 21 +++++++++------------ Src/msc_tcl.c | 2 +- Src/pangen1.c | 2 +- Src/pangen2.c | 9 ++++----- Src/pangen5.c | 13 +++++++------ Src/spinlex.c | 13 +++++++------ Src/structs.c | 6 +++--- Src/sym.c | 2 -- Src/tl_mem.c | 2 +- 12 files changed, 42 insertions(+), 41 deletions(-) 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 0f421877..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 */ diff --git a/Src/mesg.c b/Src/mesg.c index 14a6af25..9dd3c2fa 100644 --- a/Src/mesg.c +++ b/Src/mesg.c @@ -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 fa487f34..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; } 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/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; } From ce0b4d0a926faf3d1a136c654e657b19093f7d2b Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:17:11 +0300 Subject: [PATCH 4/4] fix(pvs): resolve Low Level (Level 3) static analyzer warnings and formatting notes - Explicitly cast int/char arguments to match fprintf format specifiers in pangen2.c and pangen3.c - Add NULL pointer checks in claim_has_accept() in pangen7.c - Guard pointer dereferences in getlocal() and setlocal() in sched.c - Guard NULL pointers when building struct nodes in structs.c - Guard NULL pointers in dupnode() and isequal() in tl_cache.c - Cast memory size arguments to long for printf formatting in tl_cache.c and tl_main.c --- Src/pangen2.c | 2 +- Src/pangen3.c | 2 +- Src/pangen7.c | 2 ++ Src/sched.c | 4 ++-- Src/structs.c | 22 ++++++++++++++-------- Src/tl_cache.c | 7 ++++--- Src/tl_main.c | 2 +- 7 files changed, 25 insertions(+), 16 deletions(-) diff --git a/Src/pangen2.c b/Src/pangen2.c index bad02295..8bf2e946 100644 --- a/Src/pangen2.c +++ b/Src/pangen2.c @@ -2219,7 +2219,7 @@ scan_seq(Sequence *s) && !(f->status & L_ATOM) && !(g->status & (ATOM|L_ATOM))) #endif - { fprintf(fd_tt, "\t/* mark-down line %d status %d = %d */\n", f->n->ln, f->status, (f->status & D_ATOM)); + { fprintf(fd_tt, "\t/* mark-down line %d status %d = %d */\n", f->n->ln, f->status, (int)(f->status & D_ATOM)); return 1; /* assume worst case */ } } for (h = f->sub; h; h = h->nxt) diff --git a/Src/pangen3.c b/Src/pangen3.c index c7a732d4..8bc217dd 100644 --- a/Src/pangen3.c +++ b/Src/pangen3.c @@ -526,7 +526,7 @@ comwork(FILE *fd, Lextok *now, int m) case UNLESS: fprintf(fd, "unless"); break; case TIMEOUT: fprintf(fd, "timeout"); break; default: if (isprint(now->ntyp)) - fprintf(fd, "'%c'", now->ntyp); + fprintf(fd, "'%c'", (char) now->ntyp); else fprintf(fd, "%d", now->ntyp); break; diff --git a/Src/pangen7.c b/Src/pangen7.c index 38a4413f..c27f2340 100644 --- a/Src/pangen7.c +++ b/Src/pangen7.c @@ -312,6 +312,8 @@ static int claim_has_accept(ProcList *p) { Label *l; + if (!p || !p->n) return 0; + for (l = labtab; l; l = l->nxt) { if (strcmp(l->c->name, p->n->name) == 0 && strncmp(l->s->name, "accept", 6) == 0) diff --git a/Src/sched.c b/Src/sched.c index 69ba521f..49925516 100644 --- a/Src/sched.c +++ b/Src/sched.c @@ -1008,7 +1008,7 @@ getlocal(Lextok *sn) r = findloc(s); if (r && r->type == STRUCT) return Rval_struct(sn, r, 1); /* 1 = check init */ - if (in_bound(r, n)) + if (r && in_bound(r, n)) return cast_val(r->type, r->val[n], r->nbits); return 0; } @@ -1018,7 +1018,7 @@ setlocal(Lextok *p, int m) { Symbol *r = findloc(p->sym); int n = eval(p->lft); - if (in_bound(r, n)) + if (r && in_bound(r, n)) { if (r->type == STRUCT) (void) Lval_struct(p, r, 1, m); /* 1 = check init */ else diff --git a/Src/structs.c b/Src/structs.c index 919bf453..fc0d96f6 100644 --- a/Src/structs.c +++ b/Src/structs.c @@ -547,10 +547,12 @@ retrieve(Lextok **targ, int i, int want, Lextok *n, int Ntyp) { for (k = 0; k < tl->sym->nel; k++, j++) { if (j == want) { *targ = cpnn(tl, 1, 0, 0); - (*targ)->lft = nn(ZN, CONST, ZN, ZN); - (*targ)->lft->val = k; - if (Ntyp) - (*targ)->ntyp = (short) Ntyp; + if (*targ) + { (*targ)->lft = nn(ZN, CONST, ZN, ZN); + (*targ)->lft->val = k; + if (Ntyp) + (*targ)->ntyp = (short) Ntyp; + } return -1; } } } } @@ -613,8 +615,10 @@ mk_explicit(Lextok *n, int Ok, int Ntyp) bld = mk_explicit(n->rgt->lft, Ok, Ntyp); for (x = bld; x; x = x->rgt) { y = cpnn(n, 1, 0, 0); - y->rgt = nn(ZN, '.', x->lft, ZN); - x->lft = y; + if (y) + { y->rgt = nn(ZN, '.', x->lft, ZN); + x->lft = y; + } } return bld; @@ -636,8 +640,10 @@ mk_explicit(Lextok *n, int Ok, int Ntyp) fatal("bad structure %s", n->sym->name); } x = cpnn(n, 1, 0, 0); - x->rgt = nn(ZN, '.', bld->lft, ZN); - bld->lft = x; + if (x) + { x->rgt = nn(ZN, '.', bld->lft, ZN); + bld->lft = x; + } } return bld; } diff --git a/Src/tl_cache.c b/Src/tl_cache.c index 1cf02735..baab0a68 100644 --- a/Src/tl_cache.c +++ b/Src/tl_cache.c @@ -89,8 +89,8 @@ cached(Node *n) void cache_stats(void) { - printf("cache stores : %9ld\n", Caches); - printf("cache hits : %9ld\n", CacheHits); + printf("cache stores : %9ld\n", (long) Caches); + printf("cache hits : %9ld\n", (long) CacheHits); } void @@ -139,6 +139,7 @@ dupnode(Node *n) if (!n) return n; d = getnode(n); + if (!d) return NULL; d->lft = dupnode(n->lft); d->rgt = dupnode(n->rgt); return d; @@ -242,7 +243,7 @@ isequal(Node *a, Node *b) if (!a || !b) { if (!a) - { if (b->ntyp == TRUE) + { if (b && b->ntyp == TRUE) return 1; } else { if (a->ntyp == TRUE) diff --git a/Src/tl_main.c b/Src/tl_main.c index 511b0b9a..69f33674 100644 --- a/Src/tl_main.c +++ b/Src/tl_main.c @@ -90,7 +90,7 @@ tl_UnGetchar(void) static void tl_stats(void) { extern int Stack_mx; - printf("total memory used: %9ld\n", All_Mem); + printf("total memory used: %9ld\n", (long) All_Mem); printf("largest stack sze: %9d\n", Stack_mx); cache_stats(); a_stats();