diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 7b87d3ff51..2fda2540e8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1217,9 +1217,16 @@ struct if copied then M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e; x - | y -> failwith (GobPretty.sprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local) + | Top + | Bot -> + JmpBufDomain.JmpBufSet.top () + | y -> + M.debug ~category:Imprecise "EvalJmpBuf %a is %a, not JmpBuf." CilType.Exp.pretty e VD.pretty y; + JmpBufDomain.JmpBufSet.top () end - | _ -> failwith "problem?!" + | _ -> + M.debug ~category:Imprecise "EvalJmpBuf is not Address"; + JmpBufDomain.JmpBufSet.top () end | Q.EvalInt e -> query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e 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 ( diff --git a/tests/regression/68-longjmp/56-longjmp-top.c b/tests/regression/68-longjmp/56-longjmp-top.c new file mode 100644 index 0000000000..adb3a47476 --- /dev/null +++ b/tests/regression/68-longjmp/56-longjmp-top.c @@ -0,0 +1,21 @@ +// Extracted from concrat/pigz. +#include +#include +#include + +pthread_key_t buf_key; + +int main() { + jmp_buf buf; + pthread_setspecific(buf_key, &buf); + + if (!setjmp(buf)) { + jmp_buf *buf_ptr; + buf_ptr = pthread_getspecific(buf_key); + longjmp(*buf_ptr, 1); // NO CRASH: problem?! + } + else { + __goblint_check(1); // TODO reachable: https://github.com/goblint/analyzer/pull/1210#discussion_r1350021903 + } + return 0; +}