diff --git a/CMakeLists.txt b/CMakeLists.txt index 52cf0f1a3..99386c34b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -171,3 +171,6 @@ configure_file ( "${PROJECT_SOURCE_DIR}/mrmc-config.h.in" "${PROJECT_BINARY_DIR}/mrmc-config.h" ) + +add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ./mrmc examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab) +add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ./mrmc-tests) diff --git a/src/formula/AP.h b/src/formula/AP.h index 8bda0df06..8c9f7ad16 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -59,7 +59,7 @@ public: /*! * @returns the name of the atomic proposition */ - std::string getAP() { + const std::string& getAP() { return ap; } diff --git a/src/formula/And.h b/src/formula/And.h index 16f0b6d8e..12d8d38da 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -91,15 +91,15 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula* getLeft() { - return left; + PCTLStateFormula& getLeft() { + return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula* getRight() { - return right; + PCTLStateFormula& getRight() { + return *right; } /*! diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index c0061691c..9d7cf65f3 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -97,15 +97,15 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula* getLeft() { - return left; + PCTLStateFormula& getLeft() { + return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula* getRight() { - return right; + PCTLStateFormula& getRight() { + return *right; } /*! diff --git a/src/formula/Next.h b/src/formula/Next.h index 4ec120b80..98f5d9533 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -65,8 +65,8 @@ public: /*! * @returns the child node */ - PCTLStateFormula* getChild() { - return child; + PCTLStateFormula& getChild() { + return *child; } /*! diff --git a/src/formula/Not.h b/src/formula/Not.h index dfcb7c100..09782530a 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -60,8 +60,8 @@ public: /*! * @returns The child node */ - PCTLStateFormula* getChild() { - return child; + PCTLStateFormula& getChild() { + return *child; } /*! diff --git a/src/formula/Or.h b/src/formula/Or.h index 51a2f88fd..a5072b02a 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -90,15 +90,15 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula* getLeft() { - return left; + PCTLStateFormula& getLeft() { + return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula* getRight() { - return right; + PCTLStateFormula& getRight() { + return *right; } /*! diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index b0585fd58..622c2effc 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -73,21 +73,21 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - PCTLPathFormula* getPathFormula () { - return pathFormula; + PCTLPathFormula& getPathFormula () { + return *pathFormula; } /*! * @returns the lower bound for the probability */ - T getLowerBound() { + const T& getLowerBound() { return lower; } /*! * @returns the upper bound for the probability */ - T getUpperBound() { + const T& getUpperBound() { return upper; } diff --git a/src/formula/Until.h b/src/formula/Until.h index df80ee0e0..be02eb5d9 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -90,15 +90,15 @@ public: /*! * @returns a pointer to the left child node */ - PCTLStateFormula* getLeft() { - return left; + PCTLStateFormula& getLeft() { + return *left; } /*! * @returns a pointer to the right child node */ - PCTLStateFormula* getRight() { - return right; + PCTLStateFormula& getRight() { + return *right; } /*! diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 0ed215a86..457d2f6a1 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -10,25 +10,9 @@ #include "src/storage/BitVector.h" #include - -/* Map types: By default, the boost hash map is used. - * If the macro USE_STD_MAP is defined, the default C++ class (std::map) - * is used instead. - */ -#ifdef USE_STD_MAP -# include -# define MAP std::map -#else -# ifdef USE_STD_UNORDERED_MAP -# include -# define MAP std::unordered_map -# else -# include "boost/unordered_map.hpp" -# define MAP boost::unordered_map -# endif -#endif - #include +#include +#include namespace mrmc { @@ -230,7 +214,7 @@ private: * by mapping the name to a specific index in the array of all * individual labelings. */ - MAP nameToLabelingMap; + std::unordered_map nameToLabelingMap; /*! * Stores all individual labelings. To find the labeling associated with diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 252d6dcc1..932673be4 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -106,6 +106,9 @@ int main(const int argc, const char* argv[]) { if (s != nullptr) { delete s; } + + delete labparser.getLabeling(); + delete traparser.getMatrix(); LOG4CPLUS_INFO(logger, "Nothing more to do, exiting."); diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index d53e1c424..ba56c44a0 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -46,6 +46,7 @@ namespace parser { * @return The pointer to the created labeling object. */ LabParser::LabParser(uint_fast64_t node_count, const char * filename) + : labeling(nullptr) { /* * open file @@ -124,7 +125,15 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename) { buf += cnt; cnt = strcspn(buf, separator); // position of next separator - if (cnt > 0) + if (cnt >= sizeof(proposition)) + { + /* + * if token is longer than our buffer, the following strncpy code might get risky... + */ + LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found."); + throw mrmc::exceptions::wrong_file_format(); + } + else if (cnt > 0) { /* * next token is: #DECLARATION: just skip it diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h index c5cd029f6..67aec1178 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/readLabFile.h @@ -11,11 +11,15 @@ namespace parser { /*! * @brief Load label file and return initialized AtomicPropositionsLabeling object. + * + * Note that this class creates a new AtomicPropositionsLabeling object that can + * be accessed via getLabeling(). However, it will not delete this object! */ class LabParser : Parser { public: LabParser(uint_fast64_t node_count, const char* filename); + mrmc::models::AtomicPropositionsLabeling* getLabeling() { return this->labeling; diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp index 45ed6e20b..0871bfebd 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/readTraFile.cpp @@ -118,6 +118,7 @@ uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode) */ TraParser::TraParser(const char * filename) + : matrix(nullptr) { /* * enforce locale where decimal point is '.' diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h index 813752db7..7ec735123 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/readTraFile.h @@ -11,12 +11,15 @@ namespace parser { /*! * @brief Load transition system from file and return initialized * StaticSparseMatrix object. + * + * Note that this class creates a new StaticSparseMatrix object that can be + * accessed via getMatrix(). However, it does not delete this object! */ class TraParser : Parser { public: TraParser(const char* filename); - + mrmc::storage::SquareSparseMatrix* getMatrix() { return this->matrix; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index c50f10a29..dca00e61d 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -112,17 +112,17 @@ public: if (initTrue) { // Finally, create the full bucket array. - bucketArray = new uint64_t[bucketCount]; + this->bucketArray = new uint64_t[bucketCount]; // Now initialize the values. for (uint_fast64_t i = 0; i < bucketCount; ++i) { - bucketArray[i] = -1ll; + this->bucketArray[i] = -1ll; } truncateLastBucket(); } else { // Finally, create the full bucket array. - bucketArray = new uint64_t[bucketCount](); + this->bucketArray = new uint64_t[bucketCount](); } } @@ -134,7 +134,7 @@ public: BitVector(const BitVector &bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) { LOG4CPLUS_WARN(logger, "Invoking copy constructor."); bucketArray = new uint64_t[bucketCount]; - std::copy(bv.bucketArray, bv.bucketArray + bucketCount, bucketArray); + std::copy(bv.bucketArray, bv.bucketArray + this->bucketCount, this->bucketArray); } //! Destructor @@ -142,8 +142,8 @@ public: * Destructor. Frees the underlying bucket array. */ ~BitVector() { - if (bucketArray != nullptr) { - delete[] bucketArray; + if (this->bucketArray != nullptr) { + delete[] this->bucketArray; } } @@ -178,7 +178,7 @@ public: } // Reserve a temporary array for copying. - uint_fast64_t* tempArray = new uint_fast64_t[newBucketCount]; + uint64_t* tempArray = new uint64_t[newBucketCount]; // Copy over the elements from the old bit vector. uint_fast64_t copySize = (newBucketCount <= bucketCount) ? newBucketCount : bucketCount; diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index ac5260599..fd9c0b904 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -112,19 +112,19 @@ public: */ ~SquareSparseMatrix() { setState(MatrixStatus::UnInitialized); - if (valueStorage != NULL) { + if (valueStorage != nullptr) { //free(value_storage); delete[] valueStorage; } - if (columnIndications != NULL) { + if (columnIndications != nullptr) { //free(column_indications); delete[] columnIndications; } - if (rowIndications != NULL) { + if (rowIndications != nullptr) { //free(row_indications); delete[] rowIndications; } - if (diagonalStorage != NULL) { + if (diagonalStorage != nullptr) { //free(diagonal_storage); delete[] diagonalStorage; } @@ -507,7 +507,7 @@ public: uint_fast64_t rowStart; uint_fast64_t rowEnd; uint_fast64_t zeroCount = 0; - for (uint_fast64_t row = 0; row <= rowCount; ++row) { + for (uint_fast64_t row = 0; row < rowCount; ++row) { rowStart = rowIndications[row]; rowEnd = rowIndications[row + 1]; while (rowStart < rowEnd) { @@ -518,7 +518,7 @@ public: } // Then add the elements on the diagonal. - for (uint_fast64_t i = 0; i <= rowCount; ++i) { + for (uint_fast64_t i = 0; i < rowCount; ++i) { if (diagonalStorage[i] == 0) zeroCount++; // tripletList.push_back(IntTriplet(i, i, diagonalStorage[i])); } diff --git a/test/storage/SquareSparseMatrixTest.cpp b/test/storage/SquareSparseMatrixTest.cpp index e10d6bf88..da42aacc4 100644 --- a/test/storage/SquareSparseMatrixTest.cpp +++ b/test/storage/SquareSparseMatrixTest.cpp @@ -157,6 +157,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) ASSERT_EQ(target, row * 10 + col); } } + + delete ssm; } TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) { @@ -187,6 +189,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) ASSERT_EQ(target, row * 10 + col); } } + + delete ssm; } TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) { @@ -234,6 +238,8 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target)); ASSERT_EQ(target, coeff.value()); } + + delete ssm; } TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) { @@ -281,6 +287,8 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target)); ASSERT_EQ(target, coeff.value()); } + + delete ssm; } TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) { @@ -311,4 +319,7 @@ TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) ASSERT_EQ(values[row * 10 + col], esm->coeff(row, col)); } } + + delete esm; + delete ssm; }