walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: Add FP and String literals in determining that condition can (#2969)

This commit is contained in:
Georgy Komarov 2020-12-22 11:25:54 +03:00 committed by GitHub
parent fcb496fb40
commit 0731df7d2d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 82 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/exprengine.cpp
View File

@ -1404,13 +1404,13 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
{
const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty())
return true;
if (MathLib::isFloat(name)) {
float f = MathLib::toDoubleNumber(name);
return value >= f - 0.00001 && value <= f + 0.00001;
}
const Data *data = dynamic_cast<Data *>(dataBase);
if (data->constraints.empty())
return true;
#ifdef USE_Z3
// Check the value against the constraints
ExprData exprData;
@ -2555,6 +2555,12 @@ static std::string execute(const Token *start, const Token *end, Data &data)
} else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
canBeFalse = i->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
} else if (std::dynamic_pointer_cast<ExprEngine::StringLiteralValue>(condValue)) {
canBeFalse = false;
canBeTrue = true;
} else if (auto f = std::dynamic_pointer_cast<ExprEngine::FloatRange>(condValue)) {
canBeFalse = f->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", f, std::make_shared<ExprEngine::FloatRange>("0.0", 0.0, 0.0)).isTrue(&data);
}
Data &thenData(data);

73
test/testexprengine.cpp
View File

@ -62,6 +62,11 @@ private:
TEST_CASE(if3);
TEST_CASE(if4);
TEST_CASE(if5);
TEST_CASE(ifAlwaysTrue1);
TEST_CASE(ifAlwaysTrue2);
TEST_CASE(ifAlwaysTrue3);
TEST_CASE(ifAlwaysFalse1);
TEST_CASE(ifAlwaysFalse2);
TEST_CASE(ifelse1);
TEST_CASE(ifif);
TEST_CASE(ifreturn);
@ -152,6 +157,7 @@ private:
}
replace(line, "(fp.gt ", "(> ");
replace(line, "(fp.lt ", "(< ");
replace(line, "(_ +zero 11 53)", "0.0");
replace(line, "(fp #b0 #b10000000010 #x899999999999a)", "12.3");
replace(line, "(/ 123.0 10.0)", "12.3");
int par = 0;
@ -448,6 +454,73 @@ private:
expr("void foo(const int *x) { if (f1() && *x > 12) dostuff(*x == 5); }", "=="));
}
void ifAlwaysTrue1() {
const char code[] = "int foo() {\n"
" int a = 42;\n"
" if (1) {\n"
" a = 0;\n"
" }\n"
" return a == 0;\n"
"}";
const char expected[] = "(distinct 1 0)\n"
"(= 0 0)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifAlwaysTrue2() {
const char code[] = "int foo() {\n"
" int a = 42;\n"
" if (12.3) {\n"
" a = 0;\n"
" }\n"
" return a == 0;\n"
"}";
const char expected[] = "(distinct 12.3 0.0)\n"
"(= 0 0)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifAlwaysTrue3() {
const char code[] = "int foo() {\n"
" int a = 42;\n"
" if (\"test\") {\n"
" a = 0;\n"
" }\n"
" return a == 0;\n"
"}";
// String literals are always true. z3 will not be involved.
ASSERT_EQUALS("", expr(code, "=="));
}
void ifAlwaysFalse1() {
const char code[] = "int foo() {\n"
" int a = 42;\n"
" if (0) {\n"
" a = 0;\n"
" }\n"
" return a == 0;\n"
"}";
const char expected[] = "(= 0 0)\n"
"(= 42 0)\n"
"z3::unsat\n";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifAlwaysFalse2() {
const char code[] = "int foo() {\n"
" int a = 42;\n"
" if (0.0) {\n"
" a = 0;\n"
" }\n"
" return a == 0;\n"
"}";
const char expected[] = "(= 0.0 0.0)\n"
"(= 42 0)\n"
"z3::unsat\n";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifelse1() {
ASSERT_EQUALS("(<= $1 5)\n"