From 062ec6c872cf59fd30a2991368ec5bc02bcb893d Mon Sep 17 00:00:00 2001 From: Martino Luca Date: Tue, 19 Jul 2016 08:39:35 -0700 Subject: [PATCH] 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 | 7 ++- .../c/frontend/vaarg_expr/vaarg_expr.c | 24 ++++++++ .../c/frontend/vaarg_expr/vaarg_expr.c.dot | 51 ++++++++++++++++ infer/tests/endtoend/c/VAArgExprTest.java | 59 +++++++++++++++++++ infer/tests/frontend/c/VAArgExprTest.java | 31 ++++++++++ 5 files changed, 169 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c create mode 100644 infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot create mode 100644 infer/tests/endtoend/c/VAArgExprTest.java create mode 100644 infer/tests/frontend/c/VAArgExprTest.java diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 81495fd72..4278b9ba2 100644 --- a/infer/src/clang/cTrans.ml +++ b/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_trans trans_state expr_info + | OffsetOfExpr (_, _, expr_info) + | VAArgExpr (_, _, expr_info) -> + trans_into_undefined_expr trans_state expr_info | s -> (Printing.log_stats "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \ diff --git a/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c b/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c new file mode 100644 index 000000000..20c1614ed --- /dev/null +++ b/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 + +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; +} diff --git a/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot b/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot new file mode 100644 index 000000000..43858886b --- /dev/null +++ b/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 ; +} diff --git a/infer/tests/endtoend/c/VAArgExprTest.java b/infer/tests/endtoend/c/VAArgExprTest.java new file mode 100644 index 000000000..6be0af71b --- /dev/null +++ b/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 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})); + } + +} diff --git a/infer/tests/frontend/c/VAArgExprTest.java b/infer/tests/frontend/c/VAArgExprTest.java new file mode 100644 index 000000000..3527b0923 --- /dev/null +++ b/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); + } +}