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

ExprEngine; Fix problem when float suffix is used

This commit is contained in:
Daniel Marjamäki 2020-12-22 15:17:36 +01:00
parent 347fccb207
commit 1812951640
2 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/exprengine.cpp
View File

@ -1278,12 +1278,14 @@ public:
#endif #endif
} }
z3::expr z3_fp_val(long double value, const std::string &name) { z3::expr z3_fp_val(long double value, std::string name) {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0) #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
(void)name; (void)name;
return context.fpa_val(static_cast<double>(value)); return context.fpa_val(static_cast<double>(value));
#else #else
(void)value; (void)value;
while (name.size() > 1 && (name.back() == 'f' || name.back() == 'F' || name.back() == 'l' || name.back() == 'L'))
name.erase(name.size() - 1);
return context.real_val(name.c_str()); return context.real_val(name.c_str());
#endif #endif
} }

8
test/testexprengine.cpp
View File

@ -102,6 +102,7 @@ private:
TEST_CASE(floatValue1); TEST_CASE(floatValue1);
TEST_CASE(floatValue2); TEST_CASE(floatValue2);
TEST_CASE(floatValue3); TEST_CASE(floatValue3);
TEST_CASE(floatValue4);
TEST_CASE(functionCall1); TEST_CASE(functionCall1);
TEST_CASE(functionCall2); TEST_CASE(functionCall2);
@ -827,6 +828,13 @@ private:
ASSERT_EQUALS(expected, expr(code, ">")); ASSERT_EQUALS(expected, expr(code, ">"));
} }
void floatValue4() {
const char code[] = "void foo(float f) { return f > 12.3f; }";
const char expected[] = "(> $1 12.3)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, ">"));
}
void functionCall1() { void functionCall1() {
ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x")); ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));