From a4261deb3f784720d0806cf92c1c9165d2cbe36e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 16 Oct 2023 17:36:23 +0300 Subject: [PATCH] Add final message for unknown ignored longjmp --- src/framework/constraints.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 21f3958a81..95a13ed516 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1663,7 +1663,8 @@ struct if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets; let handle_target target = match target with | JmpBufDomain.BufferEntryOrTop.AllTargets -> - M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env + M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env; + M.msg_final Error ~category:Unsound ~tags:[Category Imprecise; Category Call] "Longjmp to unknown target ignored" | Target (target_node, target_context) -> let target_fundec = Node.find_fundec target_node in if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (