From: Gabor Horvath <xazax.hun@gmail.com>
Date: Fri, 12 May 2017 07:02:54 +0000 (+0000)
Subject: [analyzer] Add modelling of __builtin_assume
X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=6aa8fdcd35f4cd4a0b3b0cf0ee48b87c08a11f7e;p=clang

[analyzer] Add modelling of __builtin_assume

Differential Revision: https://reviews.llvm.org/D33092


git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@302880 91177308-0d34-0410-b5e6-96231b3b80d8
---

diff --git a/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp b/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
index 8c2aef21b3..48d6cd8a52 100644
--- a/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
+++ b/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
@@ -41,6 +41,22 @@ bool BuiltinFunctionChecker::evalCall(const CallExpr *CE,
   default:
     return false;
 
+  case Builtin::BI__builtin_assume: {
+    assert (CE->arg_begin() != CE->arg_end());
+    SVal ArgSVal = state->getSVal(CE->getArg(0), LCtx);
+    if (ArgSVal.isUndef())
+      return true; // Return true to model purity.
+
+    state = state->assume(ArgSVal.castAs<DefinedOrUnknownSVal>(), true);
+    // FIXME: do we want to warn here? Not right now. The most reports might
+    // come from infeasible paths, thus being false positives.
+    if (!state)
+      return true;
+
+    C.addTransition(state);
+    return true;
+  }
+
   case Builtin::BI__builtin_unpredictable:
   case Builtin::BI__builtin_expect:
   case Builtin::BI__builtin_assume_aligned:
diff --git a/test/Analysis/builtin-assume.c b/test/Analysis/builtin-assume.c
new file mode 100644
index 0000000000..00d651d9e3
--- /dev/null
+++ b/test/Analysis/builtin-assume.c
@@ -0,0 +1,8 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+void f(int i) {
+  __builtin_assume(i < 10);
+  clang_analyzer_eval(i < 15); // expected-warning {{TRUE}}
+}