Add virtual destructors to classes having virtual functions.

(Silences warnings from -Wdelete-non-virtual-dtor -Wnon-virtual-dtor)

src/storm-dft/builder/DftExplorationHeuristic.h

@@ -22,6 +22,8 @@ namespace storm {
 
             DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate);
 
+            virtual ~DFTExplorationHeuristic() = default;
+
             void setBounds(ValueType lowerBound, ValueType upperBound);
 
             virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0;

src/storm-pgcl/storage/pgcl/AbstractStatementVisitor.h

@@ -13,6 +13,8 @@ namespace storm {
          */
         class AbstractStatementVisitor {
         public:
+            virtual ~AbstractStatementVisitor() = default;
+
             // Those functions need to be implemented for every possible
             // statement instantiation.
             virtual void visit(class AssignmentStatement const&) = 0;

src/storm-pgcl/storage/ppg/ProgramAction.h

@@ -13,7 +13,9 @@ namespace storm {
             ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) {
                 
             }
-            
+
+            virtual ~ProgramAction() = default;
+
             ProgramActionIdentifier id() const {
                 return actId;
             }

src/storm/abstraction/MenuGameAbstractor.h

@@ -24,6 +24,8 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         class MenuGameAbstractor {
         public:
+            virtual ~MenuGameAbstractor() = default;
+
             /// Retrieves the abstraction.
             virtual MenuGame<DdType, ValueType> abstract() = 0;
 

src/storm/abstraction/QualitativeResult.h

@@ -13,6 +13,8 @@ namespace storm {
         template <storm::dd::DdType Type>
         class QualitativeResult {
         public:
+            virtual ~QualitativeResult() = default;
+
             virtual storm::dd::Bdd<Type> const& getStates() const = 0;
         };
         

src/storm/abstraction/QualitativeResultMinMax.h

@@ -10,6 +10,8 @@ namespace storm {
         
         class QualitativeResultMinMax {
         public:
+            virtual ~QualitativeResultMinMax() = default;
+
             virtual bool isSymbolic() const;
             
             template<storm::dd::DdType Type>

src/storm/abstraction/StateSet.h

@@ -10,6 +10,8 @@ namespace storm {
         
         class StateSet {
         public:
+            virtual ~StateSet() = default;
+
             virtual bool isSymbolic() const;
             
             template<storm::dd::DdType Type>

src/storm/counterexamples/Counterexample.h

@@ -7,6 +7,8 @@ namespace storm {
         
         class Counterexample {
         public:
+            virtual ~Counterexample() = default;
+
             virtual void writeToStream(std::ostream& out) const = 0;
         };
         

src/storm/logic/FormulaVisitor.h

@@ -10,6 +10,8 @@ namespace storm {
 
         class FormulaVisitor {
         public:
+            virtual ~FormulaVisitor() = default;
+
             virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;

src/storm/modelchecker/hints/ModelCheckerHint.h

@@ -15,7 +15,8 @@ namespace storm {
         class ModelCheckerHint {
         public:
             ModelCheckerHint() = default;
-            
+            virtual ~ModelCheckerHint() = default;
+
             // Returns true iff this hint does not contain any information.
             virtual bool isEmpty() const;
             

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h

@@ -24,7 +24,9 @@ namespace storm {
                 SparseMultiObjectivePreprocessorTask(std::shared_ptr<Objective<typename SparseModelType::ValueType>> const& objective) : objective(objective) {
                     // intentionally left empty
                 }
-                
+
+                virtual ~SparseMultiObjectivePreprocessorTask() = default;
+
                 virtual void perform(SparseModelType& preprocessedModel) const = 0;
                 
                 virtual bool requiresEndComponentAnalysis() const {

src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h

@@ -27,7 +27,9 @@ namespace storm {
                  * @param oneStepTargetProbabilities For each state the probability to go to a goal state in one step.
                  */
                 DsMpiDtmcUpperRewardBoundsComputer(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards, std::vector<ValueType> const& oneStepTargetProbabilities);
-                
+
+                virtual ~DsMpiDtmcUpperRewardBoundsComputer() = default;
+
                 /*!
                  * Computes upper bounds on the expected rewards.
                  */

src/storm/models/sparse/ItemLabeling.h

@@ -33,6 +33,7 @@ namespace storm {
                 ItemLabeling(ItemLabeling const& other) = default;
                 ItemLabeling& operator=(ItemLabeling const& other) = default;
 
+                virtual ~ItemLabeling() = default;
 
                 virtual bool isStateLabeling() const;
                 virtual bool isChoiceLabeling() const;

src/storm/models/sparse/StateAnnotation.h

@@ -9,6 +9,8 @@ namespace storm {
             
             class StateAnnotation {
             public:
+                virtual ~StateAnnotation() = default;
+
                 virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const = 0;
             };
             

src/storm/permissivesched/PermissiveSchedulerComputation.h

@@ -26,8 +26,9 @@ namespace storm {
             {
                 
             }
-            
-                    
+
+            virtual ~PermissiveSchedulerComputation() = default;
+
             virtual void calculatePermissiveScheduler(bool lowerBound, double boundary) = 0;
             
             void setPenalties(PermissiveSchedulerPenalties penalties) {

src/storm/settings/ArgumentBase.h

@@ -26,7 +26,9 @@ namespace storm {
 			ArgumentBase(std::string const& name, std::string const& description) : hasBeenSet(false), name(name), description(description) {
                 // Intentionally left empty.
             }
-            
+
+            virtual ~ArgumentBase() = default;
+
             /*!
              * Retrieves the type of the argument.
              *

src/storm/settings/ArgumentValidators.h

@@ -12,6 +12,8 @@ namespace storm {
         template <typename ValueType>
         class ArgumentValidator {
         public:
+            virtual ~ArgumentValidator() = default;
+
             /*!
              * Checks whether the argument passes the validation.
              */

src/storm/solver/GameSolver.h

@@ -167,6 +167,7 @@ namespace storm {
         class GameSolverFactory {
         public:
             GameSolverFactory();
+            virtual ~GameSolverFactory() = default;
 
             virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix) const;
             virtual std::unique_ptr<GameSolver<ValueType>> create(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix, storm::storage::SparseMatrix<ValueType>&& player2Matrix) const;

src/storm/solver/LinearEquationSolver.h

@@ -179,6 +179,8 @@ namespace storm {
         template<typename ValueType>
         class LinearEquationSolverFactory {
         public:
+            virtual ~LinearEquationSolverFactory() = default;
+
             /*!
              * Creates a new linear equation solver instance with the given matrix.
              *

src/storm/solver/LpSolver.h

@@ -36,6 +36,8 @@ namespace storm {
              */
             LpSolver(OptimizationDirection const& optDir);
 
+            virtual ~LpSolver() = default;
+
             /*!
              * Registers an upper- and lower-bounded continuous variable, i.e. a variable that may take all real values
              * within its bounds.

src/storm/solver/MinMaxLinearEquationSolver.h

@@ -207,6 +207,7 @@ namespace storm {
         class MinMaxLinearEquationSolverFactory {
         public:
             MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
+	    virtual ~MinMaxLinearEquationSolverFactory() = default;
             
             std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
             std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;

src/storm/solver/SmtSolver.h

@@ -36,7 +36,8 @@ namespace storm {
                  * @param manager The manager responsible for the variables whose value can be requested.
                  */
                 ModelReference(storm::expressions::ExpressionManager const& manager);
-                
+                virtual ~ModelReference() = default;
+
                 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const = 0;
 				virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const = 0;
                 virtual double getRationalValue(storm::expressions::Variable const& variable) const = 0;

src/storm/solver/SymbolicEquationSolver.h

@@ -13,6 +13,7 @@ namespace storm {
         public:
             SymbolicEquationSolver() = default;
             SymbolicEquationSolver(storm::dd::Bdd<DdType> const& allRows);
+            virtual ~SymbolicEquationSolver() = default;
 
             virtual void setLowerBounds(storm::dd::Add<DdType, ValueType> const& lowerBounds);
             virtual void setLowerBound(ValueType const& lowerBound);

src/storm/solver/SymbolicGameSolver.h

@@ -54,7 +54,9 @@ namespace storm {
              * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one.
              */
             SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
-            
+
+            virtual ~SymbolicGameSolver() = default;
+
             /*!
              * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon
              * construction time of the solver object.
@@ -133,6 +135,8 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicGameSolverFactory {
         public:
+            virtual ~SymbolicGameSolverFactory() = default;
+
             virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
         };
         

src/storm/solver/SymbolicLinearEquationSolver.h

@@ -33,7 +33,8 @@ namespace storm {
         class SymbolicLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
         public:
             SymbolicLinearEquationSolver();
-            
+            virtual ~SymbolicLinearEquationSolver() = default;
+
             /*!
              * Constructs a symbolic linear equation solver with the given meta variable sets and pairs.
              *
@@ -116,6 +117,8 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         class SymbolicLinearEquationSolverFactory {
         public:
+            virtual ~SymbolicLinearEquationSolverFactory() = default;
+
             std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;
             
             std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const;

src/storm/solver/SymbolicMinMaxLinearEquationSolver.h

@@ -62,7 +62,8 @@ namespace storm {
         class SymbolicMinMaxLinearEquationSolver : public SymbolicEquationSolver<DdType, ValueType> {
         public:
             SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings = SymbolicMinMaxLinearEquationSolverSettings<ValueType>());
-            
+            virtual ~SymbolicMinMaxLinearEquationSolver() = default;
+
             /*!
              * Constructs a symbolic min/max linear equation solver with the given meta variable sets and pairs.
              *
@@ -237,6 +238,8 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         class SymbolicMinMaxLinearEquationSolverFactory {
         public:
+            virtual ~SymbolicMinMaxLinearEquationSolverFactory() = default;
+
             virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) const = 0;
             
             /*!

src/storm/solver/TerminationCondition.h

@@ -10,6 +10,8 @@ namespace storm {
         template<typename ValueType>
         class TerminationCondition {
         public:
+            virtual ~TerminationCondition() = default;
+
             /*!
              * Retrieves whether the guarantee provided by the solver for the current result is sufficient to terminate.
              */

src/storm/solver/stateelimination/EliminatorBase.h

@@ -19,7 +19,8 @@ namespace storm {
                 typedef typename FlexibleRowType::iterator FlexibleRowIterator;
                 
                 EliminatorBase(storm::storage::FlexibleSparseMatrix<ValueType>& matrix, storm::storage::FlexibleSparseMatrix<ValueType>& transposedMatrix);
-                
+                virtual ~EliminatorBase() = default;
+
                 void eliminate(uint64_t row, uint64_t column, bool clearRow);
                 
                 // Provide virtual methods that can be customized by subclasses to govern side-effect of the elimination.

src/storm/solver/stateelimination/StatePriorityQueue.h

@@ -10,6 +10,8 @@ namespace storm {
          
             class StatePriorityQueue {
             public:
+                virtual ~StatePriorityQueue() = default;
+
                 virtual bool hasNext() const = 0;
                 virtual storm::storage::sparse::state_type pop() = 0;
                 virtual void update(storm::storage::sparse::state_type state);

src/storm/storage/bisimulation/BisimulationDecomposition.h

@@ -180,7 +180,9 @@ namespace storm {
              * @param options The options to use during for the decomposition.
              */
             BisimulationDecomposition(ModelType const& model, Options const& options);
-            
+
+            virtual ~BisimulationDecomposition() = default;
+
             /*!
              * Retrieves the quotient of the model under the computed bisimulation.
              *

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -255,6 +255,8 @@ namespace storm {
                     STORM_LOG_TRACE("Partition has " << partitionBdd.existsAbstract(model.getRowVariables()).getNonZeroCount() << " states in " << this->numberOfBlocks << " blocks.");
                 }
 
+                virtual ~InternalSparseQuotientExtractorBase() = default;
+
                 storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
                     return extractMatrixInternal(transitionMatrix);
                 }

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -67,7 +67,8 @@ namespace storm {
             InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType> const& other) = default;
             InternalAdd(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
             InternalAdd& operator=(InternalAdd<DdType::CUDD, ValueType>&& other) = default;
-            
+            virtual ~InternalAdd() = default;
+
             /*!
              * Retrieves whether the two DDs represent the same function.
              *

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -60,7 +60,8 @@ namespace storm {
             InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType> const& other) = default;
             InternalAdd(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
             InternalAdd& operator=(InternalAdd<DdType::Sylvan, ValueType>&& other) = default;
-            
+            virtual ~InternalAdd() = default;
+
             /*!
              * Retrieves whether the two DDs represent the same function.
              *
@@ -732,7 +733,7 @@ namespace storm {
             static MTBDD getLeaf(uint_fast64_t value);
 
             /*!
-             * Retrieves the sylvan representation of the given storm::RatíonalNumber.
+             * Retrieves the sylvan representation of the given storm::Rat�onalNumber.
              *
              * @return The sylvan node for the given value.
              */

src/storm/storage/expressions/CompiledExpression.h

@@ -7,6 +7,7 @@ namespace storm {
         
         class CompiledExpression {
         public:
+            virtual ~CompiledExpression() = default;
             
             virtual bool isExprtkCompiledExpression() const;
             ExprtkCompiledExpression& asExprtkCompiledExpression();

src/storm/storage/expressions/ExpressionEvaluatorBase.h

@@ -9,7 +9,8 @@ namespace storm {
         class ExpressionEvaluatorBase {
         public:
             ExpressionEvaluatorBase(storm::expressions::ExpressionManager const& manager);
-            
+            virtual ~ExpressionEvaluatorBase() = default;
+
             virtual bool asBool(Expression const& expression) const = 0;
             virtual int_fast64_t asInt(Expression const& expression) const = 0;
             virtual RationalReturnType asRational(Expression const& expression) const = 0;

src/storm/storage/expressions/ExpressionVisitor.h

@@ -20,6 +20,8 @@ namespace storm {
         
         class ExpressionVisitor {
         public:
+            virtual ~ExpressionVisitor() = default;
+
             virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) = 0;
             virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) = 0;
             virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) = 0;

src/storm/storage/expressions/Type.h

@@ -15,6 +15,7 @@ namespace storm {
         class BaseType {
         public:
             BaseType();
+            virtual ~BaseType() = default;
             
             /*!
              * Retrieves the mask that is associated with this type.

src/storm/storage/jani/Composition.h

@@ -9,6 +9,8 @@ namespace storm {
         
         class Composition {
         public:
+            virtual ~Composition() = default;
+
             virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0;
             
             virtual void write(std::ostream& stream) const = 0;

src/storm/storage/jani/CompositionVisitor.h

@@ -11,6 +11,8 @@ namespace storm {
         
         class CompositionVisitor {
         public:
+            virtual ~CompositionVisitor() = default;
+
             virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) = 0;
             virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) = 0;
         };

src/storm/storage/prism/Composition.h

@@ -10,6 +10,7 @@ namespace storm {
         class Composition {
         public:
             Composition() = default;
+            virtual ~Composition() = default;
             
             friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
             

src/storm/storage/prism/CompositionVisitor.h

@@ -15,6 +15,8 @@ namespace storm {
         
         class CompositionVisitor {
         public:
+            virtual ~CompositionVisitor() = default;
+
             virtual boost::any visit(ModuleComposition const& composition, boost::any const& data) = 0;
             virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) = 0;
             virtual boost::any visit(HidingComposition const& composition, boost::any const& data) = 0;

src/storm/storage/prism/Variable.h

@@ -17,7 +17,8 @@ namespace storm {
             Variable& operator=(Variable const& otherVariable)= default;
             Variable(Variable&& otherVariable) = default;
             Variable& operator=(Variable&& otherVariable) = default;
-
+            virtual ~Variable() = default;
+            
             /*!
              * Retrieves the name of the variable.
              *

src/storm/utility/solver.h

@@ -59,6 +59,8 @@ namespace storm {
             template<typename ValueType>
             class LpSolverFactory {
             public:
+                virtual ~LpSolverFactory() = default;
+
                 /*!
                  * Creates a new linear equation solver instance with the given name.
                  *
@@ -98,6 +100,8 @@ namespace storm {
 
             class SmtSolverFactory {
             public:
+                virtual ~SmtSolverFactory() = default;
+
                 /*!
                  * Creates a new SMT solver instance.
                  *