diff --git a/CMakeLists.txt b/CMakeLists.txt index a1b8c29b3..c0179e39d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -114,8 +114,10 @@ if(CMAKE_COMPILER_IS_GNUCC) set(STORM_COMPILED_BY "GCC") # Set standard flags for GCC set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") + set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops") add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -Wno-deprecated-declarations") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) @@ -123,7 +125,7 @@ if(CMAKE_COMPILER_IS_GNUCC) endif(STORM_USE_POPCNT) # Set the no-strict-aliasing target for GCC - set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ") + set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing") elseif(MSVC) set(STORM_COMPILED_BY "MSVC") # required for GMM to compile, ugly error directive in their code @@ -146,7 +148,7 @@ else(CLANG) # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. set (CLANG ON) # Set standard flags for clang - set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") + set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") @@ -162,6 +164,7 @@ else(CLANG) add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024") + set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic") # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt index 4d08513de..c9f821a21 100644 --- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt +++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt @@ -20,9 +20,13 @@ include_directories("${PROJECT_SOURCE_DIR}/src/nanotrav") include_directories("${PROJECT_SOURCE_DIR}/src/st") include_directories("${PROJECT_SOURCE_DIR}/src/util") -if(MSVC) +if(CMAKE_COMPILER_IS_GNUCC) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function") +elseif(MSVC) # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) +else(CLANG) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-function") endif() # Since we do not target Alphas, this symbol is always set diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc index 3262108aa..b8f7d3983 100644 --- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc +++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc @@ -2815,7 +2815,7 @@ Cudd::Walsh( size_t n = x.size(); DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; - for (int i = 0; i < n; i++) { + for (size_t i = 0; i < n; i++) { X[i] = x[i].getNode(); Y[i] = y[i].getNode(); } @@ -3612,7 +3612,7 @@ ADD::SwapVariables( DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; - for (int i = 0; i < n; i++) { + for (size_t i = 0; i < n; i++) { X[i] = x[i].node; Y[i] = y[i].node; } @@ -3646,7 +3646,7 @@ BDD::SwapVariables( DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; DdNode **Y = new DdNode *[n]; - for (int i = 0; i < n; i++) { + for (size_t i = 0; i < n; i++) { X[i] = x[i].node; Y[i] = y[i].node; } @@ -3666,7 +3666,7 @@ BDD::AdjPermuteX( size_t n = x.size(); DdManager *mgr = p->manager; DdNode **X = new DdNode *[n]; - for (int i = 0; i < n; i++) { + for (size_t i = 0; i < n; i++) { X[i] = x[i].node; } DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, static_cast(n)); diff --git a/resources/3rdparty/glpk-4.53/CMakeLists.txt b/resources/3rdparty/glpk-4.53/CMakeLists.txt index b09ec9e1c..24ee34121 100644 --- a/resources/3rdparty/glpk-4.53/CMakeLists.txt +++ b/resources/3rdparty/glpk-4.53/CMakeLists.txt @@ -53,7 +53,7 @@ message(STATUS "GLPK - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") if(CMAKE_COMPILER_IS_GNUCC) message(STATUS "GLPK - Using Compiler Configuration: GCC") # Set standard flags for GCC - set(CMAKE_C_FLAGS "${CMAKE_CXX_FLAGS} -Wno-return-type") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-return-type -Wno-parentheses -Wno-unused-variable -Wno-unused-but-set-variable -Wno-unused-value -Wno-unused-function -Wno-address -Wno-unused-label") add_definitions(-DHAVE_CONFIG_H=1) elseif(MSVC) message(STATUS "GLPK - Using Compiler Configuration: MSVC") diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 518d21972..adf65d728 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -343,7 +343,6 @@ namespace storm { // Get some data members for convenience. typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - ValueType one = storm::utility::one(); ValueType zero = storm::utility::zero(); //first calculate LRA for the Maximal End Components. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index e4087ad52..498370e02 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -692,23 +692,10 @@ namespace storm { return maximalDepth; } - namespace { - static int chunkCounter = 0; - static int counter = 0; - } - template void SparseDtmcEliminationModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) { auto eliminationStart = std::chrono::high_resolution_clock::now(); - ++counter; - STORM_LOG_TRACE("Eliminating state " << state << "."); - if (counter > matrix.getNumberOfRows() / 10) { - ++chunkCounter; - STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); - counter = 0; - } - bool hasSelfLoop = false; ValueType loopProbability = storm::utility::zero(); @@ -752,7 +739,6 @@ namespace storm { // Now connect the predecessors of the state being eliminated with its successors. typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); - std::size_t numberOfPredecessors = currentStatePredecessors.size(); std::size_t predecessorForwardTransitionCount = 0; // In case we have a constrained elimination, we need to keep track of the new predecessors. diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 23764fd61..065ad4327 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -69,7 +69,7 @@ namespace storm { #ifdef WINDOWS sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1); #else - int ret = sscanf(filehintBuffer, formatString.c_str(), hint); + sscanf(filehintBuffer, formatString.c_str(), hint); #endif for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);