From a7096f748b0c4a0979aeb488ebc6ddef96087e7a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 17 May 2020 16:51:39 +0200 Subject: [PATCH] Fix segfault for empty spare modules --- src/storm-dft/storage/dft/DFT.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 0e00c4423..75d43eb47 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -754,14 +754,17 @@ namespace storm { // Check independence of spare modules // TODO: comparing one element of each spare module sufficient? for (auto module1 = mSpareModules.begin(); module1 != mSpareModules.end(); ++module1) { - size_t firstElement = module1->second.front(); - for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) { - if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) { - if (!wellformed) { - stream << std::endl; + if (!module1->second.empty()) { + // Empty modules are allowed for the primary module of a spare gate + size_t firstElement = module1->second.front(); + for (auto module2 = std::next(module1); module2 != mSpareModules.end(); ++module2) { + if (std::find(module2->second.begin(), module2->second.end(), firstElement) != module2->second.end()) { + if (!wellformed) { + stream << std::endl; + } + stream << "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap."; + wellformed = false; } - stream << "Spare modules of '" << getElement(module1->first)->name() << "' and '" << getElement(module2->first)->name() << "' should not overlap."; - wellformed = false; } } }