summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2017-09-26 13:02:32 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2017-09-26 13:02:32 -0700
commit0f9f1fee128c86f3a1210134f1f22a0343793d4a (patch)
treeb1da0e71c045b337bbf671662f1e7ab09f4d4ae2 /src/smt
parente76b70bfa6053b8de7868e595cbe6317ae0ef11c (diff)
Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and GetModelCommand to nullptr. (#1142)
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/command.cpp8
-rw-r--r--src/smt/command.h30
2 files changed, 21 insertions, 17 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback