Translate VAArgExpr

Summary: Translate `VAArgExpr` (http://clang.llvm.org/doxygen/classclang_1_1VAArgExpr.html) into an expression that has an undefined value.

Reviewed By: dulmarod

Differential Revision: D3548756

fbshipit-source-id: c02a47d

infer/src/clang/cTrans.ml

@@ -2312,7 +2312,7 @@ struct
          | _ -> assert false) (* More cases to come. With the assert false we can find them *)
     | _ -> assert false (* Expect that this doesn't happen *)
 
-  and offsetOfExpr_trans trans_state expr_info =
+  and trans_into_undefined_expr trans_state expr_info =
     let tenv = trans_state.context.CContext.tenv in
     let typ = CTypes_decl.get_type_from_expr_info expr_info tenv in
     { empty_res_trans with exps = [CTrans_utils.undefined_expression (), typ] }
@@ -2605,8 +2605,9 @@ struct
     | CXXNoexceptExpr (_, _, expr_info, cxx_noexcept_expr_info) ->
         booleanValue_trans trans_state expr_info cxx_noexcept_expr_info.Clang_ast_t.xnee_value
 
-    | OffsetOfExpr (_, _, expr_info) ->
+    | OffsetOfExpr (_, _, expr_info)
-        offsetOfExpr_trans trans_state expr_info
+    | VAArgExpr (_, _, expr_info) ->
+        trans_into_undefined_expr trans_state expr_info
 
     | s -> (Printing.log_stats
               "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \

infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c

@@ -0,0 +1,24 @@
+/*
+ * 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.
+ */
+
+#include <stdarg.h>
+
+int foo(int x, ...) {
+  va_list valist;
+  va_start(valist, x);
+  int i = va_arg(valist, int);
+  int val;
+  if (i == 9) {
+    val = 9 / 0;
+  } else {
+    val = 4 / 0;
+  }
+  va_end(valist);
+  return val;
+}

infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot

@@ -0,0 +1,51 @@
+/* @generated */
+digraph iCFG {
+12 [label="12:  Call _fun___builtin_va_start \n   _fun___builtin_va_start(&valist:void *,&x:int &) [line 14]\n " shape="box"]
+	
+
+	 12 -> 11 ;
+11 [label="11:  DeclStmt \n   *&i:int =n$2 [line 15]\n " shape="box"]
+	
+
+	 11 -> 6 ;
+10 [label="10:  BinaryOperatorStmt: Assign \n   *&val:int =(4 / 0) [line 20]\n " shape="box"]
+	
+
+	 10 -> 5 ;
+9 [label="9:  BinaryOperatorStmt: Assign \n   *&val:int =(9 / 0) [line 18]\n " shape="box"]
+	
+
+	 9 -> 5 ;
+8 [label="8: Prune (false branch) \n   PRUNE(((n$1 == 9) == 0), false); [line 17]\n " shape="invhouse"]
+	
+
+	 8 -> 10 ;
+7 [label="7: Prune (true branch) \n   PRUNE(((n$1 == 9) != 0), true); [line 17]\n " shape="invhouse"]
+	
+
+	 7 -> 9 ;
+6 [label="6:  BinaryOperatorStmt: EQ \n   n$1=*&i:int  [line 17]\n " shape="box"]
+	
+
+	 6 -> 7 ;
+	 6 -> 8 ;
+5 [label="5: + \n  " ]
+	
+
+	 5 -> 4 ;
+4 [label="4:  Call _fun___builtin_va_end \n   _fun___builtin_va_end(&valist:void *) [line 22]\n " shape="box"]
+	
+
+	 4 -> 3 ;
+3 [label="3:  Return Stmt \n   n$0=*&val:int  [line 23]\n  *&return:int =n$0 [line 23]\n " shape="box"]
+	
+
+	 3 -> 2 ;
+2 [label="2: Exit foo \n  " color=yellow style=filled]
+	
+
+1 [label="1: Start foo\nFormals:  x:int \nLocals:  val:int  i:int  valist:void [1] \n   DECLARE_LOCALS(&return,&val,&i,&valist); [line 12]\n " color=yellow style=filled]
+	
+
+	 1 -> 12 ;
+}

infer/tests/endtoend/c/VAArgExprTest.java

@@ -0,0 +1,59 @@
+/*
+ * 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.
+ */
+
+package endtoend.c;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsLineNumbers.containsLines;
+
+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 VAArgExprTest {
+
+  public static final String FILE =
+      "infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder =
+      new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createCInferCommand(
+      folder,
+      FILE);
+
+  }
+
+  @Test
+  public void matchErrors()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferObjC(inferCmd);
+    assertThat(
+        "Results should contain the correct " + DIVIDE_BY_ZERO,
+        inferResults,
+        containsLines(new int[] {18, 20}));
+  }
+
+}

infer/tests/frontend/c/VAArgExprTest.java

@@ -0,0 +1,31 @@
+/*
+ * 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.
+ */
+
+package frontend.c;
+
+import org.junit.Rule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.ClangFrontendUtils;
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+
+public class VAArgExprTest {
+  String FILE = "infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c";
+
+  @Rule
+  public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @Test
+  public void frontendTest() throws InterruptedException, IOException, InferException {
+    ClangFrontendUtils.createAndCompareCDotFiles(folder, FILE);
+  }
+}