Translate AttributedStmt and Fallthrough attribute

Reviewed By: akotulski

Differential Revision: D3469616

fbshipit-source-id: fe18937

infer/src/clang/cTrans.ml

@@ -2293,6 +2293,14 @@ struct
         conditionalOperator_trans trans_state stmt_info stmt_list' expr_info
     | _  -> binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list
 
+  and attributedStmt_trans trans_state stmts attrs =
+    let open Clang_ast_t in
+    match stmts, attrs with
+    | [stmt], [attr] ->
+        (match stmt, attr with
+         | NullStmt _, FallThroughAttr _ -> nullStmt_trans trans_state.succ_nodes
+         | _ -> assert false) (* More cases to come. With the assert false we can find them *)
+    | _ -> assert false (* Expect that this doesn't happen *)
 
   (* Translates a clang instruction into SIL instructions. It takes a       *)
   (* a trans_state containing current info on the translation and it returns *)
@@ -2574,6 +2582,9 @@ struct
         let trans_state' = { trans_state with priority = Free } in
         lambdaExpr_trans trans_state' expr_info decl
 
+    | AttributedStmt (_, stmts, attrs) ->
+        attributedStmt_trans trans_state stmts attrs
+
     | s -> (Printing.log_stats
               "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \
                Translation need to be defined. Statement ignored.... \n"

infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp

@@ -0,0 +1,27 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+int h() { return 3; }
+
+int switch_with_fallthrough(int n) {
+  int res = 5;
+  switch (n) {
+    case 22:
+    case 33:
+      [[clang::fallthrough]];
+    case 66:
+      [[clang::fallthrough]];
+    case 77:
+      res = h();
+      break;
+  }
+  return res;
+}
+
+int test_fallthrough() { return 1 / (switch_with_fallthrough(66) - 3); }

infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp.dot

@@ -0,0 +1,84 @@
+/* @generated */
+digraph iCFG {
+20 [label="20:  Return Stmt \n   n$0=_fun_switch_with_fallthrough(66:int ) [line 27]\n  *&return:int =(1 / (n$0 - 3)) [line 27]\n " shape="box"]
+	
+
+	 20 -> 19 ;
+19 [label="19: Exit test_fallthrough \n  " color=yellow style=filled]
+	
+
+18 [label="18: Start test_fallthrough\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 27]\n " color=yellow style=filled]
+	
+
+	 18 -> 20 ;
+17 [label="17:  DeclStmt \n   *&res:int =5 [line 13]\n " shape="box"]
+	
+
+	 17 -> 7 ;
+16 [label="16: Prune (false branch) \n   PRUNE(((n$1 == 22) == 0), false); [line 15]\n " shape="invhouse"]
+	
+
+	 16 -> 13 ;
+	 16 -> 14 ;
+15 [label="15: Prune (true branch) \n   PRUNE(((n$1 == 22) != 0), true); [line 15]\n " shape="invhouse"]
+	
+
+	 15 -> 8 ;
+14 [label="14: Prune (false branch) \n   PRUNE(((n$1 == 33) == 0), false); [line 16]\n " shape="invhouse"]
+	
+
+	 14 -> 11 ;
+	 14 -> 12 ;
+13 [label="13: Prune (true branch) \n   PRUNE(((n$1 == 33) != 0), true); [line 16]\n " shape="invhouse"]
+	
+
+	 13 -> 8 ;
+12 [label="12: Prune (false branch) \n   PRUNE(((n$1 == 66) == 0), false); [line 18]\n " shape="invhouse"]
+	
+
+	 12 -> 9 ;
+	 12 -> 10 ;
+11 [label="11: Prune (true branch) \n   PRUNE(((n$1 == 66) != 0), true); [line 18]\n " shape="invhouse"]
+	
+
+	 11 -> 8 ;
+10 [label="10: Prune (false branch) \n   PRUNE(((n$1 == 77) == 0), false); [line 20]\n " shape="invhouse"]
+	
+
+	 10 -> 6 ;
+9 [label="9: Prune (true branch) \n   PRUNE(((n$1 == 77) != 0), true); [line 20]\n " shape="invhouse"]
+	
+
+	 9 -> 8 ;
+8 [label="8:  BinaryOperatorStmt: Assign \n   n$2=_fun_h() [line 21]\n  *&res:int =n$2 [line 21]\n " shape="box"]
+	
+
+	 8 -> 6 ;
+7 [label="7:  Switch_stmt \n   n$1=*&n:int  [line 14]\n " shape="box"]
+	
+
+	 7 -> 15 ;
+	 7 -> 16 ;
+6 [label="6:  Return Stmt \n   n$0=*&res:int  [line 24]\n  *&return:int =n$0 [line 24]\n " shape="box"]
+	
+
+	 6 -> 5 ;
+5 [label="5: Exit switch_with_fallthrough \n  " color=yellow style=filled]
+	
+
+4 [label="4: Start switch_with_fallthrough\nFormals:  n:int \nLocals:  res:int  \n   DECLARE_LOCALS(&return,&res); [line 12]\n " color=yellow style=filled]
+	
+
+	 4 -> 17 ;
+3 [label="3:  Return Stmt \n   *&return:int =3 [line 10]\n " shape="box"]
+	
+
+	 3 -> 2 ;
+2 [label="2: Exit h \n  " color=yellow style=filled]
+	
+
+1 [label="1: Start h\nFormals: \nLocals:  \n   DECLARE_LOCALS(&return); [line 10]\n " color=yellow style=filled]
+	
+
+	 1 -> 3 ;
+}

infer/tests/endtoend/cpp/FallthroughTest.java

@@ -0,0 +1,62 @@
+/*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package endtoend.cpp;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class FallthroughTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/cpp/frontend/attributes/clang_fallthrough.cpp";
+
+  public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
+  private static ImmutableList<String> inferCmd;
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder =
+      new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createCPPInferCommand(folder, SOURCE_FILE);
+  }
+
+  @Test
+  public void whenInferRunsOnDivideByZeroThenDivideByZeroIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferC(inferCmd);
+    String[] procedures = {"test_fallthrough"};
+    assertThat(
+        "Results should contain divide by zero error",
+        inferResults,
+        containsExactly(
+            DIVIDE_BY_ZERO,
+            SOURCE_FILE,
+            procedures
+        )
+    );
+  }
+
+
+}

infer/tests/frontend/cpp/AttributesTest.java

@@ -0,0 +1,38 @@
+/*
+ * Copyright (c) 2015 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package frontend.cpp;
+
+import org.junit.Rule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.ClangFrontendUtils;
+
+public class AttributesTest {
+
+  String basePath = "infer/tests/codetoanalyze/cpp/frontend/attributes/";
+
+  @Rule
+  public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException {
+    ClangFrontendUtils.createAndCompareCppDotFiles(folder, basePath + fileRelative);
+  }
+
+  @Test
+  public void testClangFallthroughDotFilesMatch()
+      throws InterruptedException, IOException, InferException {
+    frontendTest("clang_fallthrough.cpp");
+  }
+
+}