Issue non-termination warning for longjmp calls

goblint · Oct 12, 2023 · 44b4492 · 44b4492
1 parent 8be0343
commit 44b4492
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -1684,6 +1684,15 @@ struct
       )
       in
       List.iter handle_path (S.paths_as_set conv_ctx);
+      if !AnalysisState.should_warn && List.mem "termination" @@ get_string_list "ana.activated" then (
+        AnalysisState.svcomp_may_not_terminate := true;
+        let msgs =
+          [(Pretty.dprintf
+              "The program might not terminate! (Longjmp)",
+            None
+           );] in
+        M.msg_group Warning ~category:NonTerminating "Possibly non terminating loops" msgs
+      );
       S.D.bot ()
     | _ -> S.special conv_ctx lv f args
   let threadenter ctx = S.threadenter (conv ctx)

diff --git a/tests/regression/78-termination/49-longjmp.c b/tests/regression/78-termination/49-longjmp.c
@@ -0,0 +1,11 @@
+// SKIP NONTERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+#include <setjmp.h>
+jmp_buf buf;
+int main()
+{
+    if(setjmp(buf)) {
+
+    }
+
+    longjmp(buf, 1);
+}