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); +}