[frontend] Fix a bug in translation of empty for-loop

Summary:
This diff fixes a bug in the translation of an empty for-loop.  When both initialization and
incrementation statements did not introduce a new node, the frontend generated an incorrect results
where the for-loop was unreachable from the entry node.

Fixes  https://github.com/facebook/infer/issues/1374

Reviewed By: jvillard

Differential Revision: D25912142

fbshipit-source-id: 15b65cb84

infer/src/clang/cTrans.ml

@@ -2224,7 +2224,11 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
     let root_nodes =
       match loop_kind with
       | Loops.For _ -> (
-        match init_incr_nodes with Some (nodes_init, _) -> nodes_init | None -> assert false )
+        match init_incr_nodes with
+        | Some (nodes_init, _) ->
+            if List.is_empty nodes_init then [join_node] else nodes_init
+        | None ->
+            assert false )
       | Loops.While _ | Loops.DoWhile _ ->
           [join_node]
     in

infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c

@@ -134,3 +134,11 @@ void threshold_by_comparison_2_Bad() {
     arr[j] = 0;
   }
 }
+
+void infinite_for_loop_Good() {
+  int arr[5];
+  int x = 0;
+  for (x;;) {
+  }
+  arr[10] = 0;
+}

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

@@ -102,6 +102,7 @@ codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_
 codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `count`,<Length trace>,Parameter `arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: 5]
+codetoanalyze/c/bufferoverrun/for_loop.c, infinite_for_loop_Good, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_1_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]