From 2801f0f041fe053b5cdbedd6064bdebc8d5c5352 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Wed, 20 Dec 2017 18:13:57 +0000
Subject: [PATCH] Avoid crashing when --dependence-graph is used by correcting
 namespace scoping.

The namespace has to last as long as the domain does, otherwise the
dependence graph will wind up with a reference to a dead, stack allocated
object, leading to some exciting crashes.
---
 src/goto-analyzer/goto_analyzer_parse_options.cpp | 11 +++++++----
 src/goto-analyzer/goto_analyzer_parse_options.h   |  2 +-
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index f8d1fc1d331..414ff3d854c 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -311,7 +311,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 /// For the task, build the appropriate kind of analyzer
 /// Ideally this should be a pure function of options.
 /// However at the moment some domains require the goto_model
-ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options)
+ai_baset *goto_analyzer_parse_optionst::build_analyzer(
+  const optionst &options,
+  const namespacet &ns)
 {
   ai_baset *domain = nullptr;
 
@@ -324,7 +326,7 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options)
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      domain=new dependence_grapht(namespacet(goto_model.symbol_table));
+      domain=new dependence_grapht(ns);
     }
     else if(options.get_bool_option("intervals"))
     {
@@ -348,7 +350,7 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options)
     }
     else if(options.get_bool_option("dependence-graph"))
     {
-      domain=new dependence_grapht(namespacet(goto_model.symbol_table));
+      domain=new dependence_grapht(ns);
     }
     else if(options.get_bool_option("intervals"))
     {
@@ -611,7 +613,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     // Build analyzer
     status() << "Selecting abstract domain" << eom;
-    std::unique_ptr<ai_baset> analyzer(build_analyzer(options));
+    namespacet ns(goto_model.symbol_table);  // Must live as long as the domain.
+    std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
 
     if(analyzer == nullptr)
     {
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index a5d5d0f4c9c..98181e385d7 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -168,7 +168,7 @@ class goto_analyzer_parse_optionst:
 
   virtual int perform_analysis(const optionst &options);
 
-  ai_baset *build_analyzer(const optionst &options);
+  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
 
   void eval_verbosity();