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

ExprEngine; Fix floating point comparison

This commit is contained in:
Daniel Marjamäki 2020-12-21 13:23:08 +01:00
parent c22290f5a3
commit c3e798968c
2 changed files with 24 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
lib/exprengine.cpp
View File

@ -1215,6 +1215,13 @@ public:
}
if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
if (floatRange->name[0] != '$')
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return context.fpa_val(static_cast<double>(floatRange->minValue));
#else
return context.real_val(floatRange->name.c_str());
#endif
auto it = valueExpr.find(v->name);
if (it != valueExpr.end())
return it->second;

19
test/testexprengine.cpp
View File

@ -105,6 +105,7 @@ private:
TEST_CASE(functionCall5);
TEST_CASE(functionCallContract1);
TEST_CASE(functionCallContract2);
TEST_CASE(int1);
@ -151,6 +152,7 @@ private:
}
replace(line, "(fp.gt ", "(> ");
replace(line, "(fp.lt ", "(< ");
replace(line, "(fp #b0 #b10000000010 #x899999999999a)", "12.3");
int par = 0;
for (char pos : line) {
if (pos == '(')
@ -751,8 +753,8 @@ private:
}
void floatValue3() {
const char code[] = "void foo(float f) { return f > 12.0; }";
const char expected[] = "(> $1 |12.0|)\n"
const char code[] = "void foo(float f) { return f > 12.3; }";
const char expected[] = "(> $1 12.3)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, ">"));
}
@ -805,6 +807,19 @@ private:
functionCallContractExpr(code, s));
}
void functionCallContract2() {
const char code[] = "void foo(float x);\n"
"void bar(float x) { foo(x); }";
Settings s;
s.functionContracts["foo(x)"] = "x < 12.3";
ASSERT_EQUALS("checkContract:{\n"
"(ite (< $2 12.3) false true)\n"
"}\n",
functionCallContractExpr(code, s));
}
void int1() {
ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n"