diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4d48d2439f..f0ec31b28e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1242,6 +1242,7 @@ struct if AD.mem Addr.UnknownPtr jmp_buf then M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e; begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with + (* dummy *) | JmpBuf (x, copied, invalid) -> 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;