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

ExprEngine; add a 'stupid' handling of floating point promotions for integers

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

15
lib/exprengine.cpp
View File

@ -1155,6 +1155,14 @@ public:
auto op1 = getExpr(b->op1);
auto op2 = getExpr(b->op2);
// floating point promotion
if (b->binop != "&&" && b->binop != "||" && b->binop != "<<" && b->binop != ">>") {
if (z3_is_fp(op1) || z3_is_fp(op2)) {
z3_to_fp(op1);
z3_to_fp(op2);
}
}
if (b->binop == "+")
return op1 + op2;
if (b->binop == "-")
@ -1298,6 +1306,13 @@ public:
#endif
}
int floatSymbol = 0;
void z3_to_fp(z3::expr &e) {
if (e.is_int())
// TODO: Is there a better way to promote e?
e = z3_fp_const("f" + std::to_string(++floatSymbol));
}
z3::expr z3_int_val(int128_t value) {
#if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1)
return context.int_val(int64_t(value));

7
test/testexprengine.cpp
View File

@ -103,6 +103,7 @@ private:
TEST_CASE(floatValue2);
TEST_CASE(floatValue3);
TEST_CASE(floatValue4);
TEST_CASE(floatValue5);
TEST_CASE(functionCall1);
TEST_CASE(functionCall2);
@ -835,6 +836,12 @@ private:
ASSERT_EQUALS(expected, expr(code, ">"));
}
void floatValue5() { // float < int
const char code[] = "void foo(float f) { if (f < 1){} }";
const char expected[] = "(< $1 f1)\n" // TODO: The "f1" should be something like (float)1
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "<"));
}
void functionCall1() {
ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));