From a61ea32aea292c06b75c930f323346537976c630 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 30 Apr 2020 16:41:39 +0200
Subject: [PATCH] Fixed some GCC warnings

---
 .../results/RegionRefinementCheckResult.cpp            | 10 ++++++++--
 src/storm-parsers/parser/DirectEncodingParser.cpp      |  2 --
 src/storm/logic/CumulativeRewardFormula.cpp            |  3 ---
 src/storm/logic/InstantaneousRewardFormula.cpp         |  2 +-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp
index 320dda2e8..7c2a5e18c 100644
--- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp
+++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp
@@ -48,7 +48,10 @@ namespace storm {
                 
                 out << "Region refinement Check result (visualization):" << std::endl;
                 out << " \t x-axis: " << x << "  \t y-axis: " << y << "  \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl;
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) {
+                    out << "#";
+                }
+                out << std::endl;
                 
                 CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber<CoefficientType>(sizeX);
                 CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber<CoefficientType>(sizeY);
@@ -94,7 +97,10 @@ namespace storm {
                     }
                     out << "#" << std::endl;
                 }
-                for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl;
+                for (uint_fast64_t i = 0; i < sizeX+2; ++i) {
+                    out << "#";
+                }
+                out << std::endl;
             } else {
                 STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters.");
             }
diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp
index 683a87d77..1dd6322d9 100644
--- a/src/storm-parsers/parser/DirectEncodingParser.cpp
+++ b/src/storm-parsers/parser/DirectEncodingParser.cpp
@@ -164,7 +164,6 @@ namespace storm {
             // Iterate over all lines
             std::string line;
             size_t row = 0;
-            size_t firstRowOfState = 0;
             size_t state = 0;
             bool firstState = true;
             bool firstActionForState = true;
@@ -197,7 +196,6 @@ namespace storm {
                         STORM_LOG_TRACE("new Row Group starts at " << row << ".");
                         builder.newRowGroup(row);
                     }
-                    firstRowOfState = row;
 
                     if (continuousTime) {
                         // Parse exit rate for CTMC or MA
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index 7abcdc7e4..33633b319 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/src/storm/logic/CumulativeRewardFormula.cpp
@@ -99,7 +99,6 @@ namespace storm {
         double CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             double value = bounds.at(i).getBound().evaluateAsDouble();
-            STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
@@ -107,7 +106,6 @@ namespace storm {
         storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational();
-            STORM_LOG_THROW(value >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
@@ -115,7 +113,6 @@ namespace storm {
         uint64_t CumulativeRewardFormula::getBound(unsigned i) const {
             checkNoVariablesInBound(bounds.at(i).getBound());
             uint64_t value = bounds.at(i).getBound().evaluateAsInt();
-            STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
         
diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp
index 37bdee1c9..1ed2c1f66 100644
--- a/src/storm/logic/InstantaneousRewardFormula.cpp
+++ b/src/storm/logic/InstantaneousRewardFormula.cpp
@@ -55,7 +55,7 @@ namespace storm {
         template <>
         uint64_t InstantaneousRewardFormula::getBound() const {
             checkNoVariablesInBound(bound);
-            uint64_t value = bound.evaluateAsInt();
+            int64_t value = bound.evaluateAsInt();
             STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }