From 2224e86ce5e770cedd4558cfff6379471424e743 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 9 Oct 2023 11:46:24 +0300 Subject: [PATCH] Fix longjmp crash on Uninitialized --- src/analyses/base.ml | 11 +++++++++-- tests/regression/68-longjmp/56-longjmp-top.c | 2 +- 2 files changed, 10 insertions(+), 3 deletions(-) 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/tests/regression/68-longjmp/56-longjmp-top.c b/tests/regression/68-longjmp/56-longjmp-top.c index 4a12a43792..4d57b42fd3 100644 --- a/tests/regression/68-longjmp/56-longjmp-top.c +++ b/tests/regression/68-longjmp/56-longjmp-top.c @@ -12,7 +12,7 @@ int main() { if (!setjmp(buf)) { jmp_buf *buf_ptr; buf_ptr = pthread_getspecific(buf_key); - longjmp(*buf_ptr, 1); // TODO NO CRASH: problem?! + longjmp(*buf_ptr, 1); // NO CRASH: problem?! } else { __goblint_check(1); // reachable