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

Verification: Handle Cppcheck annotations __cppcheck_low__ and __cppcheck_high__

This commit is contained in:
Daniel Marjamäki 2019-12-24 21:14:14 +01:00
parent 755e2d261c
commit f0ac19514b
2 changed files with 31 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
lib/exprengine.cpp
View File

@ -286,6 +286,16 @@ namespace {
constraints.push_back(std::make_shared<ExprEngine::BinOpResult>(equals?"==":"!=", lhsValue, rhsValue));
}
void addConstraints(ExprEngine::ValuePtr value, const Token *tok) {
MathLib::bigint low;
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::LOW, &low))
addConstraint(std::make_shared<ExprEngine::BinOpResult>(">=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(low), low, low)), true);
MathLib::bigint high;
if (tok->getCppcheckAttribute(TokenImpl::CppcheckAttributes::Type::HIGH, &high))
addConstraint(std::make_shared<ExprEngine::BinOpResult>("<=", value, std::make_shared<ExprEngine::IntRange>(std::to_string(high), high, high)), true);
}
private:
TrackExecution * const mTrackExecution;
const int mDataIndex;
@ -1455,8 +1465,11 @@ static ExprEngine::ValuePtr createVariableValue(const Variable &var, Data &data)
}
if (var.isArray())
return std::make_shared<ExprEngine::ArrayValue>(&data, &var);
if (valueType->isIntegral())
return getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
if (valueType->isIntegral()) {
auto value = getValueRangeFromValueType(data.getNewSymbolName(), valueType, *data.settings);
data.addConstraints(value, var.nameToken());
return value;
}
if (valueType->type == ValueType::Type::RECORD)
return createStructVal(valueType->typeScope, var.isLocal() && !var.isStatic(), data);
if (valueType->smartPointerType) {

16
test/testexprengine.cpp
View File

@ -33,6 +33,8 @@ public:
private:
void run() OVERRIDE {
#ifdef USE_Z3
TEST_CASE(annotation1);
TEST_CASE(expr1);
TEST_CASE(expr2);
TEST_CASE(expr3);
@ -143,6 +145,20 @@ private:
return ret.str();
}
void annotation1() {
const char code[] = "void f(__cppcheck_low__(100) short x) {\n"
" return x < 10;\n"
"}";
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
"(assert (>= $1 100))\n" // <- annotation
"(assert (< $1 10))\n"
"z3::unsat";
ASSERT_EQUALS(expected, expr(code, "<"));
}
void expr1() {
ASSERT_EQUALS("-32768:32767", getRange("void f(short x) { a = x; }", "x"));
}