From 44b44928668346c722ca23fb448c6da73f471276 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 12 Oct 2023 15:37:25 +0200 Subject: [PATCH] Issue non-termination warning for `longjmp` calls --- src/framework/constraints.ml | 9 +++++++++ tests/regression/78-termination/49-longjmp.c | 11 +++++++++++ 2 files changed, 20 insertions(+) create mode 100644 tests/regression/78-termination/49-longjmp.c diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 924794b9ce..cf439f2c45 100644 --- 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 new file mode 100644 index 0000000000..be13cb286c --- /dev/null +++ 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 +jmp_buf buf; +int main() +{ + if(setjmp(buf)) { + + } + + longjmp(buf, 1); +}