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

Revert "ExprEngine: Fixed float value" 

This reverts commit 1f9edc6a66.
This commit is contained in:
Daniel Marjamäki 2020-12-20 16:36:22 +01:00
parent 40e24cf417
commit 229e39e7de
2 changed files with 2 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
lib/exprengine.cpp
View File

@ -1211,13 +1211,6 @@ public:
}
if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
if (std::isdigit(floatRange->name[0]))
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return context.fpa_val(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;

18
test/testexprengine.cpp
View File

@ -103,7 +103,6 @@ private:
TEST_CASE(functionCall5);
TEST_CASE(functionCallContract1);
TEST_CASE(functionCallContract2);
TEST_CASE(int1);
@ -716,8 +715,8 @@ private:
}
void floatValue3() {
const char code[] = "void foo(float f) { return f > 12.3; }";
const char expected[] = "(> $1 (/ 123.0 10.0))\n"
const char code[] = "void foo(float f) { return f > 12.0; }";
const char expected[] = "(> $1 |12.0|)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, ">"));
}
@ -770,19 +769,6 @@ 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 >= 0.5";
ASSERT_EQUALS("checkContract:{\n"
"(ite (>= $2 (/ 1.0 2.0)) false true)\n"
"}\n",
functionCallContractExpr(code, s));
}
void int1() {
ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n"