diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 300fe693d..3ad2a5445 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -2382,8 +2382,16 @@ static std::string execute(const Token *start, const Token *end, Data &data) Recursion updateRecursion(&data.recursion, data.recursion); for (const Token *tok = start; tok != end; tok = tok->next()) { - if (Token::Match(tok, "[;{}]")) + if (Token::Match(tok, "[;{}]")) { data.trackProgramState(tok); + if (tok->str() == ";") { + const Token *prev = tok->previous(); + while (prev && !Token::Match(prev, "[;{}]")) + prev = prev->previous(); + if (Token::Match(prev, "[;{}] return|throw")) + return data.str(); + } + } if (Token::simpleMatch(tok, "__CPPCHECK_BAILOUT__ ;")) // This is intended for testing diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 5b680bf91..152cb6437 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -63,6 +63,7 @@ private: TEST_CASE(if5); TEST_CASE(ifelse1); TEST_CASE(ifif); + TEST_CASE(ifreturn); TEST_CASE(istream); @@ -460,6 +461,19 @@ private: } + void ifreturn() { // Early return + const char code[] = "void foo(unsigned char x) {\n" + " if (x > 5) { return; }\n" + " return x == 13;\n" + "}"; + + ASSERT_EQUALS("(<= $1 5)\n" + "(and (>= $1 0) (<= $1 255))\n" + "(= $1 13)\n" + "z3::unsat\n", + expr(code, "==")); + } + void istream() { const char code[] = "void foo(const std::string& in) {\n" " std::istringstream istr(in);\n"