fix(pvs): resolve Low Level (Level 3) static analyzer warnings and formatting notes

.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

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.
+
 

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;

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

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);

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')

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);
 		}

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");

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;
@@ -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)
@@ -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;
 		  }