From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 13 Oct 2015 23:59:22 +0000 (-0400)
Subject: remove options infrastructure code which depended on undefined behavior
X-Git-Tag: cvc5-1.0.0~6209^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21ecec6988c6f4b145985ea0ac506380fca6c3d2;p=cvc5.git

remove options infrastructure code which depended on undefined behavior

appears to be source of crashes on mac
---

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index d769ed109..ae0fad897 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -649,7 +649,7 @@ public:
     long& l = out.iword(s_iosIndex);
     if(l == 0) {
       // set the default print depth on this ostream
-      if(&Options::current() != NULL) {
+      if(not Options::isCurrentNull()) {
         l = options::defaultExprDepth();
       }
       if(l == 0) {
@@ -801,7 +801,7 @@ public:
     if(l == 0) {
       // set the default dag setting on this ostream
       // (offset by one to detect whether default has been set yet)
-      if(&Options::current() != NULL) {
+      if(not Options::isCurrentNull()) {
         l = options::defaultDagThresh() + 1;
       }
       if(l == 0) {
@@ -884,7 +884,7 @@ public:
     if(l == 0) {
       // set the default language on this ostream
       // (offset by one to detect whether default has been set yet)
-      if(&Options::current() != NULL) {
+      if(not Options::isCurrentNull()) {
         l = options::outputLanguage() + 1;
       }
       if(l <= 0 || l > language::output::LANG_MAX) {
diff --git a/src/options/options.h b/src/options/options.h
index 092fbe507..9656007f4 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -60,6 +60,11 @@ class CVC4_PUBLIC Options {
 
 public:
 
+  /** Return true if current Options are null */
+  static inline bool isCurrentNull() {
+    return s_current == NULL;
+  }
+
   /** Get the current Options in effect */
   static inline Options& current() {
     return *s_current;
diff --git a/src/printer/printer.h b/src/printer/printer.h
index fcc0df93c..44e5ac9f4 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -62,7 +62,7 @@ public:
       //
       // Options can be null in certain circumstances (e.g., when printing
       // the singleton "null" expr.  So we guard against segfault
-      if(&Options::current() != NULL) {
+      if(not Options::isCurrentNull()) {
         if(options::outputLanguage.wasSetByUser()) {
           lang = options::outputLanguage();
         }