From: Tim King <taking@cs.nyu.edu>
Date: Tue, 26 Sep 2017 20:02:32 +0000 (-0700)
Subject: Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and GetModel... 
X-Git-Tag: cvc5-1.0.0~5610
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f9f1fee128c86f3a1210134f1f22a0343793d4a;p=cvc5.git

Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and GetModelCommand to nullptr. (#1142)
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 86fb5cdde..a4f0c6320 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1113,8 +1113,8 @@ std::string GetAssignmentCommand::getCommandName() const throw() {
 
 /* class GetModelCommand */
 
-GetModelCommand::GetModelCommand() throw() {
-}
+GetModelCommand::GetModelCommand() throw()
+    : d_result(nullptr), d_smtEngine(nullptr) {}
 
 void GetModelCommand::invoke(SmtEngine* smtEngine) {
   try {
@@ -1164,8 +1164,8 @@ std::string GetModelCommand::getCommandName() const throw() {
 
 /* class GetProofCommand */
 
-GetProofCommand::GetProofCommand() throw() {
-}
+GetProofCommand::GetProofCommand() throw()
+    : d_result(nullptr), d_smtEngine(nullptr) {}
 
 void GetProofCommand::invoke(SmtEngine* smtEngine) {
   try {
diff --git a/src/smt/command.h b/src/smt/command.h
index 1db414cde..0e07583b2 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -602,35 +602,39 @@ public:
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetModelCommand : public Command {
-protected:
-  Model* d_result;
-  SmtEngine* d_smtEngine;
-public:
+ public:
   GetModelCommand() throw();
   ~GetModelCommand() throw() {}
   void invoke(SmtEngine* smtEngine);
   // Model is private to the library -- for now
-  //Model* getResult() const throw();
+  // Model* getResult() const throw();
   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
-  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
-};/* class GetModelCommand */
 
-class CVC4_PUBLIC GetProofCommand : public Command {
-protected:
-  Proof* d_result;
+ protected:
+  Model* d_result;
   SmtEngine* d_smtEngine;
-public:
+}; /* class GetModelCommand */
+
+class CVC4_PUBLIC GetProofCommand : public Command {
+ public:
   GetProofCommand() throw();
   ~GetProofCommand() throw() {}
   void invoke(SmtEngine* smtEngine);
   Proof* getResult() const throw();
   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
-  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
-};/* class GetProofCommand */
+
+ protected:
+  Proof* d_result;
+  SmtEngine* d_smtEngine;
+}; /* class GetProofCommand */
 
 class CVC4_PUBLIC GetInstantiationsCommand : public Command {
  public: