Fix exp.single-threaded spawning errors

1. Don't output final message if no thread creations are even attempted by the program.
2. Output non-final message for each suppressed thread.

Author: sim642

src/analyses/mCP.ml

@@ -149,12 +149,14 @@ struct
 
   let do_spawns man (xs:(varinfo * (lval option * exp list * bool)) list) =
     let spawn_one v d =
-      List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
+      if get_bool "exp.single-threaded" then (
+        M.msg_final Error ~category:Unsound "Thread not spawned";
+        M.error ~category:Unsound "Thread not spawned from %a" CilType.Varinfo.pretty v
+      )
+      else
+        List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
     in
-    if get_bool "exp.single-threaded" then
-      M.msg_final Error ~category:Unsound "Thread not spawned" (* TODO: non-final error *) (* TODO: only final error if xs is non-empty *)
-    else
-      iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
+    iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
   let do_sideg man (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) =
     let side_one v dts =

tests/regression/00-sanity/42-no-threadflag.t

@@ -33,7 +33,6 @@ Assertions should succeed, race should not be present.
     live: 5
     dead: 0
     total lines: 5
-  [Error][Unsound] Thread not spawned
 
 
 With single-threaded mode forced, but earlyglobs enabled.
@@ -46,5 +45,4 @@ Assertions should be unknown, race should not be present.
     live: 5
     dead: 0
     total lines: 5
-  [Error][Unsound] Thread not spawned
 

tests/regression/00-sanity/43-no-escape.t

@@ -26,5 +26,4 @@ Assertions should succeed.
     live: 7
     dead: 0
     total lines: 7
-  [Error][Unsound] Thread not spawned
 

tests/regression/02-base/32-single-thr.t

@@ -2,6 +2,7 @@
   [Error][Imprecise][Unsound] Function definition missing for no_spawn (32-single-thr.c:12:3-12:15)
   [Info][Imprecise] INVALIDATING ALL GLOBALS! (32-single-thr.c:12:3-12:15)
   [Info][Imprecise] Invalidating expressions: & g, (void *)(& f) (32-single-thr.c:12:3-12:15)
+  [Error][Unsound] Thread not spawned from f (32-single-thr.c:12:3-12:15)
   [Warning][Deadcode] Function 'f' is uncalled: 2 LLoC (32-single-thr.c:6:1-8:1)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 4