diff --git a/cfg/cppunit.cfg b/cfg/cppunit.cfg
index 8db767f20..b32d79b26 100644
--- a/cfg/cppunit.cfg
+++ b/cfg/cppunit.cfg
@@ -5,13 +5,13 @@
-
-
-
-
-
-
-
+
+
+
+
+
+
+
diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
index 088826c96..8061061f1 100644
--- a/lib/CMakeLists.txt
+++ b/lib/CMakeLists.txt
@@ -37,7 +37,13 @@ else()
endif()
add_library(lib_objs OBJECT ${srcs_lib} ${hdrs})
+if (CMAKE_VERSION VERSION_EQUAL "3.16" OR CMAKE_VERSION VERSION_GREATER "3.16")
+ target_precompile_headers(lib_objs PRIVATE precompiled.h)
+endif()
if (ENABLE_OSS_FUZZ AND CMAKE_CXX_COMPILER_ID MATCHES "Clang")
add_library(lib_objs_sanitized OBJECT EXCLUDE_FROM_ALL ${srcs_lib} ${hdrs})
target_compile_options(lib_objs_sanitized PRIVATE -fsanitize=address)
+ if (CMAKE_VERSION VERSION_EQUAL "3.16" OR CMAKE_VERSION VERSION_GREATER "3.16")
+ target_precompile_headers(lib_objs_sanitized PRIVATE precompiled.h)
+ endif()
endif()
diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 94f307a9f..2f239fd7c 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -204,7 +204,6 @@ namespace {
return;
mSymbols.insert(symbolicExpression);
mMap[tok].push_back(symbolicExpression + "=" + value->getRange());
-
}
void state(const Token *tok, const std::string &s) {
@@ -342,7 +341,8 @@ namespace {
mTrackExecution->symbolRange(tok, value);
if (value) {
if (auto arr = std::dynamic_pointer_cast(value)) {
- mTrackExecution->symbolRange(tok, arr->size);
+ for (const auto &dim: arr->size)
+ mTrackExecution->symbolRange(tok, dim);
for (const auto &indexAndValue: arr->data)
mTrackExecution->symbolRange(tok, indexAndValue.value);
} else if (auto s = std::dynamic_pointer_cast(value)) {
@@ -564,8 +564,8 @@ static int128_t truncateInt(int128_t value, int bits, char sign)
ExprEngine::ArrayValue::ArrayValue(const std::string &name, ExprEngine::ValuePtr size, ExprEngine::ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer)
: Value(name, ExprEngine::ValueType::ArrayValue)
, pointer(pointer), nullPointer(nullPointer), uninitPointer(uninitPointer)
- , size(size)
{
+ this->size.push_back(size);
assign(ExprEngine::ValuePtr(), value);
}
@@ -574,17 +574,16 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
, pointer(var->isPointer()), nullPointer(var->isPointer()), uninitPointer(var->isPointer())
{
if (var) {
- int sz = 1;
for (const auto &dim : var->dimensions()) {
- if (!dim.known) {
- sz = -1;
- break;
- }
- sz *= dim.num;
+ if (dim.known)
+ size.push_back(std::make_shared(std::to_string(dim.num), dim.num, dim.num));
+ else
+ size.push_back(std::make_shared(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE));
}
- if (sz >= 1)
- size = std::make_shared(std::to_string(sz), sz, sz);
+ } else {
+ size.push_back(std::make_shared(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE));
}
+
ValuePtr val;
if (var && !var->isGlobal() && !var->isStatic())
val = std::make_shared();
@@ -727,7 +726,12 @@ std::string ExprEngine::ConditionalValue::getSymbolicExpression() const
std::string ExprEngine::ArrayValue::getSymbolicExpression() const
{
std::ostringstream ostr;
- ostr << "size=" << (size ? size->name : std::string("(null)"));
+ if (size.empty())
+ ostr << "(null)";
+ else {
+ for (const auto &dim: size)
+ ostr << "[" << (dim ? dim->name : std::string("(null)")) << "]";
+ }
for (const auto &indexAndValue : data) {
ostr << ",["
<< (!indexAndValue.index ? std::string(":") : indexAndValue.index->name)
@@ -1252,6 +1256,47 @@ static void call(const std::vector &callbacks, const Token
static ExprEngine::ValuePtr executeExpression(const Token *tok, Data &data);
static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data);
+static ExprEngine::ValuePtr calculateArrayIndex(const Token *tok, Data &data, const ExprEngine::ArrayValue &arrayValue)
+{
+ int nr = 1;
+ const Token *tok2 = tok;
+ while (Token::simpleMatch(tok2->astOperand1(), "[")) {
+ tok2 = tok2->astOperand1();
+ nr++;
+ }
+
+ ExprEngine::ValuePtr totalIndex;
+ ExprEngine::ValuePtr dim;
+ while (Token::simpleMatch(tok, "[")) {
+ auto rawIndex = executeExpression(tok->astOperand2(), data);
+
+ ExprEngine::ValuePtr index;
+ if (dim)
+ index = simplifyValue(std::make_shared("*", dim, rawIndex));
+ else
+ index = rawIndex;
+
+ if (!totalIndex)
+ totalIndex = index;
+ else
+ totalIndex = simplifyValue(std::make_shared("+", index, totalIndex));
+
+ if (arrayValue.size.size() >= nr) {
+ if (arrayValue.size[nr-1]) {
+ if (!dim)
+ dim = arrayValue.size[nr-1];
+ else
+ dim = simplifyValue(std::make_shared("*", dim, arrayValue.size[nr-1]));
+ }
+ }
+
+ nr--;
+ tok = tok->astOperand1();
+ }
+
+ return totalIndex;
+}
+
static ExprEngine::ValuePtr executeReturn(const Token *tok, Data &data)
{
ExprEngine::ValuePtr retval = executeExpression(tok->astOperand1(), data);
@@ -1334,15 +1379,18 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
if (lhsToken->varId() > 0) {
data.assignValue(lhsToken, lhsToken->varId(), assignValue);
} else if (lhsToken->str() == "[") {
- auto arrayValue = data.getArrayValue(lhsToken->astOperand1());
+ const Token *tok2 = lhsToken;
+ while (Token::simpleMatch(tok2->astOperand1(), "["))
+ tok2 = tok2->astOperand1();
+ auto arrayValue = data.getArrayValue(tok2->astOperand1());
if (arrayValue) {
// Is it array initialization?
- const Token *arrayInit = lhsToken->astOperand1();
+ const Token *arrayInit = tok2->astOperand1();
if (arrayInit && arrayInit->variable() && arrayInit->variable()->nameToken() == arrayInit) {
if (assignValue->type == ExprEngine::ValueType::StringLiteralValue)
arrayValue->assign(ExprEngine::ValuePtr(), assignValue);
} else {
- auto indexValue = executeExpression(lhsToken->astOperand2(), data);
+ auto indexValue = calculateArrayIndex(lhsToken, data, *arrayValue);
arrayValue->assign(indexValue, assignValue);
}
}
@@ -1511,9 +1559,12 @@ static ExprEngine::ValuePtr executeFunctionCall(const Token *tok, Data &data)
static ExprEngine::ValuePtr executeArrayIndex(const Token *tok, Data &data)
{
- auto arrayValue = data.getArrayValue(tok->astOperand1());
+ const Token *tok2 = tok;
+ while (Token::simpleMatch(tok2->astOperand1(), "["))
+ tok2 = tok2->astOperand1();
+ auto arrayValue = data.getArrayValue(tok2->astOperand1());
if (arrayValue) {
- auto indexValue = executeExpression(tok->astOperand2(), data);
+ auto indexValue = calculateArrayIndex(tok, data, *arrayValue);
auto conditionalValues = arrayValue->read(indexValue);
for (auto value: conditionalValues)
call(data.callbacks, tok, value.second, &data);
diff --git a/lib/exprengine.h b/lib/exprengine.h
index 4d7581d29..b76a3f650 100644
--- a/lib/exprengine.h
+++ b/lib/exprengine.h
@@ -204,7 +204,7 @@ namespace ExprEngine {
ValuePtr value;
};
std::vector data;
- ValuePtr size;
+ std::vector size;
};
class StringLiteralValue: public Value {
diff --git a/lib/templatesimplifier.cpp b/lib/templatesimplifier.cpp
index 51bfd36ad..a92c9a130 100644
--- a/lib/templatesimplifier.cpp
+++ b/lib/templatesimplifier.cpp
@@ -1986,6 +1986,9 @@ void TemplateSimplifier::expandTemplate(
} else if (typeindentlevel > 0 && typetok->str() == ">" && brackets1.top()->str() == "<") {
--typeindentlevel;
brackets1.pop();
+ } else if (Token::Match(typetok, "const_cast|dynamic_cast|reinterpret_cast|static_cast <")) {
+ brackets1.push(typetok->next());
+ ++typeindentlevel;
} else if (typetok->str() == "(")
++typeindentlevel;
else if (typetok->str() == ")")
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index e3af00370..0740b6d28 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -27,6 +27,10 @@ if (BUILD_TESTS)
target_link_libraries(testrunner ${Z3_LIBRARIES})
endif()
+ if (CMAKE_VERSION VERSION_EQUAL "3.16" OR CMAKE_VERSION VERSION_GREATER "3.16")
+ target_precompile_headers(testrunner PRIVATE precompiled.h)
+ endif()
+
add_custom_target(copy_cfg ALL
COMMENT "Copying cfg files")
add_custom_command(
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index dcb80812d..c093417d4 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -70,6 +70,7 @@ private:
TEST_CASE(array2);
TEST_CASE(array3);
TEST_CASE(array4);
+ TEST_CASE(array5);
TEST_CASE(arrayInit1);
TEST_CASE(arrayInit2);
TEST_CASE(arrayUninit);
@@ -509,7 +510,20 @@ private:
"void f() { int x = buf[0]; }";
ASSERT_EQUALS("2:16: $2:0=-2147483648:2147483647\n"
"2:20: $2=-2147483648:2147483647\n"
- "2:26: { buf=($1,size=10,[:]=$2) x=$2:0}\n",
+ "2:26: { buf=($1,[10],[:]=$2) x=$2:0}\n",
+ trackExecution(code));
+ }
+
+ void array5() {
+ const char code[] = "int f(int x) {\n"
+ " int buf[3][4][5];\n"
+ " buf[x][1][2] = 10;\n"
+ " return buf[0][1][2];\n"
+ "}";
+ ASSERT_EQUALS("1:14: $1=-2147483648:2147483647\n"
+ "1:14: { x=$1}\n"
+ "2:19: { x=$1 buf=($2,[3][4][5],[:]=?)}\n"
+ "3:20: { x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n",
trackExecution(code));
}
@@ -531,7 +545,7 @@ private:
" for (int i = 0; i < 3; i++) arr[i][0] = arr[1][2];\n"
" return arr[0][0];"
"}";
- ASSERT_EQUALS("?", getRange(code, "arr[1]"));
+ ASSERT_EQUALS("?", getRange(code, "arr[1][2]"));
}
@@ -601,7 +615,7 @@ private:
void pointer1() {
const char code[] = "void f(unsigned char *p) { return *p == 7; }";
- ASSERT_EQUALS("size=$1,[:]=?,null", getRange(code, "p"));
+ ASSERT_EQUALS("[$1],[:]=?,null", getRange(code, "p"));
ASSERT_EQUALS("(and (>= $3 0) (<= $3 255))\n"
"(= $3 7)\n"
"z3::sat\n",
diff --git a/test/testsimplifytemplate.cpp b/test/testsimplifytemplate.cpp
index 77c268df6..eb520527c 100644
--- a/test/testsimplifytemplate.cpp
+++ b/test/testsimplifytemplate.cpp
@@ -256,6 +256,8 @@ private:
TEST_CASE(template_variable_4);
TEST_CASE(simplifyDecltype);
+
+ TEST_CASE(castInExpansion);
}
std::string tok(const char code[], bool debugwarnings = false, Settings::PlatformType type = Settings::Native) {
@@ -5129,6 +5131,21 @@ private:
"class type { } ;";
ASSERT_EQUALS(expected, tok(code));
}
+
+ void castInExpansion() {
+ const char code[] = "template class C { };\n"
+ "template class Base {};\n"
+ "template class Derived : private Base {};\n"
+ "typedef Derived(-1)> > C_;\n"
+ "class C3 { C_ c; };";
+ const char expected[] = "template < int N > class C { } ; "
+ "class Base-1>> ; "
+ "class Derived-1>> ; "
+ "class C3 { Derived-1>> c ; } ; "
+ "class Derived-1>> : private Base-1>> { } ; "
+ "class Base-1>> { } ;";
+ ASSERT_EQUALS(expected, tok(code));
+ }
};
REGISTER_TEST(TestSimplifyTemplate)
diff --git a/tools/donate_cpu_lib.py b/tools/donate_cpu_lib.py
index 4845addfe..78529fbe8 100644
--- a/tools/donate_cpu_lib.py
+++ b/tools/donate_cpu_lib.py
@@ -43,7 +43,7 @@ def get_cppcheck(cppcheck_path, work_path):
os.chdir(cppcheck_path)
try:
subprocess.check_call(['git', 'checkout', '-f', 'main'])
- except CalledProcessError:
+ except subprocess.CalledProcessError:
subprocess.check_call(['git', 'checkout', '-f', 'master'])
subprocess.check_call(['git', 'pull'])
subprocess.check_call(['git', 'checkout', 'origin/main', '-b', 'main'])