Verification; struct pointer member
This commit is contained in:
parent
2710a94b4b
commit
9723b28385
|
@ -1142,9 +1142,20 @@ static ExprEngine::ValuePtr executeDot(const Token *tok, Data &data)
|
||||||
if (!structValue) {
|
if (!structValue) {
|
||||||
if (tok->originalName() == "->") {
|
if (tok->originalName() == "->") {
|
||||||
std::shared_ptr<ExprEngine::ArrayValue> pointerValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
|
std::shared_ptr<ExprEngine::ArrayValue> pointerValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(data.getValue(tok->astOperand1()->varId(), nullptr, nullptr));
|
||||||
if (pointerValue && pointerValue->pointer && pointerValue->data.size() == 1) {
|
if (pointerValue && pointerValue->pointer && !pointerValue->data.empty()) {
|
||||||
call(data.callbacks, tok->astOperand1(), pointerValue, &data);
|
call(data.callbacks, tok->astOperand1(), pointerValue, &data);
|
||||||
structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(pointerValue->data[0].value);
|
auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
|
||||||
|
ExprEngine::ValuePtr ret;
|
||||||
|
for (auto val: pointerValue->read(indexValue)) {
|
||||||
|
structValue = std::dynamic_pointer_cast<ExprEngine::StructValue>(val.second);
|
||||||
|
if (structValue) {
|
||||||
|
auto memberValue = structValue->getValueOfMember(tok->astOperand2()->str());
|
||||||
|
call(data.callbacks, tok, memberValue, &data);
|
||||||
|
if (!ret)
|
||||||
|
ret = memberValue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return ret;
|
||||||
} else {
|
} else {
|
||||||
call(data.callbacks, tok->astOperand1(), data.getValue(tok->astOperand1()->varId(), nullptr, nullptr), &data);
|
call(data.callbacks, tok->astOperand1(), data.getValue(tok->astOperand1()->varId(), nullptr, nullptr), &data);
|
||||||
}
|
}
|
||||||
|
@ -1524,11 +1535,16 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
|
||||||
if (valueType->pointer > 0) {
|
if (valueType->pointer > 0) {
|
||||||
if (var.isLocal())
|
if (var.isLocal())
|
||||||
return std::make_shared<ExprEngine::UninitValue>();
|
return std::make_shared<ExprEngine::UninitValue>();
|
||||||
|
auto bufferSize = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
|
||||||
|
ExprEngine::ValuePtr pointerValue;
|
||||||
|
if (valueType->type == ValueType::Type::RECORD)
|
||||||
|
pointerValue = createStructVal(valueType->typeScope, var.isLocal() && !var.isStatic(), data);
|
||||||
|
else {
|
||||||
ValueType vt(*valueType);
|
ValueType vt(*valueType);
|
||||||
vt.pointer = 0;
|
vt.pointer = 0;
|
||||||
auto range = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
|
pointerValue = getValueRangeFromValueType(data.getNewSymbolName(), &vt, *data.settings);
|
||||||
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 1, ~0UL);
|
}
|
||||||
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, range, true, true, true);
|
return std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), bufferSize, pointerValue, true, true, true);
|
||||||
}
|
}
|
||||||
if (var.isArray())
|
if (var.isArray())
|
||||||
return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
|
return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
|
||||||
|
|
|
@ -81,7 +81,8 @@ private:
|
||||||
TEST_CASE(pointerAlias4);
|
TEST_CASE(pointerAlias4);
|
||||||
TEST_CASE(pointerNull1);
|
TEST_CASE(pointerNull1);
|
||||||
|
|
||||||
TEST_CASE(structMember);
|
TEST_CASE(structMember1);
|
||||||
|
TEST_CASE(structMember2);
|
||||||
#endif
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -415,19 +416,19 @@ private:
|
||||||
|
|
||||||
void pointer1() {
|
void pointer1() {
|
||||||
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
|
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
|
||||||
ASSERT_EQUALS("size=$2,[:]=$1,null,->?", getRange(code, "p"));
|
ASSERT_EQUALS("size=$1,[:]=$2,null,->?", getRange(code, "p"));
|
||||||
ASSERT_EQUALS("(declare-fun |$1:0| () Int)\n"
|
ASSERT_EQUALS("(declare-fun |$2:0| () Int)\n"
|
||||||
"(assert (and (>= |$1:0| 0) (<= |$1:0| 255)))\n"
|
"(assert (and (>= |$2:0| 0) (<= |$2:0| 255)))\n"
|
||||||
"(assert (= |$1:0| 7))\n"
|
"(assert (= |$2:0| 7))\n"
|
||||||
"z3::sat",
|
"z3::sat",
|
||||||
expr(code, "=="));
|
expr(code, "=="));
|
||||||
}
|
}
|
||||||
|
|
||||||
void pointer2() {
|
void pointer2() {
|
||||||
const char code[] = "void f(unsigned char *p) { return p[2] == 7; }";
|
const char code[] = "void f(unsigned char *p) { return p[2] == 7; }";
|
||||||
ASSERT_EQUALS("(declare-fun |$1:2| () Int)\n"
|
ASSERT_EQUALS("(declare-fun |$2:2| () Int)\n"
|
||||||
"(assert (and (>= |$1:2| 0) (<= |$1:2| 255)))\n"
|
"(assert (and (>= |$2:2| 0) (<= |$2:2| 255)))\n"
|
||||||
"(assert (= |$1:2| 7))\n"
|
"(assert (= |$2:2| 7))\n"
|
||||||
"z3::sat",
|
"z3::sat",
|
||||||
expr(code, "=="));
|
expr(code, "=="));
|
||||||
}
|
}
|
||||||
|
@ -458,7 +459,7 @@ private:
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void structMember() {
|
void structMember1() {
|
||||||
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
|
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
|
||||||
"(declare-fun $3 () Int)\n"
|
"(declare-fun $3 () Int)\n"
|
||||||
"(assert (and (>= $2 0) (<= $2 255)))\n"
|
"(assert (and (>= $2 0) (<= $2 255)))\n"
|
||||||
|
@ -472,6 +473,17 @@ private:
|
||||||
"void f(struct S s) { return s.a + s.b == 0; }", "=="));
|
"void f(struct S s) { return s.a + s.b == 0; }", "=="));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void structMember2() {
|
||||||
|
const char code[] = "struct S { int x; };\n"
|
||||||
|
"void foo(struct S *s) { return s->x == 123; }";
|
||||||
|
|
||||||
|
const char expected[] = "(declare-fun $3 () Int)\n"
|
||||||
|
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
|
||||||
|
"(assert (= $3 123))\n"
|
||||||
|
"z3::sat";
|
||||||
|
|
||||||
|
ASSERT_EQUALS(expected, expr(code, "=="));
|
||||||
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
REGISTER_TEST(TestExprEngine)
|
REGISTER_TEST(TestExprEngine)
|
||||||
|
|
Loading…
Reference in New Issue