Bug hunting; better handling of early return

This commit is contained in:
Daniel Marjamäki 2020-12-13 09:13:11 +01:00
parent b85aa626ff
commit be16b2c276
2 changed files with 23 additions and 1 deletions

View File

@ -2382,8 +2382,16 @@ static std::string execute(const Token *start, const Token *end, Data &data)
Recursion updateRecursion(&data.recursion, data.recursion); Recursion updateRecursion(&data.recursion, data.recursion);
for (const Token *tok = start; tok != end; tok = tok->next()) { for (const Token *tok = start; tok != end; tok = tok->next()) {
if (Token::Match(tok, "[;{}]")) if (Token::Match(tok, "[;{}]")) {
data.trackProgramState(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__ ;")) if (Token::simpleMatch(tok, "__CPPCHECK_BAILOUT__ ;"))
// This is intended for testing // This is intended for testing

View File

@ -63,6 +63,7 @@ private:
TEST_CASE(if5); TEST_CASE(if5);
TEST_CASE(ifelse1); TEST_CASE(ifelse1);
TEST_CASE(ifif); TEST_CASE(ifif);
TEST_CASE(ifreturn);
TEST_CASE(istream); 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() { void istream() {
const char code[] = "void foo(const std::string& in) {\n" const char code[] = "void foo(const std::string& in) {\n"
" std::istringstream istr(in);\n" " std::istringstream istr(in);\n"