From: Tim King <taking@google.com>
Date: Fri, 23 Oct 2015 22:11:57 +0000 (-0700)
Subject: Switching Options::current() to return a pointer. This helps avoid undefined behavior... 
X-Git-Tag: cvc5-1.0.0~6193
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9b7de773cdc53044e5cf4a55d4893d2be476b60;p=cvc5.git

Switching Options::current() to return a pointer. This helps avoid undefined behavior due to dereferencing a null pointer in the future.
---

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 03d7837ac..b4cea04d1 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -493,9 +493,9 @@ function handle_option {
 extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; } $internal CVC4_PUBLIC;"
       module_inlines="${module_inlines}
 #line $lineno \"$kf\"
-inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return (*Options::current())[*this]; }
 #line $lineno \"$kf\"
-inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current()->wasSetByUser(*this); }
 "
     else
       module_decls="${module_decls}
@@ -503,11 +503,11 @@ inline bool ${internal}__option_t::wasSetByUser() const { return Options::curren
 extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } $internal CVC4_PUBLIC;"
       module_inlines="${module_inlines}
 #line $lineno \"$kf\"
-inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return (*Options::current())[*this]; }
 #line $lineno \"$kf\"
-inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current()->wasSetByUser(*this); }
 #line $lineno \"$kf\"
-inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current().set(*this, v); }
+inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current()->set(*this, v); }
 "
       module_specializations="${module_specializations}
 #line $lineno \"$kf\"
@@ -783,7 +783,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links
+    Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -800,7 +800,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links
+    Options::current()->assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
diff --git a/src/options/options.h b/src/options/options.h
index 9656007f4..95c0fc331 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -66,8 +66,8 @@ public:
   }
 
   /** Get the current Options in effect */
-  static inline Options& current() {
-    return *s_current;
+  static inline Options* current() {
+    return s_current;
   }
 
   Options();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2784bb006..c863909e5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1738,7 +1738,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
     return SExpr(d_userLevels.size());
   } else if(key == "all-options") {
     // get the options, like all-statistics
-    return Options::current().getOptions();
+    return Options::current()->getOptions();
   } else {
     throw UnrecognizedOptionException();
   }