Switching Options::current() to return a pointer. This helps avoid undefined behavior...

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 03d7837ac46cd6735285f2cced86d20699e6b94c..b4cea04d13801c361c843c359fba12477a2c33fb 100755 (executable)
--- 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 9656007f4a07eaf150f5b6a27ad7d300202c2646..95c0fc331bfa067c06e77e8cc40ebbde03c03b12 100644 (file)
--- 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 2784bb0060368960eed74218cf689a74da759dfe..c863909e583b53bec4933f3852e750ae1e629b0a 100644 (file)
--- 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();
   }