Temp

Author: sava-cska

server/src/KleeRunner.cpp

@@ -138,35 +138,35 @@ static void processMethod(MethodKtests &ktestChunk,
     bool hasError = false;
     for (auto const &entry : fs::directory_iterator(kleeOut)) {
         auto const &path = entry.path();
-        if (Paths::isKtestJson(path)) {
+        if (Paths::isKtest(path)) {
             if (Paths::hasEarly(path)) {
                 hasTimeout = true;
             } else if (Paths::hasInternalError(path)) {
                 hasError = true;
             } else {
-                std::unique_ptr<TestCase, decltype(&TestCase_free)> ktestData{
-                    TC_fromFile(path.c_str()), TestCase_free
+                std::unique_ptr<KTest, decltype(&kTest_free)> ktestData{
+                    kTest_fromFile(path.c_str()), kTest_free
                 };
                 if (ktestData == nullptr) {
-                    LOG_S(WARNING) << "Unable to open .ktestjson file";
+                    LOG_S(WARNING) << "Unable to open .ktest file";
                     continue;
                 }
                 const std::vector<fs::path> &errorDescriptorFiles =
-                        Paths::getErrorDescriptors(path);
+                    Paths::getErrorDescriptors(path);
 
                 UTBotKTest::Status status = errorDescriptorFiles.empty()
-                                            ? UTBotKTest::Status::SUCCESS
-                                            : UTBotKTest::Status::FAILED;
-                std::vector<ConcretizedObject> kTestObjects(
-                    ktestData->objects, ktestData->objects + ktestData->n_objects);
+                                                ? UTBotKTest::Status::SUCCESS
+                                                : UTBotKTest::Status::FAILED;
+                std::vector<KTestObject> kTestObjects(ktestData->objects,
+                                                      ktestData->objects + ktestData->numObjects);
 
-                std::vector<UTBotKTestObject> objects = CollectionUtils::transform(
-                    kTestObjects, [](const ConcretizedObject &kTestObject) {
+                std::vector<UTBotKTestObject> objects =
+                    CollectionUtils::transform(kTestObjects, [](const KTestObject &kTestObject) {
                         return UTBotKTestObject{ kTestObject };
                     });
 
-                std::vector<std::string> errorDescriptors = CollectionUtils::transform(
-                    errorDescriptorFiles, [](const fs::path &errorFile) {
+                std::vector<std::string> errorDescriptors =
+                    CollectionUtils::transform(errorDescriptorFiles, [](const fs::path &errorFile) {
                         std::ifstream fileWithError(errorFile.c_str(), std::ios_base::in);
                         std::string content((std::istreambuf_iterator<char>(fileWithError)),
                                             std::istreambuf_iterator<char>());
@@ -219,18 +219,19 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
                                           "--libc=klee",
                                           "--utbot",
                                           "--posix-runtime",
+                                          "--skip-not-lazy-initialized",
                                           "--type-system=CXX",
                                           "--fp-runtime",
                                           "--only-output-states-covering-new",
                                           "--allocate-determ",
                                           "--external-calls=all",
                                           "--timer-interval=1000ms",
-                                          "--bcov-check-interval=8s",
+                                          "--use-cov-check=instruction-based",
                                           "-istats-write-interval=5s",
                                           "--disable-verify",
                                           "--check-div-zero=false",
                                           "--check-overshift=false",
-                                          "--skip-not-lazy-and-symbolic-pointers",
+                                          "--skip-not-symbolic-objects",
                                           "--output-dir=" + kleeOut.string()};
     if (settingsContext.useDeterministicSearcher) {
         argvData.emplace_back("--search=dfs");