ExprEngine: Arrays if-then-else
This commit is contained in:
parent
555890fdfa
commit
f80d387374
|
@ -554,6 +554,18 @@ static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData)
|
||||||
return getExpr(b.get(), exprData);
|
return getExpr(b.get(), exprData);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (auto c = std::dynamic_pointer_cast<ExprEngine::ConditionalValue>(v)) {
|
||||||
|
if (c->values.size() == 1)
|
||||||
|
return ::getExpr(c->values[0].second, exprData);
|
||||||
|
|
||||||
|
return z3::ite(::getExpr(c->values[1].first, exprData),
|
||||||
|
::getExpr(c->values[1].second, exprData),
|
||||||
|
::getExpr(c->values[0].second, exprData));
|
||||||
|
}
|
||||||
|
|
||||||
|
if (v->type == ExprEngine::ValueType::UninitValue)
|
||||||
|
return exprData.c.int_val(0);
|
||||||
|
|
||||||
throw std::runtime_error("Internal error: Unhandled value type");
|
throw std::runtime_error("Internal error: Unhandled value type");
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -197,7 +197,11 @@ private:
|
||||||
void array3() {
|
void array3() {
|
||||||
const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }";
|
const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }";
|
||||||
ASSERT_EQUALS("?,43", getRange(code, "arr[x]"));
|
ASSERT_EQUALS("?,43", getRange(code, "arr[x]"));
|
||||||
// TODO: ASSERT_EQUALS("", expr(code, "=="));
|
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
|
||||||
|
"(assert (<= v0 255))\n"
|
||||||
|
"(assert (>= v0 0))\n"
|
||||||
|
"(assert (= (ite (= v0 4) 43 0) 12))\n",
|
||||||
|
expr(code, "=="));
|
||||||
}
|
}
|
||||||
|
|
||||||
void array4() {
|
void array4() {
|
||||||
|
|
Loading…
Reference in New Issue