Fix longjmp crash on Uninitialized

goblint · Oct 9, 2023 · 2224e86 · 2224e86
1 parent fd5237a
commit 2224e86
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git 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
@@ -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