Skip to content

Commit 82a5a4b

Browse files
committed
Added regression test for pointers. Updated KLEE.
1 parent a4f9ebf commit 82a5a4b

File tree

3 files changed

+39
-1
lines changed

3 files changed

+39
-1
lines changed

server/test/framework/Regression_Tests.cpp

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -340,6 +340,42 @@ namespace {
340340
"f4");
341341
}
342342

343+
TEST_F(Regression_Test, Pointers_Alignment) {
344+
static const size_t HEX = 16;
345+
static const size_t NODE_ALIGNMENT = 8;
346+
347+
fs::path source = getTestFilePath("issue-195.c");
348+
auto [testGen, status] = createTestForFunction(source, NODE_ALIGNMENT);
349+
350+
ASSERT_TRUE(status.ok()) << status.error_message();
351+
352+
std::function<bool(const tests::Tests::TestCaseParamValue &)> checkAlignmentInNode =
353+
[&checkAlignmentInNode](const tests::Tests::TestCaseParamValue &param) {
354+
const auto stringPointer = param.view->getSubViews().at(1)->getEntryValue(nullptr);
355+
const size_t address = strtoull(stringPointer.c_str(), nullptr, HEX);
356+
bool result = (address % NODE_ALIGNMENT == 0);
357+
358+
for (const auto &innerLazyValueParam : param.lazyValues) {
359+
result &= checkAlignmentInNode(innerLazyValueParam);
360+
}
361+
return result;
362+
};
363+
364+
365+
checkTestCasePredicates(
366+
testGen.tests.at(source).methods.begin().value().testCases,
367+
std::vector<TestCasePredicate>(
368+
{ [&checkAlignmentInNode](const tests::Tests::MethodTestCase &testCase) {
369+
for (const auto &paramValue : testCase.paramValues) {
370+
if (!checkAlignmentInNode(paramValue)) {
371+
return false;
372+
}
373+
}
374+
return true;
375+
} }),
376+
"list_sum");
377+
}
378+
343379
TEST_F(Regression_Test, Generate_Folder) {
344380
fs::path folderPath = getTestFilePath("ISSUE-140");
345381
auto [testGen, status] = createTestForFolder(folderPath, true, true);

server/test/suites/regression/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,4 +49,6 @@ target_compile_definitions(issue-276 PUBLIC EXPORT2="")
4949
target_compile_definitions(issue-276 PUBLIC EXPORT3=4)
5050
target_compile_definitions(issue-276 PUBLIC EXPORT4="4")
5151

52+
add_library(issue-195 issue-195.c)
53+
5254
set_target_properties(regression PROPERTIES LINK_WHAT_YOU_USE TRUE)

0 commit comments

Comments
 (0)