From 7e57562220e049434db9af6a095c7da1312b4618 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 2 Oct 2023 17:05:18 +0300 Subject: [PATCH] Add final message for exp.single-threaded --- src/analyses/mCP.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 1b6a7e5a1d..9eb21b77ef 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -144,7 +144,9 @@ struct let spawn_one v d = List.iter (fun (lval, args) -> ctx.spawn lval v args) d in - if not (get_bool "exp.single-threaded") then + if get_bool "exp.single-threaded" then + M.msg_final Error ~category:Unsound "Thread not spawned" + else iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) =