[pre-analysis] Shortcut no-return nodes to exit-node

Summary:
The attribute `[no_return]` signifies that a function doesn't return. Previously, pre-analysis had cut the links to successor nodes of such no-return function nodes. This was intended to help with suppressing reporting on unreachable paths for some analyses. However, this results in having these nodes as dangling, with no connection to exit nodes.

This diff additionally shortcuts these no-return function nodes to exit node. This would allow us to  enhance inter-procedural analyses like pulse to kepp track of paths that do not return since we will be keeping their connections at exit node rather than completely cutting them of as before. It would also allow us to assume that all paths start at the one start node and end at the one exit node (at least syntactically in the CFG).

Reviewed By: skcho

Differential Revision: D20736043

fbshipit-source-id: 0eace1bdb

infer/src/backend/preanal.ml

@@ -330,7 +330,9 @@ module NoReturn = struct
   let process proc_desc =
     Procdesc.iter_nodes
       (fun node ->
-        if has_noreturn_call node then Procdesc.set_succs node ~normal:(Some []) ~exn:None )
+        if has_noreturn_call node then
+          let exit_node = Procdesc.get_exit_node proc_desc in
+          Procdesc.set_succs node ~normal:(Some [exit_node]) ~exn:None )
       proc_desc
 end
 

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -92,6 +92,7 @@ codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, null_pointer
 codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, null_pointer_with_function_pointer, 4, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, potentially_null_pointer_passed_as_argument, 3, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, simple_null_pointer, 2, NULL_DEREFERENCE, B1
+codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, unreachable_null_no_return_ok_FP, 5, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/short.c, f_error, 2, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE, B1

infer/tests/codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c

@@ -145,3 +145,14 @@ void unreachable_null_ok() {
   }
   *p = 42;
 }
+
+void no_ret() { will_not_return(); }
+
+// pre-analysis is not inter-procedural for handling no_return calls
+void unreachable_null_no_return_ok_FP() {
+  int* p = NULL;
+  if (p == NULL) {
+    no_ret(); // inter-procedural call to no_return
+  }
+  *p = 42;
+}