diff --git a/CMakeLists.txt b/CMakeLists.txt index f273e7f97..7065c87db 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,7 +24,7 @@ endif() #Configurations for GCC if(CMAKE_COMPILER_IS_GNUCC) - set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic") + set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -Werror -pedantic") # Turn on popcnt instruction if possible if (USE_POPCNT) diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h index 83b7ced16..86cb93e11 100644 --- a/src/models/atomic_propositions_labeling.h +++ b/src/models/atomic_propositions_labeling.h @@ -58,7 +58,7 @@ public: * @param state_count The number of states of the model. * @param ap_count The number of atomic propositions. */ - AtomicPropositionsLabeling(const uint_fast32_t state_count, const uint_fast32_t ap_count) + AtomicPropositionsLabeling(const uint_fast32_t state_count, const uint_fast32_t ap_count) : state_count(state_count), ap_count(ap_count), aps_current(0) { this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count]; for (uint_fast32_t i = 0; i < ap_count; ++i) { @@ -78,8 +78,7 @@ public: name_to_labeling_map(atomic_propositions_labeling.name_to_labeling_map) { this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count]; for (uint_fast32_t i = 0; i < ap_count; ++i) { - this->single_labelings[i] = new SingleAtomicPropositionLabeling( - *atomic_propositions_labeling.single_labelings[i]); + this->single_labelings[i] = new SingleAtomicPropositionLabeling(*atomic_propositions_labeling.single_labelings[i]); } } @@ -89,7 +88,6 @@ public: */ virtual ~AtomicPropositionsLabeling() { // delete all the single atomic proposition labelings in the map - MAP::iterator it; for (uint_fast32_t i = 0; i < ap_count; ++i) { delete this->single_labelings[i]; this->single_labelings[i] = NULL; diff --git a/src/models/backward_transitions.h b/src/models/backward_transitions.h index a99f0ae3e..2f6d3d49a 100644 --- a/src/models/backward_transitions.h +++ b/src/models/backward_transitions.h @@ -35,43 +35,47 @@ public: * @param transition_matrix The (0-based) matrix representing the transition * relation. */ - BackwardTransitions(mrmc::sparse::StaticSparseMatrix* transitionMatrix) - : numberOfStates(transitionMatrix->getRowCount()), - numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { - this->state_indices_list = new uint_fast64_t[numberOfStates + 1]; + BackwardTransitions(mrmc::sparse::StaticSparseMatrix* transitionMatrix) { + numberOfNonZeroTransitions = transitionMatrix->getNonZeroEntryCount(); this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions]; + + numberOfStates = transitionMatrix->getRowCount(); + this->state_indices_list = new uint_fast64_t[numberOfStates + 1]; // First, we need to count how many backward transitions each state has. // NOTE: We disregard the diagonal here, as we only consider "true" // predecessors. - for (uint_fast64_t i = 0; i <= numberOfStates; i++) { + for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { this->state_indices_list[*rowIt + 1]++; } } // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i <= numberOfStates; i++) { + for (uint_fast64_t i = 1; i < numberOfStates; i++) { this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[i]; } // Put a sentinel element at the end of the indices list. This way, // for each state i the range of indices can be read off between // state_indices_list[i] and state_indices_list[i + 1]. - this->state_indices_list[numberOfStates + 1] = numberOfNonZeroTransitions; + this->state_indices_list[numberOfStates] = numberOfNonZeroTransitions; // Create an array that stores the next index for each state. Initially // this corresponds to the previously computed accumulated offsets. - uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates + 1]; - memcpy(next_state_index_list, state_indices_list, (numberOfStates + 1) * sizeof(uint_fast64_t)); + uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates]; + memcpy(next_state_index_list, state_indices_list, numberOfStates * sizeof(uint_fast64_t)); // Now we are ready to actually fill in the list of predecessors for // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i <= numberOfStates; i++) { + for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) { this->predecessor_list[next_state_index_list[*rowIt]++] = i; } } + + // Now we can dispose of the auxiliary array. + delete[] next_state_index_list; } //! Destructor @@ -79,10 +83,10 @@ public: * Destructor. Frees the internal storage. */ ~BackwardTransitions() { - if (this->predecessor_list != NULL) { + if (this->predecessor_list != nullptr) { delete[] this->predecessor_list; } - if (this->state_indices_list != NULL) { + if (this->state_indices_list != nullptr) { delete[] this->state_indices_list; } } diff --git a/src/models/dtmc.h b/src/models/dtmc.h index afe4b3fd2..c01e341b1 100644 --- a/src/models/dtmc.h +++ b/src/models/dtmc.h @@ -55,6 +55,20 @@ public: pantheios::log_DEBUG("Copy constructor of DTMC invoked."); } + //! Destructor + /*! + * Destructor. Frees the matrix and labeling associated with this DTMC. + * + */ + ~Dtmc() { + if (this->probability_matrix != nullptr) { + delete this->probability_matrix; + } + if (this->state_labeling != nullptr) { + delete this->state_labeling; + } + } + /*! * Returns the state space size of the DTMC. * @return The size of the state space of the DTMC. diff --git a/src/mrmc-cpp.cpp b/src/mrmc-cpp.cpp index 2de514550..2dbee8c29 100644 --- a/src/mrmc-cpp.cpp +++ b/src/mrmc-cpp.cpp @@ -42,11 +42,12 @@ int main(const int argc, const char* argv[]) { try { - s = new mrmc::settings::Settings(argc, argv, NULL); + s = new mrmc::settings::Settings(argc, argv, nullptr); } catch (mrmc::exceptions::InvalidSettings) { std::cout << "Could not recover from settings error, terminating." << std::endl; + delete s; return 1; } @@ -65,7 +66,9 @@ int main(const int argc, const char* argv[]) { mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), s->getString("labfile").c_str()); mrmc::models::Dtmc dtmc(probMatrix, labeling); - + if (s != nullptr) { + delete s; + } return 0; } diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index 2a3742afe..35210d5a6 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -25,9 +25,12 @@ # define STRTOK_FUNC strtok_r #endif +// Only disable the warning if we are not using GCC, because +// GCC does not know this pragma and raises a warning +#ifndef __GNUG__ // Disable C4996 - This function or variable may be unsafe. #pragma warning(disable:4996) - +#endif namespace mrmc { @@ -150,7 +153,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c while (fgets(s, BUFFER_SIZE, P)) { char * token = NULL; - uint_fast32_t node = 0; + unsigned int node = 0; /* First token has to be a number identifying the node, * hence it is treated differently from the other tokens. */ @@ -167,7 +170,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c if (token == NULL) { break; } - result->addAtomicPropositionToState(token, node); + result->addAtomicPropositionToState(token, static_cast(node)); } while (token != NULL); } diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp index 5d652758b..ca4a59cc5 100644 --- a/src/parser/read_tra_file.cpp +++ b/src/parser/read_tra_file.cpp @@ -26,8 +26,12 @@ namespace mrmc { namespace parser{ +// Only disable the warning if we are not using GCC, because +// GCC does not know this pragma and raises a warning +#ifndef __GNUG__ // Disable C4996 - This function or variable may be unsafe. #pragma warning(disable:4996) +#endif /*! * This method does the first pass through the .tra file and computes @@ -46,7 +50,7 @@ static uint_fast32_t make_first_pass(FILE* p) { throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)"); } char s[BUFFER_SIZE]; //String buffer - uint_fast32_t rows=0, non_zero=0; + int rows=0, non_zero=0; //Reading No. of states if (fgets(s, BUFFER_SIZE, p) != NULL) { @@ -69,7 +73,7 @@ static uint_fast32_t make_first_pass(FILE* p) { //And increase number of transitions while (NULL != fgets( s, BUFFER_SIZE, p )) { - uint_fast32_t row=0, col=0; + int row=0, col=0; double val=0.0; if (sscanf( s, "%d%d%lf", &row, &col, &val ) != 3) { (void)fclose(p); @@ -80,7 +84,7 @@ static uint_fast32_t make_first_pass(FILE* p) { --non_zero; } } - return non_zero; + return static_cast(non_zero); } @@ -95,7 +99,8 @@ static uint_fast32_t make_first_pass(FILE* p) { sparse::StaticSparseMatrix * read_tra_file(const char * filename) { FILE *p = NULL; char s[BUFFER_SIZE]; - uint_fast32_t rows, non_zero; + uint_fast64_t non_zero = 0; + int rows = 0; sparse::StaticSparseMatrix *sp = NULL; p = fopen(filename, "r"); @@ -121,7 +126,7 @@ sparse::StaticSparseMatrix * read_tra_file(const char * filename) { * Note that the result is not used in this function as make_first_pass() * computes the relevant number (non_zero) */ - uint_fast32_t nnz=0; + int nnz = 0; if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) { (void)fclose(p); throw mrmc::exceptions::wrong_file_format(); @@ -135,7 +140,7 @@ sparse::StaticSparseMatrix * read_tra_file(const char * filename) { * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal * non-zero elements has to be specified (which is non_zero, computed by make_first_pass) */ - sp = new sparse::StaticSparseMatrix(rows + 1); + sp = new sparse::StaticSparseMatrix(static_cast(rows) + 1); if ( NULL == sp ) { throw std::bad_alloc(); return NULL; @@ -144,7 +149,7 @@ sparse::StaticSparseMatrix * read_tra_file(const char * filename) { //Reading transitions (one per line) and saving the results in the matrix while (NULL != fgets(s, BUFFER_SIZE, p )) { - uint_fast32_t row=0, col=0; + int row=0, col=0; double val = 0.0; if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) { (void)fclose(p); @@ -158,7 +163,7 @@ sparse::StaticSparseMatrix * read_tra_file(const char * filename) { " to position ", pantheios::integer(row), " x ", pantheios::integer(col)); - sp->addNextValue(row,col,val); + sp->addNextValue(static_cast(row),static_cast(col),static_cast(val)); } (void)fclose(p); diff --git a/src/reward/reward_model.h b/src/reward/reward_model.h index 52b2039b0..45a4a77d6 100644 --- a/src/reward/reward_model.h +++ b/src/reward/reward_model.h @@ -27,7 +27,7 @@ class RewardModel { typedef const DataClass& crDataClass; public: - RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : null_value(null_value), state_count(state_count) { + RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : state_count(state_count), null_value(null_value) { this->reward_vector = new VectorImpl>(this->state_count); // init everything to zero diff --git a/src/sparse/static_sparse_matrix.h b/src/sparse/static_sparse_matrix.h index b778fd352..621c1a8a1 100644 --- a/src/sparse/static_sparse_matrix.h +++ b/src/sparse/static_sparse_matrix.h @@ -47,7 +47,7 @@ public: * @see hasError() */ enum MatrixStatus { - Error = -1, UnInitialized = 0, Initialized = 1, ReadReady = 2, + Error = -1, UnInitialized = 0, Initialized = 1, ReadReady = 2 }; //! Constructor @@ -56,11 +56,7 @@ public: * @param rows The number of rows of the matrix */ StaticSparseMatrix(uint_fast64_t rows) - : internalStatus(MatrixStatus::UnInitialized), - currentSize(0), lastRow(0), valueStorage(nullptr), - diagonalStorage(nullptr), columnIndications(nullptr), - rowIndications(nullptr), rowCount(rows), nonZeroEntryCount(0) { } - + : rowCount(rows), nonZeroEntryCount(0), valueStorage(nullptr), diagonalStorage(nullptr), columnIndications(nullptr), rowIndications(nullptr), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { } //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given sparse matrix. @@ -322,7 +318,7 @@ public: // Fill in the missing entries in the row_indications array. // (Can happen because of empty rows at the end.) if (lastRow != rowCount) { - for (uint_fast64_t i = lastRow + 1; i <= rowCount; ++i) { + for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { rowIndications[i] = currentSize; } } @@ -331,7 +327,7 @@ public: // array. This eases iteration work, as now the indices of row i // are always between row_indications[i] and row_indications[i + 1], // also for the first and last row. - rowIndications[rowCount + 1] = nonZeroEntryCount; + rowIndications[rowCount] = nonZeroEntryCount; setState(MatrixStatus::ReadReady); }