diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 84d7eff1ed..31dc668937 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -758,7 +758,7 @@ struct None in let funs = List.filter_map one_function functions in - if [] = funs then begin + if [] = funs && not (S.D.is_bot ctx.local) then begin M.msg_final Warning ~category:Unsound ~tags:[Category Call] "No suitable function to call"; M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call."; d (* because LevelSliceLifter *) diff --git a/tests/regression/00-sanity/38-evalfunvar-dead.c b/tests/regression/00-sanity/38-evalfunvar-dead.c new file mode 100644 index 0000000000..26c779c7e6 --- /dev/null +++ b/tests/regression/00-sanity/38-evalfunvar-dead.c @@ -0,0 +1,8 @@ +#include + +int main() { + int (*fp)() = &rand; + abort(); + fp(); // NOWARN (No suitable function to call) + return 0; +}