ExprEngine; Fixed bug. Constraint expressions must be boolean

This commit is contained in:
Daniel Marjamäki 2020-05-27 19:37:07 +02:00
parent d87680f965
commit f482eb49cd
3 changed files with 70 additions and 1 deletions

View File

@ -890,7 +890,7 @@ struct ExprData {
z3::expr getConstraintExpr(ExprEngine::ValuePtr v) {
if (v->type == ExprEngine::ValueType::IntRange)
return (getExpr(v) != 0);
return getExpr(v);
return bool_expr(getExpr(v));
}
private:
@ -2527,3 +2527,60 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer,
else if (errorLogger)
errorLogger->bughuntingReport(report.str());
}
static void dumpRecursive(ExprEngine::ValuePtr val)
{
if (!val)
std::cout << "NULL";
switch (val->type) {
case ExprEngine::ValueType::AddressOfValue:
std::cout << "AddressOfValue(" << std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(val)->varId << ")";
break;
case ExprEngine::ValueType::ArrayValue:
std::cout << "ArrayValue";
break;
case ExprEngine::ValueType::BailoutValue:
std::cout << "BailoutValue";
break;
case ExprEngine::ValueType::BinOpResult: {
auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(val);
std::cout << "(";
dumpRecursive(b->op1);
std::cout << " " << b->binop << " ";
dumpRecursive(b->op2);
std::cout << ")";
}
break;
case ExprEngine::ValueType::ConditionalValue:
std::cout << "ConditionalValue";
break;
case ExprEngine::ValueType::FloatRange:
std::cout << "FloatRange";
break;
case ExprEngine::ValueType::IntRange:
std::cout << "IntRange";
break;
case ExprEngine::ValueType::IntegerTruncation:
std::cout << "IntegerTruncation(";
dumpRecursive(std::dynamic_pointer_cast<ExprEngine::IntegerTruncation>(val)->inputValue);
std::cout << ")";
break;
case ExprEngine::ValueType::StringLiteralValue:
std::cout << "StringLiteralValue";
break;
case ExprEngine::ValueType::StructValue:
std::cout << "StructValue";
break;
case ExprEngine::ValueType::UninitValue:
std::cout << "UninitValue";
break;
}
}
void ExprEngine::dump(ExprEngine::ValuePtr val)
{
dumpRecursive(val);
std::cout << "\n";
}

View File

@ -310,5 +310,7 @@ namespace ExprEngine {
void executeFunction(const Scope *functionScope, ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings, const std::vector<Callback> &callbacks, std::ostream &report);
void runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer, const Settings *settings);
void dump(ExprEngine::ValuePtr val);
}
#endif // exprengineH

View File

@ -46,6 +46,7 @@ private:
TEST_CASE(expr5);
TEST_CASE(expr6);
TEST_CASE(expr7);
TEST_CASE(expr8);
TEST_CASE(exprAssign1);
TEST_CASE(exprAssign2); // Truncation
@ -302,6 +303,15 @@ private:
expr(code, ">"));
}
void expr8() {
const char code[] = "void foo(int x, int y) {\n"
" if (x % 32) {}\n"
" y==3;\n"
"}";
// Do not crash
expr(code, "==");
}
void exprAssign1() {
ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
}