aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTed Kremenek <kremenek@apple.com>2009-04-10 00:59:50 +0000
committerTed Kremenek <kremenek@apple.com>2009-04-10 00:59:50 +0000
commit52e5602056e4cade24cbcca57767e94e1d430b03 (patch)
treecae7aa770a469c35b40754fc2e044ffa5010fed8
parent11c7d32ac2f8a784a3cc4714a9f1977ab5859185 (diff)
Fix: <rdar://problem/6776949> Branch condition evaluates to an uninitialized value (argc is guaranteed to be >= 1)
The analyzer now adds the precondition that the first argument of 'main' is > 0. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@68757 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--lib/Analysis/GRExprEngine.cpp26
-rw-r--r--test/Analysis/misc-ps.m22
2 files changed, 47 insertions, 1 deletions
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index 1d1100a55a..46d1f798cf 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -161,7 +161,31 @@ void GRExprEngine::AddCheck(GRSimpleAPICheck *A) {
}
const GRState* GRExprEngine::getInitialState() {
- return StateMgr.getInitialState();
+ const GRState *state = StateMgr.getInitialState();
+
+ // Precondition: the first argument of 'main' is an integer guaranteed
+ // to be > 0.
+ // FIXME: It would be nice if we had a more general mechanism to add
+ // such preconditions. Some day.
+ if (const FunctionDecl *FD = dyn_cast<FunctionDecl>(&StateMgr.getCodeDecl()))
+ if (strcmp(FD->getIdentifier()->getName(), "main") == 0 &&
+ FD->getNumParams() > 0) {
+ const ParmVarDecl *PD = FD->getParamDecl(0);
+ QualType T = PD->getType();
+ if (T->isIntegerType())
+ if (const MemRegion *R = StateMgr.getRegion(PD)) {
+ SVal V = GetSVal(state, loc::MemRegionVal(R));
+ SVal Constraint = EvalBinOp(BinaryOperator::GT, V,
+ ValMgr.makeZeroVal(T),
+ getContext().IntTy);
+ bool isFeasible = false;
+ const GRState *newState = Assume(state, Constraint, true,
+ isFeasible);
+ if (newState) state = newState;
+ }
+ }
+
+ return state;
}
//===----------------------------------------------------------------------===//
diff --git a/test/Analysis/misc-ps.m b/test/Analysis/misc-ps.m
index 777784aabc..0f85d22436 100644
--- a/test/Analysis/misc-ps.m
+++ b/test/Analysis/misc-ps.m
@@ -245,3 +245,25 @@ void rdar_6777003(int x) {
*p = 1; // expected-warning{{Dereference of null pointer}}
}
+// <rdar://problem/6776949>
+// main's 'argc' argument is always > 0
+int main(int argc, char* argv[]) {
+ int *p = 0;
+
+ if (argc == 0)
+ *p = 1;
+
+ if (argc == 1)
+ return 1;
+
+ int x = 1;
+ int i;
+
+ for(i=1;i<argc;i++){
+ p = &x;
+ }
+
+ return *p; // no-warning
+}
+
+