Merge pull request #1347 from goblint/evalfunvar-dead

Fix no function to call warnings on dead code

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 *)

tests/regression/00-sanity/38-evalfunvar-dead.c

@@ -0,0 +1,8 @@
+#include <stdlib.h>
+
+int main() {
+  int (*fp)() = &rand;
+  abort();
+  fp(); // NOWARN (No suitable function to call)
+  return 0;
+}