From 9301cb65de3fcbc24e29db534338d606961159d3 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Thu, 8 Sep 2016 07:58:26 +0100
Subject: [PATCH 01/32] Add XML and JSON output to the base of both domains and
 analysis.

---
 src/analyses/ai.cpp | 147 ++++++++++++++++++++++++++++++++++++++++++++
 src/analyses/ai.h   |  88 ++++++++++++++++++++++++++
 2 files changed, 235 insertions(+)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index dd976334aae..5fa5974ea2e 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -85,6 +85,153 @@ void ai_baset::output(
 
 /*******************************************************************\
 
+Function: ai_baset::output_json
+
+  Inputs: The namespace and goto_functions
+
+ Outputs: The JSON object
+
+ Purpose: Output the domains for the whole program as JSON
+
+\*******************************************************************/
+
+jsont ai_baset::output_json(
+  const namespacet &ns,
+  const goto_functionst &goto_functions) const
+{
+  json_objectt result;
+  
+  for(goto_functionst::function_mapt::const_iterator
+      f_it=goto_functions.function_map.begin();
+      f_it!=goto_functions.function_map.end();
+      f_it++)
+  {
+    if(f_it->second.body_available())
+    {
+      result[as_string(f_it->first)] = output_json(ns, f_it->second.body, f_it->first);
+    } else {
+      result[as_string(f_it->first)] = json_stringt("no body");
+    }
+  }
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: ai_baset::output_json
+
+  Inputs: The namespace, goto_program and it's identifier
+
+ Outputs: The JSON object
+
+ Purpose: Output the domains for a single function as JSON
+
+\*******************************************************************/
+
+jsont ai_baset::output_json(
+  const namespacet &ns,
+  const goto_programt &goto_program,
+  const irep_idt &identifier) const
+{
+  json_arrayt contents;
+  
+  forall_goto_program_instructions(i_it, goto_program)
+  {
+    json_objectt location;
+    location["location_number"] = json_numbert(std::to_string(i_it->location_number));
+    location["source_location"] = json_stringt(i_it->source_location.as_string());
+    location["domain"] = find_state(i_it).output_json(*this, ns);
+
+    // Ideally we need output_instruction_json
+    std::ostringstream out;
+    goto_program.output_instruction(ns, identifier, out, i_it);
+    location["instruction"] = json_stringt(out.str());
+
+    contents.push_back(location);
+  }
+
+  return contents;
+}
+
+/*******************************************************************\
+
+Function: ai_baset::output_xml
+
+  Inputs: The namespace and goto_functions
+
+ Outputs: The XML object
+
+ Purpose: Output the domains for the whole program as XML
+
+\*******************************************************************/
+
+xmlt ai_baset::output_xml(
+  const namespacet &ns,
+  const goto_functionst &goto_functions) const
+{
+  xmlt program("program");
+  
+  for(goto_functionst::function_mapt::const_iterator
+      f_it=goto_functions.function_map.begin();
+      f_it!=goto_functions.function_map.end();
+      f_it++)
+  {
+    xmlt function("function");
+    function.set_attribute("name", as_string(f_it->first));
+    function.set_attribute("body_available", f_it->second.body_available());
+    
+    if(f_it->second.body_available())
+    {
+      function.new_element(output_xml(ns, f_it->second.body, f_it->first));
+    }
+
+    program.new_element(function);
+  }
+
+  return program;
+}
+
+/*******************************************************************\
+
+Function: ai_baset::output_xml
+
+  Inputs: The namespace, goto_program and it's identifier
+
+ Outputs: The XML object
+
+ Purpose: Output the domains for a single function as XML
+
+\*******************************************************************/
+
+xmlt ai_baset::output_xml(
+  const namespacet &ns,
+  const goto_programt &goto_program,
+  const irep_idt &identifier) const
+{
+  xmlt function_body;
+  
+  forall_goto_program_instructions(i_it, goto_program)
+  {
+    xmlt location;
+    location.set_attribute("location_number", std::to_string(i_it->location_number));
+    location.set_attribute("source_location", i_it->source_location.as_string());
+
+    location.new_element(find_state(i_it).output_xml(*this, ns));
+
+    // Ideally we need output_instruction_xml
+    std::ostringstream out;
+    goto_program.output_instruction(ns, identifier, out, i_it);
+    location.set_attribute("instruction", out.str());
+
+    function_body.new_element(location);
+  }
+
+  return function_body;
+}
+
+/*******************************************************************\
+
 Function: ai_baset::entry_state
 
   Inputs:
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 5265830c1e0..3d47c541edd 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -11,6 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <map>
 #include <iosfwd>
+#include <sstream>
+
+#include <util/json.h>
+#include <util/xml.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -53,6 +57,27 @@ class ai_domain_baset
   {
   }
   
+  virtual jsont output_json(
+    const ai_baset &ai,
+    const namespacet &ns) const
+  {
+    std::ostringstream out;
+    output(out, ai, ns);
+    json_stringt json(out.str());
+    return json;
+  }
+  
+  virtual xmlt output_xml(
+    const ai_baset &ai,
+    const namespacet &ns) const
+  {
+    std::ostringstream out;
+    output(out, ai, ns);
+    xmlt xml("domain");
+    xml.data = out.str();
+    return xml;
+  }
+   
   // no states
   virtual void make_bottom()
   {
@@ -162,6 +187,58 @@ class ai_baset
     output(ns, goto_function.body, "", out);
   }
 
+  
+  virtual jsont output_json(
+    const namespacet &ns,
+    const goto_functionst &goto_functions) const;
+
+  inline jsont output_json(
+    const goto_modelt &goto_model) const
+  {
+    const namespacet ns(goto_model.symbol_table);
+    return output_json(ns, goto_model.goto_functions);
+  }
+
+  inline jsont output_json(
+    const namespacet &ns,
+    const goto_programt &goto_program) const
+  {
+    return output_json(ns, goto_program, "");
+  }
+
+  inline jsont output_json(
+    const namespacet &ns,
+    const goto_functionst::goto_functiont &goto_function) const
+  {
+    return output_json(ns, goto_function.body, "");
+  }
+
+  
+  virtual xmlt output_xml(
+    const namespacet &ns,
+    const goto_functionst &goto_functions) const;
+
+  inline xmlt output_xml(
+    const goto_modelt &goto_model) const
+  {
+    const namespacet ns(goto_model.symbol_table);
+    return output_xml(ns, goto_model.goto_functions);
+  }
+
+  inline xmlt output_xml(
+    const namespacet &ns,
+    const goto_programt &goto_program) const
+  {
+    return output_xml(ns, goto_program, "");
+  }
+
+  inline xmlt output_xml(
+    const namespacet &ns,
+    const goto_functionst::goto_functiont &goto_function) const
+  {
+    return output_xml(ns, goto_function.body, "");
+  }
+  
 protected:
   // overload to add a factory
   virtual void initialize(const goto_programt &);
@@ -177,6 +254,17 @@ class ai_baset
     const irep_idt &identifier,
     std::ostream &out) const;
 
+  virtual jsont output_json(
+    const namespacet &ns,
+    const goto_programt &goto_program,
+    const irep_idt &identifier) const;
+  
+  virtual xmlt output_xml(
+    const namespacet &ns,
+    const goto_programt &goto_program,
+    const irep_idt &identifier) const;
+
+
   // the work-queue is sorted by location number
   typedef std::map<unsigned, locationt> working_sett;
   

From 860031b61b209cd781fd84dc891f1d1a4974eaeb Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Thu, 8 Sep 2016 08:05:42 +0100
Subject: [PATCH 02/32] Make evaluation and/or simplification of conditions a
 domain operation.

---
 src/analyses/ai.h | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index 3d47c541edd..a4fd3cd9499 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/json.h>
 #include <util/xml.h>
+#include <util/expr.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -99,6 +100,11 @@ class ai_domain_baset
   //
   // This computes the join between "this" and "b".
   // Return true if "this" has changed.
+
+  // Used to evaluate or simplify conditions with respect to the domain
+  virtual exprt domain_simplify (const exprt &condition) const {
+    return condition;
+  }
 };
 
 // don't use me -- I am just a base class

From 1246ba56bdc2e68a0f328fcb3f5899f769f304bc Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 07:48:58 +0100
Subject: [PATCH 03/32] Refactor goto-analyze so that task, analysis, domain
 and output can all be selected independently.

---
 src/analyses/interval_domain.cpp              |  51 ++++
 src/analyses/interval_domain.h                |   4 +-
 src/analyses/is_threaded.h                    |   5 +
 src/goto-analyzer/Makefile                    |   1 +
 .../goto_analyzer_parse_options.cpp           | 172 +++++++++++-
 .../goto_analyzer_parse_options.h             |   6 +-
 src/goto-analyzer/static_analyzer.cpp         | 205 +++++++-------
 src/goto-analyzer/static_analyzer.h           |   3 +-
 src/goto-analyzer/static_show_domain.cpp      |  83 ++++++
 src/goto-analyzer/static_show_domain.h        |  26 ++
 src/goto-analyzer/static_simplifier.cpp       | 250 ++++++++++++++++++
 src/goto-analyzer/static_simplifier.h         |  26 ++
 12 files changed, 713 insertions(+), 119 deletions(-)
 create mode 100644 src/goto-analyzer/static_show_domain.cpp
 create mode 100644 src/goto-analyzer/static_show_domain.h
 create mode 100644 src/goto-analyzer/static_simplifier.cpp
 create mode 100644 src/goto-analyzer/static_simplifier.h

diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 4f8aca54d4b..bdebe9a14e6 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -500,3 +500,54 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const
   else
     return true_exprt();
 }
+
+/*******************************************************************\
+
+Function: interval_domaint::domain_simplify
+
+  Inputs: The expression to simplify.
+
+ Outputs: A simplified version of the expression.
+
+ Purpose: Uses the domain to simplify a given expression using context-specific information.
+
+\*******************************************************************/
+
+exprt interval_domaint::domain_simplify (const exprt &condition) const
+{
+  interval_domaint d(*this);
+  
+  //merge intervals to properly handle conjunction
+  if (condition.id()==ID_and)
+  {
+    interval_domaint a;
+    a.make_top();
+    a.assume(condition,ns);
+    
+#ifdef DEBUG
+    a.output(std::cout, interval_analysis, ns);
+    d.output(std::cout, interval_analysis, ns);
+#endif
+    
+    if (!a.merge(d, t, t))
+      goto make_true;
+  }
+  else if (condition.id()==ID_symbol)
+  {
+    //TODO: we have to handle symbol expression
+  }
+  else
+  {
+    d.assume(not_exprt(condition), ns);
+    if(d.is_bottom())
+      goto make_true;
+  }
+
+  return condition;
+  
+ make_true:
+  exprt e;
+  e.make_true();
+  return e;
+}
+ 
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 0c3d9aa68c9..bcc6b373081 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -75,7 +75,9 @@ class interval_domaint:public ai_domain_baset
   {
     return bottom;
   }
-
+  
+  virtual exprt domain_simplify (const exprt &condition) const;
+  
 protected:
   bool bottom;
 
diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h
index 88a785a71b9..38c36f8ad28 100644
--- a/src/analyses/is_threaded.h
+++ b/src/analyses/is_threaded.h
@@ -29,6 +29,11 @@ class is_threadedt
     return is_threaded_set.find(t)!=is_threaded_set.end();
   }
   
+  inline bool operator()(void) const
+  {
+    return !is_threaded_set.empty();
+  }
+  
 protected:
   typedef std::set<goto_programt::const_targett> is_threaded_sett;
   is_threaded_sett is_threaded_set;
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index fb58884a559..7d27be382e4 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -1,5 +1,6 @@
 SRC = goto_analyzer_main.cpp goto_analyzer_parse_options.cpp \
       taint_parser.cpp taint_analysis.cpp static_analyzer.cpp \
+      static_show_domain.cpp static_simplifier.cpp \
       unreachable_instructions.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 5f5efcf942e..ea9e372617c 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
 
+#include <analyses/is_threaded.h>
 #include <analyses/goto_check.h>
 #include <analyses/local_may_alias.h>
 
@@ -47,6 +48,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "taint_analysis.h"
 #include "unreachable_instructions.h"
 #include "static_analyzer.h"
+#include "static_show_domain.h"
+#include "static_simplifier.h"
 
 /*******************************************************************\
 
@@ -218,6 +221,101 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("error-label"))
     options.set_option("error-label", cmdline.get_values("error-label"));
   #endif
+
+  
+  // Output format choice
+  options.set_option("text", false);
+  options.set_option("json", false);
+  options.set_option("xml", false);
+  options.set_option("outfile", "-");
+  
+  if (cmdline.isset("text"))
+  {
+    options.set_option("text", true);
+    options.set_option("outfile", cmdline.get_value("text"));  
+  }
+  else if (cmdline.isset("json"))
+  {
+    options.set_option("json", true);
+    options.set_option("outfile", cmdline.get_value("json"));
+  }
+  else if (cmdline.isset("xml"))
+  {
+    options.set_option("xml", true);
+    options.set_option("outfile", cmdline.get_value("xml"));
+  }
+  else
+  {
+    options.set_option("text", true);
+  }
+
+  
+  // Task options
+  options.set_option(    "show", false);
+  options.set_option(  "verify", false);
+  options.set_option("simplify", false);
+
+  if (cmdline.isset("show") ||
+      cmdline.isset("show-intervals") ||
+      cmdline.isset("show-non-null"))
+    options.set_option("show", true);
+  else if (cmdline.isset("verify"))
+    options.set_option("verify", true);
+  else if (cmdline.isset("simplify"))
+  {
+    options.set_option("simplify", true);
+    options.set_option("outfile", cmdline.get_value("simplify"));
+  }
+
+  if (!(options.get_bool_option("show")  ||
+	options.get_bool_option("verify")  ||
+	options.get_bool_option("simplify")))
+  {
+    status() << "Task defaults to --show" << eom;
+    options.set_option("show", true);
+  }
+
+  
+  // Abstract interpreter choice
+  options.set_option("sequential", false);
+  options.set_option("concurrent", false);
+
+  if (cmdline.isset("sequential"))
+    options.set_option("sequential", true);
+  else if (cmdline.isset("concurrent"))
+    options.set_option("concurrent", true);
+  else
+  {
+    is_threadedt is_threaded(goto_model.goto_functions);
+    bool contains_concurrent_code = is_threaded();
+
+    options.set_option("sequential", !contains_concurrent_code);
+    options.set_option("concurrent",  contains_concurrent_code);
+  }
+
+  
+  // Domain choice
+  options.set_option("constants", false);
+  options.set_option("intervals", false);
+  options.set_option("non-null", false);
+
+  if (cmdline.isset("intervals") ||
+      cmdline.isset("show-intervals")) 
+    options.set_option("intervals", true);
+  else if (cmdline.isset("non-null") ||
+      cmdline.isset("show-non-null")) 
+    options.set_option("non-null", true);
+  else if (cmdline.isset("constants"))
+    options.set_option("constants", true);
+    
+  if (!(options.get_bool_option("constants")  ||
+	options.get_bool_option("intervals")  ||
+	options.get_bool_option("non-null")))
+  {
+    status() << "Domain defaults to --constants" << eom;
+    options.set_option("constants", true);
+  }
+  
 }
 
 /*******************************************************************\
@@ -342,17 +440,47 @@ int goto_analyzer_parse_optionst::doit()
     return 0;
   }
 
-  if(cmdline.isset("non-null") ||
-     cmdline.isset("intervals"))
+
+  // Output file factory
+  std::ostream *out;
+  const std::string outfile = options.get_option("outfile");
+  if (outfile == "-")
+    out = &std::cout;
+  else
+  {
+    out = new std::ofstream(outfile);
+    if(!*out)
+    {
+      error() << "Failed to open output file `"
+	      << outfile << "'" << eom;
+      return 6;
+    }
+  }
+
+
+  // Run the analysis
+  bool result = true;
+  if (options.get_bool_option("show"))
+    result = static_show_domain(goto_model, options, get_message_handler(), *out);
+
+  else if (options.get_bool_option("verify"))
+    result =    static_analyzer(goto_model, options, get_message_handler(), *out);
+
+  else if (options.get_bool_option("simplify"))
+    result =  static_simplifier(goto_model, options, get_message_handler(), *out);
+  else
   {
-    optionst options;
-    options.set_option("json", cmdline.get_value("json"));
-    options.set_option("xml", cmdline.get_value("xml"));
-    bool result=
-      static_analyzer(goto_model, options, get_message_handler());
-    return result?10:0;
+    error() << "No task given" << eom;
+    return 6;
   }
+  
+  if (out != &std::cout)
+    delete out;
+  
+  return result?10:0;
 
+  
+  // Final defensive error case
   error() << "no analysis option given -- consider reading --help"
           << eom;
   return 6;
@@ -526,17 +654,33 @@ void goto_analyzer_parse_optionst::help()
     " goto-analyzer [-h] [--help]  show help\n"
     " goto-analyzer file.c ...     source file names\n"
     "\n"
-    "Analyses:\n"
+    "Task options:\n"
     "\n"
-    " --taint file_name            perform taint analysis using rules in given file\n"
-    " --unreachable-instructions   list dead code\n"
-    " --intervals                  interval analysis\n"
-    " --non-null                   non-null analysis\n"
+    " --show                       run abstract interpreter and display domains\n"
+    " --verify                     run abstract interpreter and check assertions\n"
+    " --simplify file_name         run abstract interpreter and simplify program\n"
+    "\n"
+    "Abstract interpreter options:\n"
     "\n"
-    "Analysis options:\n"
+    " --sequential                 use sequential abstract interpreter\n"
+    " --concurrent                 use concurrent abstract interpreter\n"
+    "\n"
+    "Domain options:\n"
+    "\n"
+    " --constants                  constant abstraction\n"
+    " --intervals                  interval abstraction\n"
+    " --non-null                   non-null abstraction\n"
+    "\n"
+    "Output options:\n"
+    " --text file_name             output results in plain text to given file\n"
     " --json file_name             output results in JSON format to given file\n"
     " --xml file_name              output results in XML format to given file\n"
     "\n"
+    "Other analyses:\n"
+    "\n"
+    " --taint file_name            perform taint analysis using rules in given file\n"
+    " --unreachable-instructions   list dead code\n"
+    "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"
     " -D macro                     define preprocessor macro (C/C++)\n"
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 7eba4c7b247..65913968a2a 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -33,10 +33,12 @@ class optionst;
   "(gcc)(arch):" \
   "(taint):(show-taint)" \
   "(show-local-may-alias)" \
-  "(json):(xml):" \
+  "(json):(xml):(text):" \
   "(unreachable-instructions)" \
   "(intervals)(show-intervals)" \
-  "(non-null)(show-non-null)"
+  "(non-null)(show-non-null)" \
+  "(show)(verify)(simplify):" \
+  "(sequential)(concurrent)"
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,
diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index 89e511288af..0de14c28562 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -8,25 +8,28 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <fstream>
 
-#include <util/threeval.h>
 #include <util/json.h>
 #include <util/xml.h>
 
 #include <analyses/interval_domain.h>
+#include <analyses/constant_propagator.h>
 
 #include "static_analyzer.h"
 
+template <class analyzerT>
 class static_analyzert:public messaget
 {
 public:
   static_analyzert(
     const goto_modelt &_goto_model,
     const optionst &_options,
-    message_handlert &_message_handler):
+    message_handlert &_message_handler,
+    std::ostream &_out):
     messaget(_message_handler),
     goto_functions(_goto_model.goto_functions),
     ns(_goto_model.symbol_table),
-    options(_options)
+    options(_options),
+    out(_out)
   {
   }
   
@@ -36,38 +39,39 @@ class static_analyzert:public messaget
   const goto_functionst &goto_functions;
   const namespacet ns;
   const optionst &options;
+  std::ostream &out;
 
   // analyses
-  ait<interval_domaint> interval_analysis;
+  analyzerT domain;
 
   void plain_text_report();
-  void json_report(const std::string &);  
-  void xml_report(const std::string &);  
-  
-  tvt eval(goto_programt::const_targett);
+  void json_report();
+  void xml_report();
 };
 
 /*******************************************************************\
 
-Function: static_analyzert::operator()
+Function: static_analyzert<analyzerT>::operator()
 
-  Inputs:
+  Inputs: None.
 
- Outputs:
+ Outputs: false on success, true on failure.
 
- Purpose: 
+ Purpose: Run the analysis, check the assertions and report in the correct format.
 
 \*******************************************************************/
 
-bool static_analyzert::operator()()
+template <class analyzerT>
+bool static_analyzert<analyzerT>::operator()()
 {
-  status() << "performing interval analysis" << eom;
-  interval_analysis(goto_functions, ns);
+  status() << "performing analysis" << eom;
+  domain(goto_functions, ns);
 
-  if(!options.get_option("json").empty())
-    json_report(options.get_option("json"));
-  else if(!options.get_option("xml").empty())
-    xml_report(options.get_option("xml"));
+  
+  if(options.get_bool_option("json"))
+    json_report();
+  else if(options.get_bool_option("xml"))
+    xml_report();
   else
     plain_text_report();
 
@@ -76,38 +80,18 @@ bool static_analyzert::operator()()
   
 /*******************************************************************\
 
-Function: static_analyzert::eval
+Function: static_analyzert<analyzerT>::plain_text_report
 
-  Inputs:
+  Inputs: None.
 
- Outputs:
+ Outputs: Text report via out.
 
- Purpose: 
+ Purpose: Check the assertions and give results as text.
 
 \*******************************************************************/
 
-tvt static_analyzert::eval(goto_programt::const_targett t)
-{
-  exprt guard=t->guard;
-  interval_domaint d=interval_analysis[t];
-  d.assume(not_exprt(guard), ns);
-  if(d.is_bottom()) return tvt(true);
-  return tvt::unknown();          
-}
-
-/*******************************************************************\
-
-Function: static_analyzert::plain_text_report
-
-  Inputs:
-
- Outputs:
-
- Purpose: 
-
-\*******************************************************************/
-
-void static_analyzert::plain_text_report()
+template <class analyzerT>
+void static_analyzert<analyzerT>::plain_text_report()
 {
   unsigned pass=0, fail=0, unknown=0;
   
@@ -123,8 +107,8 @@ void static_analyzert::plain_text_report()
     forall_goto_program_instructions(i_it, f_it->second.body)
     {
       if(!i_it->is_assert()) continue;
-      
-      tvt r=eval(i_it);
+
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
       
       result() << '[' << i_it->source_location.get_property_id()
                << ']' << ' ';
@@ -133,45 +117,40 @@ void static_analyzert::plain_text_report()
       if(!i_it->source_location.get_comment().empty())
         result() << ", " << i_it->source_location.get_comment();
       result() << ": ";
-      if(r.is_true())
-        result() << "SUCCESS";
-      else if(r.is_false())
-        result() << "FAILURE";
+      if(simplified.is_true())
+        { result() << "SUCCESS"; pass++; }
+      else if(simplified.is_false())
+        { result() << "FAILURE"; fail++; }
       else
-        result() << "UNKNOWN";
+        { result() << "UNKNOWN"; unknown++; }
       result() << eom;
 
-      if(r.is_true())
-        pass++;
-      else if(r.is_false())
-        fail++;
-      else
-        unknown++;
     }
 
     status() << '\n';
   }
   
-  status() << "SUMMARY: " << pass << " pass, " << fail << " fail, "
+  status() << "SUMMARY: " << pass << " pass, " << fail << " fail if reachable, "
            << unknown << " unknown\n";
 }
 
 /*******************************************************************\
 
-Function: static_analyzert::json_report
+Function: static_analyzert<analyzerT>::json_report
 
-  Inputs:
+  Inputs: None.
 
- Outputs:
+ Outputs: JSON report via out.
 
- Purpose: 
+ Purpose: Check the assertions and give results as JSON.
 
 \*******************************************************************/
 
-void static_analyzert::json_report(const std::string &file_name)
+template <class analyzerT>
+void static_analyzert<analyzerT>::json_report()
 {
   json_arrayt json_result;
-  
+
   forall_goto_functions(f_it, goto_functions)
   {
     if(!f_it->second.body.has_assertion()) continue;
@@ -182,14 +161,14 @@ void static_analyzert::json_report(const std::string &file_name)
     forall_goto_program_instructions(i_it, f_it->second.body)
     {
       if(!i_it->is_assert()) continue;
-      
-      tvt r=eval(i_it);
+
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
 
       json_objectt &j=json_result.push_back().make_object();
 
-      if(r.is_true())
+      if(simplified.is_true())
         j["status"]=json_stringt("SUCCESS");
-      else if(r.is_false())
+      else if(simplified.is_false())
         j["status"]=json_stringt("FAILURE");
       else 
         j["status"]=json_stringt("UNKNOWN");
@@ -200,32 +179,25 @@ void static_analyzert::json_report(const std::string &file_name)
         i_it->source_location.get_comment()));
     }
   }
-
-  std::ofstream out(file_name);
-  if(!out)
-  {
-    error() << "failed to open JSON output file `"
-            << file_name << "'" << eom;
-    return;
-  }
   
-  status() << "Writing report to `" << file_name << "'" << eom;
+  status() << "Writing JSON report" << eom;
   out << json_result;
 }
 
 /*******************************************************************\
 
-Function: static_analyzert::xml_report
+Function: static_analyzert<analyzerT>::xml_report
 
-  Inputs:
+  Inputs: None.
 
- Outputs:
+ Outputs: XML report via out.
 
- Purpose: 
+ Purpose: Check the assertions and give results as XML.
 
 \*******************************************************************/
 
-void static_analyzert::xml_report(const std::string &file_name)
+template <class analyzerT>
+void static_analyzert<analyzerT>::xml_report()
 {
   xmlt xml_result;
   
@@ -240,13 +212,13 @@ void static_analyzert::xml_report(const std::string &file_name)
     {
       if(!i_it->is_assert()) continue;
       
-      tvt r=eval(i_it);
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
 
       xmlt &x=xml_result.new_element("result");
 
-      if(r.is_true())
+      if(simplified.is_true())
         x.set_attribute("status", "SUCCESS");
-      else if(r.is_false())
+      else if(simplified.is_false())
         x.set_attribute("status", "FAILURE");
       else 
         x.set_attribute("status", "UNKNOWN");
@@ -257,15 +229,7 @@ void static_analyzert::xml_report(const std::string &file_name)
     }
   }
 
-  std::ofstream out(file_name);
-  if(!out)
-  {
-    error() << "failed to open XML output file `"
-            << file_name << "'" << eom;
-    return;
-  }
-  
-  status() << "Writing report to `" << file_name << "'" << eom;
+  status() << "Writing XML report" << eom;
   out << xml_result;
 }
 
@@ -273,21 +237,60 @@ void static_analyzert::xml_report(const std::string &file_name)
 
 Function: static_analyzer
 
-  Inputs:
+  Inputs: The goto_model to check, options giving the domain and output,
+          the message handler and output stream.
 
- Outputs:
+ Outputs: Report via out.
 
- Purpose: 
+ Purpose: Runs the analyzer, check assertions and generate a report.
 
 \*******************************************************************/
 
 bool static_analyzer(
   const goto_modelt &goto_model,
   const optionst &options,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  std::ostream &out)
 {
-  return static_analyzert(
-    goto_model, options, message_handler)();
+  if (options.get_bool_option("sequential"))
+  {
+    if (options.get_bool_option("constants"))
+      return static_analyzert<ait<constant_propagator_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    else if (options.get_bool_option("intervals"))
+      return static_analyzert<ait<interval_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  return static_analyzert<ait<non_null_domaint> >
+    //    (goto_model, options, message_handler, out)();
+    
+    else
+      return true;
+  }
+  else if (options.get_bool_option("concurrent"))
+  {
+    // Constant and interval don't have merge_shared yet
+#if 0
+    if (options.get_bool_option("constants"))
+      return static_analyzert<concurrency_aware_ait<constant_propagator_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    else if (options.get_bool_option("intervals"))
+      return static_analyzert<concurrency_aware_ait<interval_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  return static_analyzert<concurrency_aware_ait<non_null_domaint> >
+    //    (goto_model, options, message_handler, out)();
+    
+    else
+#endif
+      return true;
+  }
+  else
+    return true;
 }
 
 /*******************************************************************\
diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h
index 02fa064ab11..ffdc82fd542 100644
--- a/src/goto-analyzer/static_analyzer.h
+++ b/src/goto-analyzer/static_analyzer.h
@@ -20,7 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com
 bool static_analyzer(
   const goto_modelt &,
   const optionst &,
-  message_handlert &);
+  message_handlert &,
+  std::ostream &);
 
 void show_intervals(
   const goto_modelt &,
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
new file mode 100644
index 00000000000..5501e8380ca
--- /dev/null
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+Module:
+
+Author: Martin Brain, martin.brain@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#include <fstream>
+
+#include <util/message.h>
+#include <util/json.h>
+#include <util/xml.h>
+
+#include <analyses/interval_domain.h>
+#include <analyses/constant_propagator.h>
+
+#include "static_show_domain.h"
+
+/*******************************************************************\
+
+Function: static_show_domain
+
+  Inputs: The goto_model to analyze, options giving the domain and output,
+          the message handler and output stream.
+
+ Outputs: The abstract domain via out.
+
+ Purpose: Runs the analyzer and then prints out the domain.
+
+\*******************************************************************/
+
+bool static_show_domain(
+  const goto_modelt &goto_model,
+  const optionst &options,
+  message_handlert &message_handler,
+  std::ostream &out)
+{
+  ai_baset *domain = NULL;
+  
+  if (options.get_bool_option("sequential"))
+  {
+    if (options.get_bool_option("constants"))
+      domain = new ait<constant_propagator_domaint>();
+    
+    else if (options.get_bool_option("intervals"))
+      domain = new ait<interval_domaint>();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  domain = new ait<non_null_domaint>();
+    
+  }
+  else if (options.get_bool_option("concurrent"))
+  {
+    // Constant and interval don't have merge_shared yet
+#if 0
+    if (options.get_bool_option("constants"))
+      domain = new concurrency_aware_ait<constant_propagator_domaint>();
+    
+    else if (options.get_bool_option("intervals"))
+      domain = new concurrency_aware_ait<interval_domaint>();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  domain = new concurrency_aware_ait<non_null_domaint>();    
+#endif
+  }
+
+  if (domain == NULL)
+    return true;
+
+  //status() << "performing analysis" << eom;
+  (*domain)(goto_model);
+
+  if(options.get_bool_option("json"))
+    out << domain->output_json(goto_model);
+  else if(options.get_bool_option("xml"))
+    out << domain->output_xml(goto_model);
+  else
+    domain->output(goto_model, out);
+
+  delete domain;
+  return false;
+}
diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h
new file mode 100644
index 00000000000..66681adf5e6
--- /dev/null
+++ b/src/goto-analyzer/static_show_domain.h
@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: 
+
+Author: Martin Brain, martin.brain@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef CPROVER_STATIC_SHOW_DOMAIN_H
+#define CPROVER_STATIC_SHOW_DOMAIN_H
+
+#include <iosfwd>
+
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/options.h>
+
+#include <goto-programs/goto_model.h>
+
+bool static_show_domain(
+  const goto_modelt &,
+  const optionst &,
+  message_handlert &,
+  std::ostream &);
+
+#endif
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
new file mode 100644
index 00000000000..2da5fc5c7c0
--- /dev/null
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -0,0 +1,250 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+//#define DEBUG
+
+#ifdef DEBUG
+#include <iostream>
+#endif
+
+#include <fstream>
+
+#include <goto-programs/write_goto_binary.h>
+
+#include <analyses/interval_domain.h>
+#include <analyses/constant_propagator.h>
+
+#include "static_simplifier.h"
+
+template <class analyzerT>
+class static_simplifiert:public messaget
+{
+public:
+  static_simplifiert(
+    goto_modelt &_goto_model,
+    const optionst &_options,
+    message_handlert &_message_handler,
+    std::ostream &_out):
+    messaget(_message_handler),
+    goto_functions(_goto_model.goto_functions),
+    ns(_goto_model.symbol_table),
+    options(_options),
+    out(_out)
+  {
+  }
+  
+  bool operator()(void);
+
+protected:
+  goto_functionst &goto_functions;
+  const namespacet ns;
+  const optionst &options;
+  std::ostream &out;
+
+  // analyses
+  analyzerT domain;
+
+  void simplify_program(void);
+  unsigned simplify_guard(goto_programt::instructionst::iterator &i_it);
+};
+
+/*******************************************************************\
+
+Function: static_simplifiert<analyzerT>::operator()
+
+  Inputs: None.
+
+ Outputs: false on success, true on failure.
+
+ Purpose: Run the analysis, check the assertions and report in the correct format.
+
+\*******************************************************************/
+
+template <class analyzerT>
+bool static_simplifiert<analyzerT>::operator()(void)
+{
+  status() << "performing analysis" << eom;
+  domain(goto_functions, ns);
+
+  status() << "simplifying program" << eom;
+  simplify_program();
+
+  status() << "writing goto binary" << eom;
+  return write_goto_binary(out, ns.get_symbol_table(), goto_functions);
+}
+
+
+/*******************************************************************\
+
+Function: static_simplifiert<analyzerT>::simplify_guard
+
+  Inputs: An iterator pointing to an instruction.
+
+ Outputs: 1 if simplified, 0 if not.
+
+ Purpose: Simplifies the instruction's guard using the information in the abstract domain.
+
+\*******************************************************************/
+
+template <class analyzerT>
+unsigned static_simplifiert<analyzerT>::simplify_guard(goto_programt::instructionst::iterator &i_it)
+{
+  exprt simplified = domain[i_it].domain_simplify(i_it->guard);
+  unsigned return_value = (simplified == i_it->guard) ? 0 : 1;
+  i_it->guard = simplified;
+  return return_value;
+}
+
+/*******************************************************************\
+
+Function: static_simplifiert<analyzerT>::simplify_program
+
+  Inputs: None.
+
+ Outputs: None.
+
+ Purpose: Simplifies the program using the information in the abstract domain.
+
+\*******************************************************************/
+
+template <class analyzerT>
+void static_simplifiert<analyzerT>::simplify_program()
+{
+  struct counters {
+    unsigned asserts;
+    unsigned assumes;
+    unsigned gotos;
+    unsigned assigns;
+  };
+  
+  counters simplified = {0,0,0,0};
+  counters unmodified = {0,0,0,0};
+
+  Forall_goto_functions(f_it, goto_functions)
+  {
+    Forall_goto_program_instructions(i_it, f_it->second.body)
+    {
+      if (i_it->is_assert())
+      {
+	unsigned result = simplify_guard(i_it);
+	simplified.asserts += result;
+	unmodified.asserts += (1 - result);
+      }
+      else if (i_it->is_assume())
+      {
+	unsigned result = simplify_guard(i_it);
+	simplified.assumes += result;
+	unmodified.assumes += (1 - result);
+      }
+      else if (i_it->is_goto())
+      {
+	unsigned result = simplify_guard(i_it);
+	simplified.gotos += result;
+	unmodified.gotos += (1 - result);
+      }
+      else if (i_it->is_assign())
+      {
+	code_assignt assign(to_code_assign(i_it->code));
+	
+	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs());
+	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs());
+
+	unsigned result = (simplified_lhs == assign.lhs() &&
+			   simplified_rhs == assign.rhs()) ? 0 : 1;
+	simplified.gotos += result;
+	unmodified.gotos += (1 - result);
+
+	assign.lhs() = simplified_lhs;
+	assign.rhs() = simplified_rhs;
+	i_it->code = assign;
+      }
+    }
+  }
+  
+  //make sure the references are correct
+  goto_functions.update();
+
+    
+  status() << "SIMPLIFIED: "
+	   << " assert: " << simplified.asserts
+	   << ", assume: " << simplified.assumes
+	   << ", goto: " << simplified.gotos
+	   << ", assigns: " << simplified.assigns
+	   << "\n"
+	   << "UNMODIFIED: "
+	   << " assert: " << unmodified.asserts
+	   << ", assume: " << unmodified.assumes
+	   << ", goto: " << unmodified.gotos
+	   << ", assigns: " << unmodified.assigns
+	   << eom;
+
+  return;
+}
+
+
+
+
+/*******************************************************************\
+
+Function: static_simplifier
+
+  Inputs: The goto_model to analyze and simplify, options giving the domain,
+          the message handler and output stream.
+
+ Outputs: The simplified goto binary via out.
+
+ Purpose: Runs the analyzer, simplifies and then outputs.
+
+\*******************************************************************/
+
+bool static_simplifier(
+  goto_modelt &goto_model,
+  const optionst &options,
+  message_handlert &message_handler,
+  std::ostream &out)
+{
+  if (options.get_bool_option("sequential"))
+  {
+    if (options.get_bool_option("constants"))
+      return static_simplifiert<ait<constant_propagator_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    else if (options.get_bool_option("intervals"))
+      return static_simplifiert<ait<interval_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  return static_simplifiert<ait<non_null_domaint> >
+    //    (goto_model, options, message_handler, out)();
+    
+    else
+      return true;
+  }
+  else if (options.get_bool_option("concurrent"))
+  {
+    // Constant and interval don't have merge_shared yet
+#if 0
+    if (options.get_bool_option("constants"))
+      return static_simplifiert<concurrency_aware_ait<constant_propagator_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    else if (options.get_bool_option("intervals"))
+      return static_simplifiert<concurrency_aware_ait<interval_domaint> >
+	(goto_model, options, message_handler, out)();
+    
+    //else if (options.get_bool_option("non-null"))
+    //  return static_simplifiert<concurrency_aware_ait<non_null_domaint> >
+    //    (goto_model, options, message_handler, out)();
+    
+    else
+#endif
+      return true;
+  }
+  else
+    return true;
+}
diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h
new file mode 100644
index 00000000000..0db31efea72
--- /dev/null
+++ b/src/goto-analyzer/static_simplifier.h
@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: 
+
+Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef CPROVER_STATIC_SIMPLIFIER_H
+#define CPROVER_STATIC_SIMPLIFIER_H
+
+#include <iosfwd>
+
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/options.h>
+
+#include <goto-programs/goto_model.h>
+
+bool static_simplifier(
+  goto_modelt &,
+  const optionst &,
+  message_handlert &,
+  std::ostream &);
+
+#endif

From 1b5b23b0e4acf9c2d06ecf4e8e648c4c65b288d8 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:06:42 +0100
Subject: [PATCH 04/32] Fixes for the previous commit.

---
 src/analyses/ai.h                       |  3 ++-
 src/analyses/interval_domain.cpp        | 13 ++++++-------
 src/analyses/interval_domain.h          | 10 ++++++++--
 src/goto-analyzer/static_analyzer.cpp   |  6 +++---
 src/goto-analyzer/static_simplifier.cpp |  6 +++---
 5 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index a4fd3cd9499..e9815f1f8ea 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -102,7 +102,8 @@ class ai_domain_baset
   // Return true if "this" has changed.
 
   // Used to evaluate or simplify conditions with respect to the domain
-  virtual exprt domain_simplify (const exprt &condition) const {
+  virtual exprt domain_simplify (const exprt &condition,
+				 const namespacet &ns) const {
     return condition;
   }
 };
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index bdebe9a14e6..5e789dd22f3 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -129,7 +129,7 @@ void interval_domaint::transform(
 
 /*******************************************************************\
 
-Function: interval_domaint::merge
+Function: interval_domaint::join
 
   Inputs:
 
@@ -139,10 +139,8 @@ Function: interval_domaint::merge
 
 \*******************************************************************/
 
-bool interval_domaint::merge(
-  const interval_domaint &b,
-  locationt from,
-  locationt to)
+bool interval_domaint::join(
+  const interval_domaint &b)
 {
   if(b.bottom) return false;
   if(bottom) { *this=b; return true; }
@@ -513,7 +511,8 @@ Function: interval_domaint::domain_simplify
 
 \*******************************************************************/
 
-exprt interval_domaint::domain_simplify (const exprt &condition) const
+exprt interval_domaint::domain_simplify (const exprt &condition,
+					 const namespacet &ns) const
 {
   interval_domaint d(*this);
   
@@ -529,7 +528,7 @@ exprt interval_domaint::domain_simplify (const exprt &condition) const
     d.output(std::cout, interval_analysis, ns);
 #endif
     
-    if (!a.merge(d, t, t))
+    if (!a.join(d))
       goto make_true;
   }
   else if (condition.id()==ID_symbol)
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index bcc6b373081..1b7810f0313 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -36,10 +36,15 @@ class interval_domaint:public ai_domain_baset
     const ai_baset &ai,
     const namespacet &ns) const;
 
+  bool join(const interval_domaint &b);
+  
   bool merge(
     const interval_domaint &b,
     locationt from,
-    locationt to);
+    locationt to)
+  {
+    return join(b);
+  }
   
   // no states
   virtual void make_bottom()
@@ -76,7 +81,8 @@ class interval_domaint:public ai_domain_baset
     return bottom;
   }
   
-  virtual exprt domain_simplify (const exprt &condition) const;
+  virtual exprt domain_simplify (const exprt &condition,
+				 const namespacet &ns) const;
   
 protected:
   bool bottom;
diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index 0de14c28562..a7da9e047cf 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -108,7 +108,7 @@ void static_analyzert<analyzerT>::plain_text_report()
     {
       if(!i_it->is_assert()) continue;
 
-      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns);
       
       result() << '[' << i_it->source_location.get_property_id()
                << ']' << ' ';
@@ -162,7 +162,7 @@ void static_analyzert<analyzerT>::json_report()
     {
       if(!i_it->is_assert()) continue;
 
-      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns);
 
       json_objectt &j=json_result.push_back().make_object();
 
@@ -212,7 +212,7 @@ void static_analyzert<analyzerT>::xml_report()
     {
       if(!i_it->is_assert()) continue;
       
-      exprt simplified = domain[i_it].domain_simplify(i_it->guard);
+      exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns);
 
       xmlt &x=xml_result.new_element("result");
 
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 2da5fc5c7c0..9b16d92e528 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -94,7 +94,7 @@ Function: static_simplifiert<analyzerT>::simplify_guard
 template <class analyzerT>
 unsigned static_simplifiert<analyzerT>::simplify_guard(goto_programt::instructionst::iterator &i_it)
 {
-  exprt simplified = domain[i_it].domain_simplify(i_it->guard);
+  exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns);
   unsigned return_value = (simplified == i_it->guard) ? 0 : 1;
   i_it->guard = simplified;
   return return_value;
@@ -151,8 +151,8 @@ void static_simplifiert<analyzerT>::simplify_program()
       {
 	code_assignt assign(to_code_assign(i_it->code));
 	
-	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs());
-	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs());
+	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns);
+	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns);
 
 	unsigned result = (simplified_lhs == assign.lhs() &&
 			   simplified_rhs == assign.rhs()) ? 0 : 1;

From 01e744b2ada3bea73dd97e959ca1a207fd324d2d Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:07:36 +0100
Subject: [PATCH 05/32] Remove the special case handling of --show-intervals. 
 --show --intervals does more and --show-intervals now invokes it.

---
 .../goto_analyzer_parse_options.cpp           |  6 ------
 src/goto-analyzer/static_analyzer.cpp         | 21 -------------------
 src/goto-analyzer/static_analyzer.h           |  4 ----
 3 files changed, 31 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index ea9e372617c..62e5801ecc4 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -434,12 +434,6 @@ int goto_analyzer_parse_optionst::doit()
   if(set_properties())
     return 7;
   
-  if(cmdline.isset("show-intervals"))
-  {
-    show_intervals(goto_model, std::cout);
-    return 0;
-  }
-
 
   // Output file factory
   std::ostream *out;
diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index a7da9e047cf..c82591152d6 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -292,24 +292,3 @@ bool static_analyzer(
   else
     return true;
 }
-
-/*******************************************************************\
-
-Function: show_intervals
-
-  Inputs:
-
- Outputs:
-
- Purpose: 
-
-\*******************************************************************/
-
-void show_intervals(
-  const goto_modelt &goto_model,
-  std::ostream &out)
-{
-  ait<interval_domaint> interval_analysis;
-  interval_analysis(goto_model);
-  interval_analysis.output(goto_model, out);
-}
diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h
index ffdc82fd542..72c6555d777 100644
--- a/src/goto-analyzer/static_analyzer.h
+++ b/src/goto-analyzer/static_analyzer.h
@@ -23,8 +23,4 @@ bool static_analyzer(
   message_handlert &,
   std::ostream &);
 
-void show_intervals(
-  const goto_modelt &,
-  std::ostream &);
-
 #endif

From 9bc0e26f0172e6aec4a2cd0a447aea88add3458b Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:14:45 +0100
Subject: [PATCH 06/32] Lucas' improvements and fixes to the constant and
 interval domains.

---
 src/analyses/constant_propagator.cpp | 222 ++++++++++++++++++++++-----
 src/analyses/constant_propagator.h   |   6 +
 src/analyses/interval_domain.cpp     |   4 +-
 3 files changed, 194 insertions(+), 38 deletions(-)

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 7e66937efee..66c7ca025e9 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -20,6 +20,61 @@ Author: Peter Schrammel
 
 /*******************************************************************\
 
+Function: concatenate_array_id
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt concatenate_array_id(
+		const exprt &array, const exprt &index,
+		const typet &type)
+{
+  std::string a, idx, identifier;
+  a = array.get_string(ID_identifier);
+
+  if (index.id()==ID_typecast)
+    idx = index.op0().get_string(ID_value);
+  else
+    idx = index.get_string(ID_value);
+
+  mp_integer i=string2integer(idx);
+  identifier=a+"["+integer2string(i)+"]";
+  symbol_exprt new_expr(identifier, type);
+
+  return new_expr;
+}
+
+/*******************************************************************\
+
+Function: concatenate_array_id
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt concatenate_array_id(
+		const exprt &array, const mp_integer &index,
+		const typet &type)
+{
+  std::string a, identifier;
+  a = array.get_string(ID_identifier);
+  identifier=a+"["+integer2string(index)+"]";
+  symbol_exprt new_expr(identifier, type);
+
+  return new_expr;
+}
+
+/*******************************************************************\
+
 Function: constant_propagator_domaint::assign_rec
 
   Inputs:
@@ -35,6 +90,7 @@ void constant_propagator_domaint::assign_rec(
   const exprt &lhs, const exprt &rhs,
   const namespacet &ns)
 {
+  const typet & lhs_type = ns.follow(lhs.type());
   const typet & rhs_type = ns.follow(rhs.type());
 
 #ifdef DEBUG
@@ -42,7 +98,28 @@ void constant_propagator_domaint::assign_rec(
             << " := " << from_type(ns, "", rhs_type) << std::endl;
 #endif
 
-  if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
+  if(lhs.id()==ID_symbol && rhs.id()==ID_if)
+  {
+	exprt cond=rhs.op0();
+	assert(cond.operands().size()==2);
+	if(values.is_constant(cond.op0())
+			&& values.is_constant(cond.op1()))
+	{
+      if(cond.op0().id()==ID_index)
+      {
+    	exprt index=cond.op0();
+        exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type());
+        values.replace_const(new_expr);
+        cond.op0()=new_expr;
+        cond = simplify_expr(cond,ns);
+      }
+      else
+        assert(0);
+
+      assign(values, to_symbol_expr(lhs), cond, ns);
+	}
+  }
+  else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
                          && rhs_type.id()!=ID_struct
                          && rhs_type.id()!=ID_union)
   {
@@ -51,6 +128,27 @@ void constant_propagator_domaint::assign_rec(
     else
       values.set_to_top(to_symbol_expr(lhs));
   }
+  else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array
+		                       && rhs_type.id()==ID_array)
+  {
+	exprt new_expr;
+	mp_integer idx=0;
+    forall_operands(it, rhs)
+	{
+  	  new_expr=concatenate_array_id(lhs, idx, it->type());
+  	  assign(values, to_symbol_expr(new_expr), *it, ns);
+  	  idx = idx +1;
+	}
+  }
+  else if (lhs.id()==ID_index)
+  {
+	if (values.is_constant(lhs.op1())
+	 && values.is_constant(rhs))
+	{
+	  exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type());
+      assign(values, to_symbol_expr(new_expr), rhs, ns);
+	}
+  }
 #if 0
   else //TODO: could make field or array element-sensitive
   {
@@ -85,7 +183,7 @@ void constant_propagator_domaint::transform(
   std::cout << "before:\n";
   output(std::cout,ai,ns);
 #endif
-  
+
   if(from->is_decl())
   {
     const code_declt &code_decl=to_code_decl(from->code);
@@ -105,13 +203,22 @@ void constant_propagator_domaint::transform(
   }
   else if(from->is_goto())
   {
-    exprt g; 
+	exprt g;
     if(from->get_target()==to)
       g = simplify_expr(from->guard, ns);
     else
       g = simplify_expr(not_exprt(from->guard), ns);
 
-    two_way_propagate_rec(g, ns);
+    if (g.is_false())
+     values.set_to_bottom();
+    else
+    {
+      //TODO: we need to support widening!
+      if (g.is_constant())
+        values.set_to_top();
+      else
+        two_way_propagate_rec(g, ns);
+    }
   }
   else if(from->is_dead())
   {
@@ -141,6 +248,7 @@ void constant_propagator_domaint::transform(
     else
       values.set_to_top();
   }
+
 #ifdef DEBUG
   std::cout << "after:\n";
   output(std::cout,ai,ns);
@@ -226,6 +334,30 @@ void constant_propagator_domaint::assign(
 
 /*******************************************************************\
 
+Function: constant_propagator_domaint::is_array_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const
+{
+  exprt new_expr = concatenate_array_id(expr.op0(),
+		  expr.op1(), expr.type());
+
+  if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) ==
+         replace_const.expr_map.end())
+    return false;
+
+  return true;
+}
+
+/*******************************************************************\
+
 Function: constant_propagator_domaint::valuest::is_constant
 
   Inputs:
@@ -251,6 +383,9 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
        replace_const.expr_map.end())
       return false;
 
+  if (expr.id()==ID_index)
+	return is_array_constant(expr);
+
   if(expr.id()==ID_address_of)
     return is_constant_address_of(to_address_of_expr(expr).object());
 
@@ -397,47 +532,29 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
   
   bool changed = false;
 
-  //set everything to top that is not in src
-  for(replace_symbolt::expr_mapt::const_iterator 
-        it=replace_const.expr_map.begin();
-      it!=replace_const.expr_map.end();
-      )
+  for(replace_symbolt::expr_mapt::iterator
+	  it=replace_const.expr_map.begin();
+      it!=replace_const.expr_map.end(); ) // no it++
   {
-    if(src.replace_const.expr_map.find(it->first) ==
-       src.replace_const.expr_map.end())
+    const replace_symbolt::expr_mapt::const_iterator
+      b_it=src.replace_const.expr_map.find(it->first);
+
+    if(b_it==src.replace_const.expr_map.end())
     {
       //cannot use set_to_top here
-      replace_const.expr_map.erase(it++);
+      replace_const.expr_map.erase(it);
       changed = true;
+      break;
     }
-    else ++it;
-  }
-
-  for(replace_symbolt::expr_mapt::const_iterator 
-      it=src.replace_const.expr_map.begin();
-      it!=src.replace_const.expr_map.end();
-      ++it)
-  {      
-    replace_symbolt::expr_mapt::iterator 
-      c_it = replace_const.expr_map.find(it->first);
-
-    if(c_it != replace_const.expr_map.end())
+    else
     {
-      // values are different, set to top
-      if(c_it->second != it->second)
-      {
-        changed = set_to_top(it->first);
-        assert(changed);
-      }
+      const exprt previous=it->second;
+      replace_const.expr_map[b_it->first]=b_it->second;
+      if (it->second != previous) changed = true;
+
+      it++;
     }
-    // is not in "this", ignore
-    else { }
   }
-
-#ifdef DEBUG
-  std::cout << "merged: " << changed << '\n';
-#endif
-
   return changed;
 }
 
@@ -529,6 +646,34 @@ void constant_propagator_ait::replace(
 
 /*******************************************************************\
 
+Function: constant_propagator_ait::replace_array_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void constant_propagator_ait::replace_array_symbol(exprt &expr)
+{
+  if (expr.id()==ID_index)
+	expr = concatenate_array_id(expr.op0(),
+			  expr.op1(), expr.type());
+
+  Forall_operands(it, expr)
+  {
+	if (it->id()==ID_equal)
+	  replace_array_symbol(it->op0());
+	else if (it->id()==ID_index)
+	  replace_array_symbol(expr.op0());
+  }
+
+}
+
+/*******************************************************************\
+
 Function: constant_propagator_ait::replace
 
   Inputs:
@@ -555,6 +700,7 @@ void constant_propagator_ait::replace(
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
+      replace_array_symbol(it->guard);
       s_it->second.values.replace_const(it->guard);
       it->guard = simplify_expr(it->guard, ns);
     }
@@ -563,6 +709,8 @@ void constant_propagator_ait::replace(
       exprt &rhs = to_code_assign(it->code).rhs();
       s_it->second.values.replace_const(rhs);
       rhs = simplify_expr(rhs, ns);
+      if (rhs.id()==ID_constant)
+        rhs.add_source_location()=it->code.op0().source_location();
     }
     else if(it->is_function_call())
     {
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 7c7d7086373..8583ebf0110 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -52,6 +52,7 @@ class constant_propagator_domaint:public ai_domain_baset
     }
 
     bool is_constant(const exprt &expr) const;
+    bool is_array_constant(const exprt &expr) const;
     bool is_constant_address_of(const exprt &expr) const;
     bool set_to_top(const irep_idt &id);
 
@@ -65,6 +66,7 @@ class constant_propagator_domaint:public ai_domain_baset
       replace_const.clear();
       is_bottom = false;
     }
+
   };
 
   valuest values;
@@ -106,6 +108,9 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
 protected:
   friend class constant_propagator_domaint;
 
+  void replace_array_symbol(
+		  exprt &expr);
+
   void replace(
     goto_functionst::goto_functiont &,
     const namespacet &);
@@ -117,6 +122,7 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
   void replace_types_rec(
     const replace_symbolt &replace_const, 
     exprt &expr);
+
 };
 
 #endif
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 5e789dd22f3..6f0b022f3bd 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -150,7 +150,9 @@ bool interval_domaint::join(
   for(int_mapt::iterator it=int_map.begin();
       it!=int_map.end(); ) // no it++
   {
-    const int_mapt::const_iterator b_it=b.int_map.begin();
+    //search for the variable that needs to be merged
+    //containers have different size and variable order
+    const int_mapt::const_iterator b_it=b.int_map.find(it->first);
     if(b_it==b.int_map.end())
     {
       it=int_map.erase(it);

From d64b6f171d24a301486b86b554e77c85aed20c4c Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:19:26 +0100
Subject: [PATCH 07/32] Lucas' rather fantastic regression tests.

---
 regression/goto-analyzer/Makefile             |  5 +++
 .../constant_propagation1.c                   | 14 ++++++
 .../constant_propagation_01/test.desc         |  9 ++++
 .../constant_propagation_02.c                 | 13 ++++++
 .../constant_propagation_02/test.desc         |  9 ++++
 .../constant_propagation_03.c                 | 13 ++++++
 .../constant_propagation_03/test.desc         |  9 ++++
 .../constant_propagation_04.c                 | 13 ++++++
 .../constant_propagation_04/test.desc         |  9 ++++
 .../constant_propagation_05.c                 | 13 ++++++
 .../constant_propagation_05/test.desc         |  8 ++++
 .../constant_propagation_06.c                 | 30 +++++++++++++
 .../constant_propagation_06/test.desc         | 15 +++++++
 .../constant_propagation_07.c                 | 14 ++++++
 .../constant_propagation_07/test.desc         |  9 ++++
 .../constant_propagation_08.c                 | 16 +++++++
 .../constant_propagation_08/test.desc         | 10 +++++
 .../constant_propagation_09.c                 | 14 ++++++
 .../constant_propagation_09/test.desc         |  9 ++++
 .../constant_propagation_10.c                 | 25 +++++++++++
 .../constant_propagation_10/test.desc         |  9 ++++
 .../constant_propagation_11.c                 | 17 ++++++++
 .../constant_propagation_11/test.desc         |  9 ++++
 .../constant_propagation_12.c                 | 13 ++++++
 .../constant_propagation_12/test.desc         |  9 ++++
 .../constant_propagation_13.c                 | 14 ++++++
 .../constant_propagation_13/test.desc         |  8 ++++
 .../constant_propagation_14.c                 | 13 ++++++
 .../constant_propagation_14/test.desc         |  9 ++++
 .../constant_propagation_15.c                 | 13 ++++++
 .../constant_propagation_15/test.desc         |  9 ++++
 .../constant_propagation_16.c                 | 13 ++++++
 .../constant_propagation_16/test.desc         |  8 ++++
 .../constant_propagation_17.c                 | 16 +++++++
 .../constant_propagation_17/test.desc         |  9 ++++
 .../constant_propagation_18.c                 | 13 ++++++
 .../constant_propagation_18/test.desc         |  8 ++++
 .../goto-analyzer/intervals1/intervals1.c     |  4 +-
 regression/goto-analyzer/intervals1/test.desc |  2 +-
 .../goto-analyzer/intervals10/intervals10.c   | 21 +++++++++
 .../goto-analyzer/intervals10/test.desc       | 12 ++++++
 .../goto-analyzer/intervals11/intervals11.c   | 43 +++++++++++++++++++
 .../goto-analyzer/intervals11/test.desc       |  9 ++++
 .../goto-analyzer/intervals2/intervals2.c     |  6 +--
 regression/goto-analyzer/intervals2/test.desc |  2 +-
 regression/goto-analyzer/intervals3/test.desc |  2 +-
 regression/goto-analyzer/intervals4/test.desc |  2 +-
 regression/goto-analyzer/intervals5/test.desc |  2 +-
 regression/goto-analyzer/intervals6/test.desc |  2 +-
 regression/goto-analyzer/intervals7/test.desc |  2 +-
 .../goto-analyzer/intervals8/intervals8.c     |  9 ++++
 regression/goto-analyzer/intervals8/test.desc |  8 ++++
 .../goto-analyzer/intervals9/intervals9.c     | 12 ++++++
 regression/goto-analyzer/intervals9/test.desc |  8 ++++
 54 files changed, 581 insertions(+), 12 deletions(-)
 create mode 100644 regression/goto-analyzer/constant_propagation_01/constant_propagation1.c
 create mode 100644 regression/goto-analyzer/constant_propagation_01/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c
 create mode 100644 regression/goto-analyzer/constant_propagation_02/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c
 create mode 100644 regression/goto-analyzer/constant_propagation_03/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c
 create mode 100644 regression/goto-analyzer/constant_propagation_04/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c
 create mode 100644 regression/goto-analyzer/constant_propagation_05/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c
 create mode 100644 regression/goto-analyzer/constant_propagation_06/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c
 create mode 100644 regression/goto-analyzer/constant_propagation_07/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c
 create mode 100644 regression/goto-analyzer/constant_propagation_08/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c
 create mode 100644 regression/goto-analyzer/constant_propagation_09/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c
 create mode 100644 regression/goto-analyzer/constant_propagation_10/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c
 create mode 100644 regression/goto-analyzer/constant_propagation_11/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c
 create mode 100644 regression/goto-analyzer/constant_propagation_12/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c
 create mode 100644 regression/goto-analyzer/constant_propagation_13/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c
 create mode 100644 regression/goto-analyzer/constant_propagation_14/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c
 create mode 100644 regression/goto-analyzer/constant_propagation_15/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c
 create mode 100644 regression/goto-analyzer/constant_propagation_16/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c
 create mode 100644 regression/goto-analyzer/constant_propagation_17/test.desc
 create mode 100644 regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c
 create mode 100644 regression/goto-analyzer/constant_propagation_18/test.desc
 create mode 100644 regression/goto-analyzer/intervals10/intervals10.c
 create mode 100644 regression/goto-analyzer/intervals10/test.desc
 create mode 100644 regression/goto-analyzer/intervals11/intervals11.c
 create mode 100644 regression/goto-analyzer/intervals11/test.desc
 create mode 100644 regression/goto-analyzer/intervals8/intervals8.c
 create mode 100644 regression/goto-analyzer/intervals8/test.desc
 create mode 100644 regression/goto-analyzer/intervals9/intervals9.c
 create mode 100644 regression/goto-analyzer/intervals9/test.desc

diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
index 5701431a37e..13d335a09a3 100644
--- a/regression/goto-analyzer/Makefile
+++ b/regression/goto-analyzer/Makefile
@@ -12,3 +12,8 @@ show:
 			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
+
+clean:
+	find . -name *.*~ | xargs rm -f
+	find . -name *.out | xargs rm -f
+	rm -f tests.log	
diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c
new file mode 100644
index 00000000000..801a21535a9
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+  
+  if (j==20)
+  {
+    int x=1,y=2,z;
+    z=x+y;
+    assert(z==3);
+  }
+    
+}
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
new file mode 100644
index 00000000000..021cefd596d
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation1.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c
new file mode 100644
index 00000000000..ff139437bd8
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i==0) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
new file mode 100644
index 00000000000..6a98be47719
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_02.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c
new file mode 100644
index 00000000000..f08f6020d82
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i==0) 
+  {
+    i++;
+    j++;
+  }
+  assert(j==3);
+}
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
new file mode 100644
index 00000000000..6cc2dc04c87
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_03.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c
new file mode 100644
index 00000000000..ca003ccd2b8
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j==3);
+}
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
new file mode 100644
index 00000000000..8efe559b80e
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_04.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c
new file mode 100644
index 00000000000..037fbbe0632
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}
diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc
new file mode 100644
index 00000000000..068a8edb26d
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_05/test.desc
@@ -0,0 +1,8 @@
+CORE
+constant_propagation_05.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c
new file mode 100644
index 00000000000..d1d29427250
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c
@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+
+  if(i>=20)
+    assert(i>=10); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=30); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=15); // fails
+
+  if(i<1 && i>10)
+    assert(0); // success
+
+  if(i>=10 && j>=i)
+    assert(j>=10); // success
+
+  if(i>=j)
+    assert(i>=j); // unknown
+
+  if(i>10)
+    assert(i>=11); // success
+
+  if(i<=100 && j<i)
+    assert(j<100); // success
+}
diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc
new file mode 100644
index 00000000000..365441dfc11
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_06/test.desc
@@ -0,0 +1,15 @@
+CORE
+constant_propagation_06.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
+^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
+^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
+^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
+^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
+^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
+^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
+^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c
new file mode 100644
index 00000000000..40b04edfdd0
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<51);
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
new file mode 100644
index 00000000000..a9560eeeff9
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_07.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<50: UNKNOWN$
+^\[main.assertion.2\] file constant_propagation_07.c line 13 function main, assertion i<51: SUCCESS$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c
new file mode 100644
index 00000000000..3909e3889e4
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<50);
+  assert(i<51);
+  assert(i<52);
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc
new file mode 100644
index 00000000000..2a5fee8ad0d
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_08/test.desc
@@ -0,0 +1,10 @@
+CORE
+constant_propagation_08.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
+^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$
+^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c
new file mode 100644
index 00000000000..002e9063228
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j<52);
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc
new file mode 100644
index 00000000000..3151e28dd4d
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_09/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_09.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+******** Function main
+^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c
new file mode 100644
index 00000000000..169f7965b9d
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c
@@ -0,0 +1,25 @@
+#include <assert.h>
+int main()
+{
+  signed int i;
+  signed int j;
+  i = 0;
+   if(!(i >= 2))
+  {
+    j = j + 1;
+    i = i + 1;
+    if(!(i >= 2))
+    {
+      j = j + 1;
+      i = i + 1;
+      if(!(i >= 2))
+      {
+        j = j + 1;
+        i = i + 1;
+      }
+      assert(!(i < 2));
+    }
+  }
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc
new file mode 100644
index 00000000000..f2a9dc4f270
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_10/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_10.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c
new file mode 100644
index 00000000000..3022a4f0f19
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+int main()
+{
+  int a[2];
+  int i;
+  i = 0;
+
+  if (i==0)
+    a[0]=1;
+  else
+    a[1]=2;
+
+  assert(a[0]==1 || a[1]==2);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
new file mode 100644
index 00000000000..f2a9dc4f270
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_10.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c
new file mode 100644
index 00000000000..55ea9ac7fc2
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==0);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
new file mode 100644
index 00000000000..895045498e5
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_12.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c
new file mode 100644
index 00000000000..ac5933e9177
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+  int i, y;
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==2);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc
new file mode 100644
index 00000000000..65bff1aaeee
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_13/test.desc
@@ -0,0 +1,8 @@
+CORE
+constant_propagation_13.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c
new file mode 100644
index 00000000000..124d1e30a20
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==1 /*|| a[0]==2*/);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc
new file mode 100644
index 00000000000..24c1049e8f6
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_14/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_14.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c
new file mode 100644
index 00000000000..9a7e7692d62
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int i=0, y;
+
+  if (i==0)
+    y=1;
+
+  assert(y==1);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc
new file mode 100644
index 00000000000..25c91b5b778
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_15/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_15.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c
new file mode 100644
index 00000000000..102cfd7f812
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int i=0, y;
+
+  if (i==0)
+    y=1;
+
+  assert(y==0);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc
new file mode 100644
index 00000000000..97d9467775b
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_16/test.desc
@@ -0,0 +1,8 @@
+CORE
+constant_propagation_16.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c
new file mode 100644
index 00000000000..8b426fe84b5
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+  else 
+    a[0]=2;
+
+  assert(a[0]==1 || a[0]==2);
+  assert(a[0]==1 && a[0]==2);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc
new file mode 100644
index 00000000000..750ef150d28
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_17/test.desc
@@ -0,0 +1,9 @@
+CORE
+constant_propagation_17.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_17.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$
+^\[main.assertion.2\] file constant_propagation_17.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c
new file mode 100644
index 00000000000..6639f9b5c81
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==2);
+
+  return 0;
+}
+
diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc
new file mode 100644
index 00000000000..800e1cb46c7
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_18/test.desc
@@ -0,0 +1,8 @@
+CORE
+constant_propagation_18.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_18.c line 9 function main, assertion a\[0\]==2: FAILURE$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals1/intervals1.c
index 026e572f8ef..cdec490fe6d 100644
--- a/regression/goto-analyzer/intervals1/intervals1.c
+++ b/regression/goto-analyzer/intervals1/intervals1.c
@@ -2,11 +2,11 @@
 
 int main()
 {
-  int i, j;
+  int i, j=20;
   
   if(i>=20)
     assert(i>=10);
-  
+
   if(i>=10 && i<=20)
     assert(i!=30);
 
diff --git a/regression/goto-analyzer/intervals1/test.desc b/regression/goto-analyzer/intervals1/test.desc
index 3e81f14023a..7aca700f7a5 100644
--- a/regression/goto-analyzer/intervals1/test.desc
+++ b/regression/goto-analyzer/intervals1/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals1.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$
diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals10/intervals10.c
new file mode 100644
index 00000000000..b27cc6f2001
--- /dev/null
+++ b/regression/goto-analyzer/intervals10/intervals10.c
@@ -0,0 +1,21 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j;
+
+  if(i<=100 && j<i)
+    assert(j<=100); 
+
+  if(i<=100 && j<i)
+    assert(j<101); 
+
+  if(i<=100 && j<i)
+    assert(j>100); // fails 
+
+  if(i<=100 && j<i)
+    assert(j<99); // fails 
+
+  if(i<=100 && j<i)
+    assert(j==100); // fails   
+}
diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc
new file mode 100644
index 00000000000..f2296d2a6b7
--- /dev/null
+++ b/regression/goto-analyzer/intervals10/test.desc
@@ -0,0 +1,12 @@
+CORE
+intervals10.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$
+^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$
+^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: UNKNOWN$
+^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$
+^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: UNKNOWN$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals11/intervals11.c b/regression/goto-analyzer/intervals11/intervals11.c
new file mode 100644
index 00000000000..2f061cd554d
--- /dev/null
+++ b/regression/goto-analyzer/intervals11/intervals11.c
@@ -0,0 +1,43 @@
+#include <assert.h>
+const int xLen = 10;
+const int Alen = 2;
+const int Blen = 1;
+float nondet_float();
+int main() {
+  float A[] = {1.0f,-0.5f};
+  float B[] = {1.0f};
+  int i,j;
+  float x[xLen];
+  float x_aux[xLen];
+  float y[xLen];
+  float y_aux[xLen];
+  float total=0;
+  for (i=0;i<xLen;i++) {
+    x[i]=nondet_float();    
+    __CPROVER_assume(x[i]>=-1 && x[i]<=1);
+    x_aux[i]=0;
+    y_aux[i]=0;
+  }
+  for(i=0;i<xLen;i++) {
+    y[i] = 0; //clear y
+    /* Update past x values */
+    for(j=Blen-1;j>=1;j--)
+      x_aux[j] = x_aux[j-1];
+    x_aux[0] = x[i];
+    /* Num, x values */
+    for (j = 0; j < Blen; j++) {
+      y[i] = y[i] + B[j]*x_aux[j];
+      assert(y[i]>=-1.0f && y[i]<=1.0f); //success
+    }
+    /* Den, y values */
+    for(j=0;j<Alen-1;j++) {
+      y[i] = y[i]-A[j+1]*y_aux[j];
+      assert(y[i]>=-1.0f && y[i]<=1.0f); //fails
+    }
+    /* Update past y values */
+    for(j=Alen-2;j>=1;j--)
+      y_aux[j] = y_aux[j-1];
+    y_aux[0] = y[i];
+  }
+}
+
diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc
new file mode 100644
index 00000000000..eb2cd73a6df
--- /dev/null
+++ b/regression/goto-analyzer/intervals11/test.desc
@@ -0,0 +1,9 @@
+CORE
+intervals11.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals11.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$
+^\[main.assertion.2\] file intervals11.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals2/intervals2.c
index d1eaf25240e..d542854bb6a 100644
--- a/regression/goto-analyzer/intervals2/intervals2.c
+++ b/regression/goto-analyzer/intervals2/intervals2.c
@@ -2,10 +2,10 @@
 
 int main(){
   int x;
-  if (x > 0) {
-    if (x < 20) {
+  if (x > 0 && x < 20) {
+    //if (x < 20) {
       assert(x > -10 && x < 100);
-    }
+    //}
   }
   return 0;
 }
diff --git a/regression/goto-analyzer/intervals2/test.desc b/regression/goto-analyzer/intervals2/test.desc
index 0c017f6b333..3341c4cd069 100644
--- a/regression/goto-analyzer/intervals2/test.desc
+++ b/regression/goto-analyzer/intervals2/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals2.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$
diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc
index 5db07df08a4..dceec17bc81 100644
--- a/regression/goto-analyzer/intervals3/test.desc
+++ b/regression/goto-analyzer/intervals3/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals3.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$
diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc
index 9f56ff02403..92724fd69ee 100644
--- a/regression/goto-analyzer/intervals4/test.desc
+++ b/regression/goto-analyzer/intervals4/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals4.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc
index 42554724e2d..0213e7b3297 100644
--- a/regression/goto-analyzer/intervals5/test.desc
+++ b/regression/goto-analyzer/intervals5/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals5.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$
diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc
index 14fd64f33dd..ae01b92499a 100644
--- a/regression/goto-analyzer/intervals6/test.desc
+++ b/regression/goto-analyzer/intervals6/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals6.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$
diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc
index aeeb24bd0a9..4d8619cfacb 100644
--- a/regression/goto-analyzer/intervals7/test.desc
+++ b/regression/goto-analyzer/intervals7/test.desc
@@ -1,6 +1,6 @@
 CORE
 intervals7.c
---intervals
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$
diff --git a/regression/goto-analyzer/intervals8/intervals8.c b/regression/goto-analyzer/intervals8/intervals8.c
new file mode 100644
index 00000000000..4128ac07ce5
--- /dev/null
+++ b/regression/goto-analyzer/intervals8/intervals8.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0 && x < 20) {
+      assert(x < -10 && x < 100);
+  }
+  return 0;
+}
diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc
new file mode 100644
index 00000000000..8d1f7817ab6
--- /dev/null
+++ b/regression/goto-analyzer/intervals8/test.desc
@@ -0,0 +1,8 @@
+CORE
+intervals8.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: UNKNOWN$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals9/intervals9.c
new file mode 100644
index 00000000000..e9bc51f30b5
--- /dev/null
+++ b/regression/goto-analyzer/intervals9/intervals9.c
@@ -0,0 +1,12 @@
+//#include <assert.h>
+
+int main()
+{
+  int i;
+  
+  if(i>0)
+    if(i<3)
+      assert(i>=1 && i<=2);
+ 
+  return 0;
+} 
diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc
new file mode 100644
index 00000000000..c6fec9c4c6d
--- /dev/null
+++ b/regression/goto-analyzer/intervals9/test.desc
@@ -0,0 +1,8 @@
+CORE
+intervals9.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
+--
+^warning: ignoring

From 4fa07267811b8ad165911d9e023bf2e833584f91 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:30:42 +0100
Subject: [PATCH 08/32] Make the help text more consistent.

---
 src/goto-analyzer/goto_analyzer_parse_options.cpp | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 62e5801ecc4..605cde779e3 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -649,18 +649,15 @@ void goto_analyzer_parse_optionst::help()
     " goto-analyzer file.c ...     source file names\n"
     "\n"
     "Task options:\n"
-    "\n"
     " --show                       run abstract interpreter and display domains\n"
     " --verify                     run abstract interpreter and check assertions\n"
     " --simplify file_name         run abstract interpreter and simplify program\n"
     "\n"
     "Abstract interpreter options:\n"
-    "\n"
     " --sequential                 use sequential abstract interpreter\n"
     " --concurrent                 use concurrent abstract interpreter\n"
     "\n"
     "Domain options:\n"
-    "\n"
     " --constants                  constant abstraction\n"
     " --intervals                  interval abstraction\n"
     " --non-null                   non-null abstraction\n"
@@ -671,7 +668,6 @@ void goto_analyzer_parse_optionst::help()
     " --xml file_name              output results in XML format to given file\n"
     "\n"
     "Other analyses:\n"
-    "\n"
     " --taint file_name            perform taint analysis using rules in given file\n"
     " --unreachable-instructions   list dead code\n"
     "\n"

From 94d8790885621867d98391b062195ec507ded469 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:37:06 +0100
Subject: [PATCH 09/32] Add a missing flag.

---
 src/goto-analyzer/goto_analyzer_parse_options.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 65913968a2a..8910f760f79 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -37,6 +37,7 @@ class optionst;
   "(unreachable-instructions)" \
   "(intervals)(show-intervals)" \
   "(non-null)(show-non-null)" \
+  "(constants)" \
   "(show)(verify)(simplify):" \
   "(sequential)(concurrent)"
 

From 03cbb19da675fd2bc01f9a6a13d12fa7794ecc9e Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:40:44 +0100
Subject: [PATCH 10/32] Update the flags used to match the refactoring.

---
 regression/goto-analyzer/Makefile                          | 1 +
 regression/goto-analyzer/constant_propagation_01/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_02/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_03/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_04/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_05/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_06/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_07/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_08/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_09/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_10/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_11/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_12/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_13/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_14/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_15/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_16/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_17/test.desc | 2 +-
 regression/goto-analyzer/constant_propagation_18/test.desc | 2 +-
 19 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
index 13d335a09a3..2c534c8749a 100644
--- a/regression/goto-analyzer/Makefile
+++ b/regression/goto-analyzer/Makefile
@@ -16,4 +16,5 @@ show:
 clean:
 	find . -name *.*~ | xargs rm -f
 	find . -name *.out | xargs rm -f
+	find . -name *.goto | xargs rm -f
 	rm -f tests.log	
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
index 021cefd596d..12178cfec13 100644
--- a/regression/goto-analyzer/constant_propagation_01/test.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation1.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
index 6a98be47719..4e24ea57c68 100644
--- a/regression/goto-analyzer/constant_propagation_02/test.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_02.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
index 6cc2dc04c87..9134ef9cfa8 100644
--- a/regression/goto-analyzer/constant_propagation_03/test.desc
+++ b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_03.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
index 8efe559b80e..2e27a8ec3e5 100644
--- a/regression/goto-analyzer/constant_propagation_04/test.desc
+++ b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_04.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc
index 068a8edb26d..4c196b063af 100644
--- a/regression/goto-analyzer/constant_propagation_05/test.desc
+++ b/regression/goto-analyzer/constant_propagation_05/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_05.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE$
diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc
index 365441dfc11..b914152e5a7 100644
--- a/regression/goto-analyzer/constant_propagation_06/test.desc
+++ b/regression/goto-analyzer/constant_propagation_06/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_06.c
---constant-propagation --intervals --verify
+--constants --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
index a9560eeeff9..5e6bbfc32cc 100644
--- a/regression/goto-analyzer/constant_propagation_07/test.desc
+++ b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_07.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<50: UNKNOWN$
diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc
index 2a5fee8ad0d..131ed1c001b 100644
--- a/regression/goto-analyzer/constant_propagation_08/test.desc
+++ b/regression/goto-analyzer/constant_propagation_08/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_08.c
---constant-propagation --intervals --verify
+--constants --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc
index 3151e28dd4d..562916fc138 100644
--- a/regression/goto-analyzer/constant_propagation_09/test.desc
+++ b/regression/goto-analyzer/constant_propagation_09/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_09.c
---constant-propagation --intervals --verify
+--constants --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ******** Function main
diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc
index f2a9dc4f270..bb3a4fa51fe 100644
--- a/regression/goto-analyzer/constant_propagation_10/test.desc
+++ b/regression/goto-analyzer/constant_propagation_10/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_10.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
index f2a9dc4f270..bb3a4fa51fe 100644
--- a/regression/goto-analyzer/constant_propagation_11/test.desc
+++ b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_10.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
index 895045498e5..ddec139e1d7 100644
--- a/regression/goto-analyzer/constant_propagation_12/test.desc
+++ b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_12.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc
index 65bff1aaeee..4c526d75784 100644
--- a/regression/goto-analyzer/constant_propagation_13/test.desc
+++ b/regression/goto-analyzer/constant_propagation_13/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_13.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$
diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc
index 24c1049e8f6..cdd022e1396 100644
--- a/regression/goto-analyzer/constant_propagation_14/test.desc
+++ b/regression/goto-analyzer/constant_propagation_14/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_14.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc
index 25c91b5b778..d2b49a78162 100644
--- a/regression/goto-analyzer/constant_propagation_15/test.desc
+++ b/regression/goto-analyzer/constant_propagation_15/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_15.c
---constant-propagation --simplify
+--constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
 ^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc
index 97d9467775b..3157d7a1f56 100644
--- a/regression/goto-analyzer/constant_propagation_16/test.desc
+++ b/regression/goto-analyzer/constant_propagation_16/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_16.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE$
diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc
index 750ef150d28..397848b6430 100644
--- a/regression/goto-analyzer/constant_propagation_17/test.desc
+++ b/regression/goto-analyzer/constant_propagation_17/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_17.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_17.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$
diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc
index 800e1cb46c7..8e7133092b4 100644
--- a/regression/goto-analyzer/constant_propagation_18/test.desc
+++ b/regression/goto-analyzer/constant_propagation_18/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_18.c
---constant-propagation --verify
+--constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_18.c line 9 function main, assertion a\[0\]==2: FAILURE$

From ccf757923faaa35d61edb9f565e787c8f81cc1cd Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:44:36 +0100
Subject: [PATCH 11/32] Correct the statistics printed by the simplifier.

---
 src/goto-analyzer/static_simplifier.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 9b16d92e528..7e68cb8c5f6 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -156,8 +156,8 @@ void static_simplifiert<analyzerT>::simplify_program()
 
 	unsigned result = (simplified_lhs == assign.lhs() &&
 			   simplified_rhs == assign.rhs()) ? 0 : 1;
-	simplified.gotos += result;
-	unmodified.gotos += (1 - result);
+	simplified.assign += result;
+	unmodified.assign += (1 - result);
 
 	assign.lhs() = simplified_lhs;
 	assign.rhs() = simplified_rhs;

From fc441375f2fbaa33b3d045f7b91e86517e5792c4 Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 08:45:38 +0100
Subject: [PATCH 12/32] ... and again ...

---
 src/goto-analyzer/static_simplifier.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 7e68cb8c5f6..831b42535bf 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -156,8 +156,8 @@ void static_simplifiert<analyzerT>::simplify_program()
 
 	unsigned result = (simplified_lhs == assign.lhs() &&
 			   simplified_rhs == assign.rhs()) ? 0 : 1;
-	simplified.assign += result;
-	unmodified.assign += (1 - result);
+	simplified.assigns += result;
+	unmodified.assigns += (1 - result);
 
 	assign.lhs() = simplified_lhs;
 	assign.rhs() = simplified_rhs;

From 60cb0b6f2b7fbbfd446dc250e022336945ddda0a Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 09:02:20 +0100
Subject: [PATCH 13/32] Improve the simplification of the constant domain.

---
 src/analyses/constant_propagator.cpp | 20 ++++++++++++++++++++
 src/analyses/constant_propagator.h   |  1 +
 2 files changed, 21 insertions(+)

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 66c7ca025e9..78a5275751e 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -334,6 +334,26 @@ void constant_propagator_domaint::assign(
 
 /*******************************************************************\
 
+Function: constant_propagator_domaint::assign
+
+  Inputs: The condition to simplify and its namespace.
+
+ Outputs: The simplified condition.
+
+ Purpose: Simplify the condition given context-sensitive knowledge from the domain.
+
+\*******************************************************************/
+
+exprt constant_propagator_domaint::domain_simplify (const exprt &condition,
+						    const namespacet &ns)
+{
+  exprt e(condition);
+  values.replace_const(e);
+  return simplify_expr(e, ns);
+}
+
+/*******************************************************************\
+
 Function: constant_propagator_domaint::is_array_constant
 
   Inputs:
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 8583ebf0110..7b5fbbce847 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -19,6 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset
   virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
   virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
   bool merge(const constant_propagator_domaint &, locationt, locationt);
+  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns);
 
   struct valuest
   {

From c52d799dc12551653df115896692f362e9acdd1b Mon Sep 17 00:00:00 2001
From: Martin Brain <martin@debian8564>
Date: Fri, 9 Sep 2016 09:16:11 +0100
Subject: [PATCH 14/32] Simplify arguments to function calls.

---
 src/goto-analyzer/static_simplifier.cpp | 31 +++++++++++++++++++++++--
 1 file changed, 29 insertions(+), 2 deletions(-)

diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 831b42535bf..cf8f9338322 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -120,10 +120,11 @@ void static_simplifiert<analyzerT>::simplify_program()
     unsigned assumes;
     unsigned gotos;
     unsigned assigns;
+    unsigned function_calls;
   };
   
-  counters simplified = {0,0,0,0};
-  counters unmodified = {0,0,0,0};
+  counters simplified = {0,0,0,0,0};
+  counters unmodified = {0,0,0,0,0};
 
   Forall_goto_functions(f_it, goto_functions)
   {
@@ -163,6 +164,30 @@ void static_simplifiert<analyzerT>::simplify_program()
 	assign.rhs() = simplified_rhs;
 	i_it->code = assign;
       }
+      else if (i_it->is_function_call())
+      {
+	unsigned result = 0;
+	code_function_callt fcall(to_code_function_call(i_it->code));
+	
+	exprt new_function = domain[i_it].domain_simplify(fcall.function(), ns);
+	result |= (new_function == fcall.function()) ? 0 : 1;
+	fcall.function() = new_function;
+	
+	exprt::operandst &args = fcall.arguments();
+
+	for(exprt::operandst::iterator o_it = args.begin();
+          o_it != args.end(); ++o_it)
+	{
+	  exprt new_arg = domain[i_it].domain_simplify(*o_it, ns);
+	  result |= (new_arg == *o_it) ? 0 : 1;
+	  *o_it = new_arg;
+	}
+
+	i_it->code = fcall;
+	
+	simplified.function_calls += result;
+	unmodified.function_calls += (1 - result);
+      }
     }
   }
   
@@ -175,12 +200,14 @@ void static_simplifiert<analyzerT>::simplify_program()
 	   << ", assume: " << simplified.assumes
 	   << ", goto: " << simplified.gotos
 	   << ", assigns: " << simplified.assigns
+	   << ", function calls: " << simplified.function_calls
 	   << "\n"
 	   << "UNMODIFIED: "
 	   << " assert: " << unmodified.asserts
 	   << ", assume: " << unmodified.assumes
 	   << ", goto: " << unmodified.gotos
 	   << ", assigns: " << unmodified.assigns
+	   << ", function calls: " << unmodified.function_calls
 	   << eom;
 
   return;

From 743c803d1835778e7a7f6d7a0419cd7b74e4b8e8 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 24 Oct 2016 11:51:05 +0100
Subject: [PATCH 15/32] s/sequential/flow-sensitive/ as there are other
 sequential analyses.

---
 src/goto-analyzer/goto_analyzer_parse_options.cpp | 10 +++++-----
 src/goto-analyzer/goto_analyzer_parse_options.h   |  2 +-
 src/goto-analyzer/static_analyzer.cpp             |  2 +-
 src/goto-analyzer/static_show_domain.cpp          |  2 +-
 src/goto-analyzer/static_simplifier.cpp           |  2 +-
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 605cde779e3..c2a6f070c2d 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -277,11 +277,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 
   
   // Abstract interpreter choice
-  options.set_option("sequential", false);
+  options.set_option("flow-sensitive", false);
   options.set_option("concurrent", false);
 
-  if (cmdline.isset("sequential"))
-    options.set_option("sequential", true);
+  if (cmdline.isset("flow-sensitive"))
+    options.set_option("flow-sensitive", true);
   else if (cmdline.isset("concurrent"))
     options.set_option("concurrent", true);
   else
@@ -289,7 +289,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     is_threadedt is_threaded(goto_model.goto_functions);
     bool contains_concurrent_code = is_threaded();
 
-    options.set_option("sequential", !contains_concurrent_code);
+    options.set_option("flow-sensitive", !contains_concurrent_code);
     options.set_option("concurrent",  contains_concurrent_code);
   }
 
@@ -654,7 +654,7 @@ void goto_analyzer_parse_optionst::help()
     " --simplify file_name         run abstract interpreter and simplify program\n"
     "\n"
     "Abstract interpreter options:\n"
-    " --sequential                 use sequential abstract interpreter\n"
+    " --flow-sensitive             use flow-sensitive abstract interpreter\n"
     " --concurrent                 use concurrent abstract interpreter\n"
     "\n"
     "Domain options:\n"
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 8910f760f79..d7685f2c2cd 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -39,7 +39,7 @@ class optionst;
   "(non-null)(show-non-null)" \
   "(constants)" \
   "(show)(verify)(simplify):" \
-  "(sequential)(concurrent)"
+  "(flow-sensitive)(concurrent)"
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,
diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index c82591152d6..b7c7119e0ce 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -252,7 +252,7 @@ bool static_analyzer(
   message_handlert &message_handler,
   std::ostream &out)
 {
-  if (options.get_bool_option("sequential"))
+  if (options.get_bool_option("flow-sensitive"))
   {
     if (options.get_bool_option("constants"))
       return static_analyzert<ait<constant_propagator_domaint> >
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index 5501e8380ca..7873902bfc9 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -38,7 +38,7 @@ bool static_show_domain(
 {
   ai_baset *domain = NULL;
   
-  if (options.get_bool_option("sequential"))
+  if (options.get_bool_option("flow-sensitive"))
   {
     if (options.get_bool_option("constants"))
       domain = new ait<constant_propagator_domaint>();
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index cf8f9338322..e7f7cdf1aa1 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -235,7 +235,7 @@ bool static_simplifier(
   message_handlert &message_handler,
   std::ostream &out)
 {
-  if (options.get_bool_option("sequential"))
+  if (options.get_bool_option("flow-sensitive"))
   {
     if (options.get_bool_option("constants"))
       return static_simplifiert<ait<constant_propagator_domaint> >

From fe7f88b12d213fab15c53736b07ded3da4cc1da5 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 24 Oct 2016 14:15:44 +0100
Subject: [PATCH 16/32] Add an extra argument to domain_simplify so that the
 left hand side of assignment operations is treated differently.

---
 src/analyses/ai.h                       |  3 ++-
 src/analyses/constant_propagator.cpp    | 16 +++++++++++-----
 src/analyses/constant_propagator.h      |  2 +-
 src/analyses/interval_domain.cpp        |  8 +++++++-
 src/analyses/interval_domain.h          |  3 ++-
 src/goto-analyzer/static_simplifier.cpp | 11 +++++++++--
 6 files changed, 32 insertions(+), 11 deletions(-)

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index e9815f1f8ea..5db2e933661 100644
--- a/src/analyses/ai.h
+++ b/src/analyses/ai.h
@@ -103,7 +103,8 @@ class ai_domain_baset
 
   // Used to evaluate or simplify conditions with respect to the domain
   virtual exprt domain_simplify (const exprt &condition,
-				 const namespacet &ns) const {
+				 const namespacet &ns,
+				 const bool lhs = false) const {
     return condition;
   }
 };
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 78a5275751e..df550b167a9 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -334,7 +334,7 @@ void constant_propagator_domaint::assign(
 
 /*******************************************************************\
 
-Function: constant_propagator_domaint::assign
+Function: constant_propagator_domaint::domain_simplify
 
   Inputs: The condition to simplify and its namespace.
 
@@ -345,11 +345,17 @@ Function: constant_propagator_domaint::assign
 \*******************************************************************/
 
 exprt constant_propagator_domaint::domain_simplify (const exprt &condition,
-						    const namespacet &ns)
+						    const namespacet &ns,
+						    const bool lhs)
 {
-  exprt e(condition);
-  values.replace_const(e);
-  return simplify_expr(e, ns);
+  if (lhs) {
+    // For now do not simplify the left hand sides of assignments
+    return condition;
+  } else {
+    exprt e(condition);
+    values.replace_const(e);
+    return simplify_expr(e, ns);
+  }
 }
 
 /*******************************************************************\
diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 7b5fbbce847..4a9e070d2bc 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -19,7 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset
   virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
   virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
   bool merge(const constant_propagator_domaint &, locationt, locationt);
-  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns);
+  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false);
 
   struct valuest
   {
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 6f0b022f3bd..d6b1ac9e6b3 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -514,8 +514,14 @@ Function: interval_domaint::domain_simplify
 \*******************************************************************/
 
 exprt interval_domaint::domain_simplify (const exprt &condition,
-					 const namespacet &ns) const
+					 const namespacet &ns,
+					 const bool lhs) const
 {
+  if (lhs) {
+    // For now do not simplify the left hand side of assignments
+    return condition;
+  }
+  
   interval_domaint d(*this);
   
   //merge intervals to properly handle conjunction
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index 1b7810f0313..2d4bd7f7117 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -82,7 +82,8 @@ class interval_domaint:public ai_domain_baset
   }
   
   virtual exprt domain_simplify (const exprt &condition,
-				 const namespacet &ns) const;
+				 const namespacet &ns,
+				 const bool lhs = false) const;
   
 protected:
   bool bottom;
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index e7f7cdf1aa1..2873c364edf 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -151,9 +151,16 @@ void static_simplifiert<analyzerT>::simplify_program()
       else if (i_it->is_assign())
       {
 	code_assignt assign(to_code_assign(i_it->code));
+
+	/*
+	** Simplification needs to be aware of which side of the
+	** expression it is handling as:
+	**   <i = 0, j = 1>  i = j
+	** should simplify to i = 1, not to 0 = 1.
+	*/
 	
-	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns);
-	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns);
+	exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns, true);
+	exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns, false);
 
 	unsigned result = (simplified_lhs == assign.lhs() &&
 			   simplified_rhs == assign.rhs()) ? 0 : 1;

From 1e5522a775b568bc3a9447587555e54eb1c24384 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 24 Oct 2016 14:31:57 +0100
Subject: [PATCH 17/32] Add a caveat that failures are only assertion failures
 if they are reachable.

---
 src/goto-analyzer/static_analyzer.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index b7c7119e0ce..7d54584f3f1 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -120,7 +120,7 @@ void static_analyzert<analyzerT>::plain_text_report()
       if(simplified.is_true())
         { result() << "SUCCESS"; pass++; }
       else if(simplified.is_false())
-        { result() << "FAILURE"; fail++; }
+        { result() << "FAILURE (if reachable)"; fail++; }
       else
         { result() << "UNKNOWN"; unknown++; }
       result() << eom;
@@ -169,7 +169,7 @@ void static_analyzert<analyzerT>::json_report()
       if(simplified.is_true())
         j["status"]=json_stringt("SUCCESS");
       else if(simplified.is_false())
-        j["status"]=json_stringt("FAILURE");
+        j["status"]=json_stringt("FAILURE (if reachable)");
       else 
         j["status"]=json_stringt("UNKNOWN");
 
@@ -219,7 +219,7 @@ void static_analyzert<analyzerT>::xml_report()
       if(simplified.is_true())
         x.set_attribute("status", "SUCCESS");
       else if(simplified.is_false())
-        x.set_attribute("status", "FAILURE");
+        x.set_attribute("status", "FAILURE (if reachable)");
       else 
         x.set_attribute("status", "UNKNOWN");
 

From 99d945a0d5f33d2592619a54c6ad729e4be918d6 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 24 Oct 2016 15:35:17 +0100
Subject: [PATCH 18/32] Update and check the test cases.  FUTURE for things
 where precision is currently insufficient.

---
 .../constant_propagation_01/test.desc         |  4 +-
 .../constant_propagation_02/original          |  3 +
 .../constant_propagation_02/simplified        | 81 +++++++++++++++++++
 .../constant_propagation_02/test.desc         |  4 +-
 .../constant_propagation_03/test.desc         |  4 +-
 .../constant_propagation_04/test.desc         |  4 +-
 .../constant_propagation_05/test.desc         |  2 +-
 .../constant_propagation_06/test.desc         |  2 +-
 .../constant_propagation_07/test.desc         |  3 +-
 .../constant_propagation_08/test.desc         |  4 +-
 .../constant_propagation_09/test.desc         |  2 +-
 .../constant_propagation_10/test.desc         |  4 +-
 .../constant_propagation_11/test.desc         |  8 +-
 .../constant_propagation_12/test.desc         |  6 +-
 .../constant_propagation_13/test.desc         |  2 +-
 .../constant_propagation_14/test.desc         |  2 +-
 .../constant_propagation_15/test.desc         |  6 +-
 .../constant_propagation_16/test.desc         |  4 +-
 .../constant_propagation_17/test.desc         |  2 +-
 .../constant_propagation_18/test.desc         |  2 +-
 .../goto-analyzer/intervals10/test.desc       |  6 +-
 .../goto-analyzer/intervals11/test.desc       |  2 +-
 .../goto-analyzer/intervals12/intervals12.c   | 16 ++++
 .../goto-analyzer/intervals12/test.desc       |  9 +++
 regression/goto-analyzer/intervals6/test.desc |  4 +-
 regression/goto-analyzer/intervals7/test.desc |  4 +-
 regression/goto-analyzer/intervals8/test.desc |  4 +-
 .../goto-analyzer/intervals9/intervals9.c     |  2 +-
 regression/goto-analyzer/intervals9/test.desc |  2 +-
 29 files changed, 153 insertions(+), 45 deletions(-)
 create mode 100644 regression/goto-analyzer/constant_propagation_02/original
 create mode 100644 regression/goto-analyzer/constant_propagation_02/simplified
 create mode 100644 regression/goto-analyzer/intervals12/intervals12.c
 create mode 100644 regression/goto-analyzer/intervals12/test.desc

diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
index 12178cfec13..7e9cac6056b 100644
--- a/regression/goto-analyzer/constant_propagation_01/test.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ constant_propagation1.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original
new file mode 100644
index 00000000000..13a9e245c81
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_02/original
@@ -0,0 +1,3 @@
+Task defaults to --show
+Domain defaults to --constants
+GOTO-ANALYSER version 5.5 64-bit x86_64 linux
diff --git a/regression/goto-analyzer/constant_propagation_02/simplified b/regression/goto-analyzer/constant_propagation_02/simplified
new file mode 100644
index 00000000000..6c722a607de
--- /dev/null
+++ b/regression/goto-analyzer/constant_propagation_02/simplified
@@ -0,0 +1,81 @@
+Reading GOTO program from `out.goto'
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+main /* main */
+        // 0 file constant_propagation_02.c line 5 function main
+        signed int i;
+        // 1 file constant_propagation_02.c line 5 function main
+        i = 0;
+        // 2 file constant_propagation_02.c line 5 function main
+        signed int j;
+        // 3 file constant_propagation_02.c line 5 function main
+        j = 2;
+        // 4 file constant_propagation_02.c line 7 function main
+        IF FALSE THEN GOTO 1
+        // 5 file constant_propagation_02.c line 9 function main
+        0 = 1;
+        // 6 file constant_propagation_02.c line 10 function main
+        2 = 3;
+        // 7 no location
+     1: SKIP
+        // 8 file constant_propagation_02.c line 12 function main
+        ASSERT FALSE // assertion j!=3
+        // 9 file constant_propagation_02.c line 12 function main
+        GOTO 2
+        // 10 file constant_propagation_02.c line 12 function main
+        (void)0;
+        // 11 no location
+     2: SKIP
+        // 12 file constant_propagation_02.c line 13 function main
+        dead j;
+        // 13 file constant_propagation_02.c line 13 function main
+        dead i;
+        // 14 file constant_propagation_02.c line 13 function main
+        main#return_value = NONDET(signed int);
+        // 15 file constant_propagation_02.c line 13 function main
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+_start /* _start */
+        // 16 no location
+        __CPROVER_initialize();
+        // 17 file constant_propagation_02.c line 3
+        main();
+        // 18 file constant_propagation_02.c line 3
+        return' = main#return_value;
+        // 19 file constant_propagation_02.c line 3
+        dead main#return_value;
+        // 20 file constant_propagation_02.c line 3
+        OUTPUT("return", return');
+        // 21 no location
+        END_FUNCTION
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+__CPROVER_initialize /* __CPROVER_initialize */
+        // 22 no location
+        // Labels: __CPROVER_HIDE
+        SKIP
+        // 23 file <built-in-additions> line 39
+        __CPROVER_dead_object = NULL;
+        // 24 file <built-in-additions> line 38
+        __CPROVER_deallocated = NULL;
+        // 25 file <built-in-additions> line 42
+        __CPROVER_malloc_is_new_array = FALSE;
+        // 26 file <built-in-additions> line 40
+        __CPROVER_malloc_object = NULL;
+        // 27 file <built-in-additions> line 41
+        __CPROVER_malloc_size = 0ul;
+        // 28 file <built-in-additions> line 43
+        __CPROVER_memory_leak = NULL;
+        // 29 file <built-in-additions> line 31
+        __CPROVER_next_thread_id = 0ul;
+        // 30 file <built-in-additions> line 85
+        __CPROVER_pipe_count = 0u;
+        // 31 file <built-in-additions> line 65
+        __CPROVER_rounding_mode = 0;
+        // 32 file <built-in-additions> line 29
+        __CPROVER_thread_id = 0ul;
+        // 33 file <built-in-additions> line 30
+        __CPROVER_threads_exited = ARRAY_OF(FALSE);
+        // 34 no location
+        END_FUNCTION
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
index 4e24ea57c68..635f7dcf620 100644
--- a/regression/goto-analyzer/constant_propagation_02/test.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ constant_propagation_02.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
index 9134ef9cfa8..37962658987 100644
--- a/regression/goto-analyzer/constant_propagation_03/test.desc
+++ b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ constant_propagation_03.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
index 2e27a8ec3e5..2b23ac224f7 100644
--- a/regression/goto-analyzer/constant_propagation_04/test.desc
+++ b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ constant_propagation_04.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc
index 4c196b063af..84712b085da 100644
--- a/regression/goto-analyzer/constant_propagation_05/test.desc
+++ b/regression/goto-analyzer/constant_propagation_05/test.desc
@@ -3,6 +3,6 @@ constant_propagation_05.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE$
+^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc
index b914152e5a7..db151228d5c 100644
--- a/regression/goto-analyzer/constant_propagation_06/test.desc
+++ b/regression/goto-analyzer/constant_propagation_06/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_06.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
index 5e6bbfc32cc..7494eafcd54 100644
--- a/regression/goto-analyzer/constant_propagation_07/test.desc
+++ b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,6 @@ constant_propagation_07.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<50: UNKNOWN$
-^\[main.assertion.2\] file constant_propagation_07.c line 13 function main, assertion i<51: SUCCESS$
+^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc
index 131ed1c001b..994c2c532df 100644
--- a/regression/goto-analyzer/constant_propagation_08/test.desc
+++ b/regression/goto-analyzer/constant_propagation_08/test.desc
@@ -1,6 +1,6 @@
-CORE
+FUTURE
 constant_propagation_08.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc
index 562916fc138..8cb0ec6a003 100644
--- a/regression/goto-analyzer/constant_propagation_09/test.desc
+++ b/regression/goto-analyzer/constant_propagation_09/test.desc
@@ -1,6 +1,6 @@
 CORE
 constant_propagation_09.c
---constants --intervals --verify
+--intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ******** Function main
diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc
index bb3a4fa51fe..7b78521a13d 100644
--- a/regression/goto-analyzer/constant_propagation_10/test.desc
+++ b/regression/goto-analyzer/constant_propagation_10/test.desc
@@ -3,7 +3,7 @@ constant_propagation_10.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
index bb3a4fa51fe..7c849326cf6 100644
--- a/regression/goto-analyzer/constant_propagation_11/test.desc
+++ b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -1,9 +1,9 @@
-CORE
-constant_propagation_10.c
+FUTURE
+constant_propagation_11.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
index ddec139e1d7..ca5803363ad 100644
--- a/regression/goto-analyzer/constant_propagation_12/test.desc
+++ b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -1,9 +1,9 @@
-CORE
+FUTURE
 constant_propagation_12.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc
index 4c526d75784..22f10d125e3 100644
--- a/regression/goto-analyzer/constant_propagation_13/test.desc
+++ b/regression/goto-analyzer/constant_propagation_13/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_13.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc
index cdd022e1396..a39a1f66cda 100644
--- a/regression/goto-analyzer/constant_propagation_14/test.desc
+++ b/regression/goto-analyzer/constant_propagation_14/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_14.c
 --constants --simplify out.goto
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc
index d2b49a78162..20d36183eb0 100644
--- a/regression/goto-analyzer/constant_propagation_15/test.desc
+++ b/regression/goto-analyzer/constant_propagation_15/test.desc
@@ -1,9 +1,9 @@
-CORE
+FUTURE
 constant_propagation_15.c
 --constants --simplify out.goto
 ^EXIT=0$
 ^SIGNAL=0$
-^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
-^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
+^UNMODIFIED:  assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc
index 3157d7a1f56..b56c871deb4 100644
--- a/regression/goto-analyzer/constant_propagation_16/test.desc
+++ b/regression/goto-analyzer/constant_propagation_16/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 constant_propagation_16.c
 --constants --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE$
+^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc
index 397848b6430..acecb91eb0a 100644
--- a/regression/goto-analyzer/constant_propagation_17/test.desc
+++ b/regression/goto-analyzer/constant_propagation_17/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_17.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc
index 8e7133092b4..7ea74c4d264 100644
--- a/regression/goto-analyzer/constant_propagation_18/test.desc
+++ b/regression/goto-analyzer/constant_propagation_18/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 constant_propagation_18.c
 --constants --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc
index f2296d2a6b7..794198505f1 100644
--- a/regression/goto-analyzer/intervals10/test.desc
+++ b/regression/goto-analyzer/intervals10/test.desc
@@ -1,12 +1,12 @@
-CORE
+FUTURE
 intervals10.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$
 ^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$
-^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: UNKNOWN$
+^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: FAILURE (if reachable)$
 ^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$
-^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: UNKNOWN$
+^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc
index eb2cd73a6df..039cbffbeb0 100644
--- a/regression/goto-analyzer/intervals11/test.desc
+++ b/regression/goto-analyzer/intervals11/test.desc
@@ -1,4 +1,4 @@
-CORE
+FUTURE
 intervals11.c
 --intervals --verify
 ^EXIT=0$
diff --git a/regression/goto-analyzer/intervals12/intervals12.c b/regression/goto-analyzer/intervals12/intervals12.c
new file mode 100644
index 00000000000..15d865adf80
--- /dev/null
+++ b/regression/goto-analyzer/intervals12/intervals12.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main (void) {
+  int i;
+  int j;
+
+  if (i <= 0 && j < i)
+    assert(j < 0);
+
+  if (j < i && i <= 0)
+    assert(j < 0);
+
+  return 0;
+}
+
+
diff --git a/regression/goto-analyzer/intervals12/test.desc b/regression/goto-analyzer/intervals12/test.desc
new file mode 100644
index 00000000000..59a724c28b5
--- /dev/null
+++ b/regression/goto-analyzer/intervals12/test.desc
@@ -0,0 +1,9 @@
+FUTURE
+intervals12.c
+--intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^[main.assertion.1] file intervals12.c line 8 function main, assertion j < 0: SUCCESS$
+^[main.assertion.2] file intervals12.c line 11 function main, assertion j < 0: SUCCESS$
+--
+^warning: ignoring
diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc
index ae01b92499a..6e36b7948d2 100644
--- a/regression/goto-analyzer/intervals6/test.desc
+++ b/regression/goto-analyzer/intervals6/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals6.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$
+^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc
index 4d8619cfacb..6a42b4a30ec 100644
--- a/regression/goto-analyzer/intervals7/test.desc
+++ b/regression/goto-analyzer/intervals7/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals7.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$
+^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc
index 8d1f7817ab6..7500059a717 100644
--- a/regression/goto-analyzer/intervals8/test.desc
+++ b/regression/goto-analyzer/intervals8/test.desc
@@ -1,8 +1,8 @@
-CORE
+FUTURE
 intervals8.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: UNKNOWN$
+^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals9/intervals9.c
index e9bc51f30b5..27739c7aa28 100644
--- a/regression/goto-analyzer/intervals9/intervals9.c
+++ b/regression/goto-analyzer/intervals9/intervals9.c
@@ -1,4 +1,4 @@
-//#include <assert.h>
+#include <assert.h>
 
 int main()
 {
diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc
index c6fec9c4c6d..33f92abcdb2 100644
--- a/regression/goto-analyzer/intervals9/test.desc
+++ b/regression/goto-analyzer/intervals9/test.desc
@@ -3,6 +3,6 @@ intervals9.c
 --intervals --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
+^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$
 --
 ^warning: ignoring

From 4f1a859de6284201f97b2becd84563e6b4a781ac Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 27 Oct 2016 11:54:08 +0100
Subject: [PATCH 19/32] Fix an ambiguity in method overloading.

---
 src/analyses/ai.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 5fa5974ea2e..272c271416d 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -179,7 +179,7 @@ xmlt ai_baset::output_xml(
   {
     xmlt function("function");
     function.set_attribute("name", as_string(f_it->first));
-    function.set_attribute("body_available", f_it->second.body_available());
+    function.set_attribute("body_available", f_it->second.body_available() ? "true" : "false");
     
     if(f_it->second.body_available())
     {

From e829f9a0ae3d8122b1c2c4603889555dd308c7f4 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 27 Oct 2016 11:54:56 +0100
Subject: [PATCH 20/32] Improve error reporting for unsupported combinations of
 task / interpreter / domain.

---
 src/goto-analyzer/static_analyzer.cpp    | 12 +++++++++---
 src/goto-analyzer/static_show_domain.cpp |  4 ++++
 src/goto-analyzer/static_simplifier.cpp  | 11 ++++++++---
 3 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index 7d54584f3f1..c8e6c0a4ca0 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -267,7 +267,7 @@ bool static_analyzer(
     //    (goto_model, options, message_handler, out)();
     
     else
-      return true;
+      goto fail;
   }
   else if (options.get_bool_option("concurrent"))
   {
@@ -287,8 +287,14 @@ bool static_analyzer(
     
     else
 #endif
-      return true;
+      goto fail;
   }
   else
-    return true;
+    goto fail;
+
+  
+ fail :
+  messaget m(message_handler);
+  m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom;
+  return true;
 }
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index 7873902bfc9..e0b874ff844 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -66,7 +66,11 @@ bool static_show_domain(
   }
 
   if (domain == NULL)
+  {
+    messaget m(message_handler);
+    m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom;
     return true;
+  }
 
   //status() << "performing analysis" << eom;
   (*domain)(goto_model);
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 2873c364edf..f183965f4e9 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -257,7 +257,7 @@ bool static_simplifier(
     //    (goto_model, options, message_handler, out)();
     
     else
-      return true;
+      goto fail;
   }
   else if (options.get_bool_option("concurrent"))
   {
@@ -277,8 +277,13 @@ bool static_simplifier(
     
     else
 #endif
-      return true;
+      goto fail;
   }
   else
-    return true;
+    goto fail;
+
+ fail :
+  messaget m(message_handler);
+  m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom;
+  return true;
 }

From 05769c43b41725a49005b69908015f7dcf389d97 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Tue, 1 Nov 2016 11:01:59 +0000
Subject: [PATCH 21/32] Add output_json to the dependence_graph abstract
 domain.

---
 src/analyses/dependence_graph.cpp | 46 +++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 44bcf2211eb..f237a97cb19 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -11,6 +11,8 @@ Date: August 2013
 
 #include <cassert>
 
+#include <util/json.h>
+
 #include "goto_rw.h"
 
 #include "dependence_graph.h"
@@ -351,6 +353,50 @@ void dep_graph_domaint::output(
   }
 }
 
+/*******************************************************************\
+
+Function: dep_graph_domaint::output_json
+
+  Inputs: The abstract interpreter and the namespace.
+
+ Outputs: The domain, formatted as a JSON object.
+
+ Purpose: Outputs the current value of the domain.
+
+\*******************************************************************/
+
+
+jsont dep_graph_domaint::output_json(
+    const ai_baset &ai,
+    const namespacet &ns) const
+{
+  json_arrayt graph;
+  
+  for(dep_graph_domaint::depst::const_iterator cdi=control_deps.begin();
+      cdi!=control_deps.end();
+      ++cdi)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["location_number"] = json_numbert(std::to_string((*cdi)->location_number));
+    link["source_location"] = json_stringt((*cdi)->source_location.as_string());
+    link["type"]=json_stringt("control");
+  }
+
+  for(dep_graph_domaint::depst::const_iterator ddi=data_deps.begin();
+      ddi!=data_deps.end();
+      ++ddi)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["location_number"] = json_numbert(std::to_string((*ddi)->location_number));
+    link["source_location"] = json_stringt((*ddi)->source_location.as_string());
+    link["type"]=json_stringt("data");
+  }
+
+  return graph;
+}
+
+
+
 /*******************************************************************\
 
 Function: dependence_grapht::add_dep

From 499d911cdc4da4b578de9217e67e3316e6c257b9 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Tue, 1 Nov 2016 11:02:48 +0000
Subject: [PATCH 22/32] ... and the header file ...

---
 src/analyses/dependence_graph.h | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h
index 1b07b4ec140..c0d255ea662 100644
--- a/src/analyses/dependence_graph.h
+++ b/src/analyses/dependence_graph.h
@@ -43,6 +43,10 @@ class dep_graph_domaint:public ai_domain_baset
       const ai_baset &ai,
       const namespacet &ns) const;
 
+  virtual jsont output_json(
+    const ai_baset &ai,
+    const namespacet &ns) const;
+
   void set_node_id(unsigned id)
   {
     node_id=id;

From db28f6e38f887cf9cd6aca12d481642b443ba7e1 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Tue, 1 Nov 2016 11:04:54 +0000
Subject: [PATCH 23/32] Add support for generating the dependency graph to
 goto-analyze, including dot format.

---
 src/goto-analyzer/goto_analyzer_parse_options.cpp | 14 +++++++++++++-
 src/goto-analyzer/goto_analyzer_parse_options.h   |  5 +++--
 src/goto-analyzer/static_show_domain.cpp          | 15 ++++++++++++++-
 3 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index c2a6f070c2d..48e5aad0a73 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -227,6 +227,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("text", false);
   options.set_option("json", false);
   options.set_option("xml", false);
+  options.set_option("dot", false);
   options.set_option("outfile", "-");
   
   if (cmdline.isset("text"))
@@ -244,6 +245,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("xml", true);
     options.set_option("outfile", cmdline.get_value("xml"));
   }
+  else if (cmdline.isset("dot"))
+  {
+    options.set_option("dot", true);
+    options.set_option("outfile", cmdline.get_value("dot"));
+  }
   else
   {
     options.set_option("text", true);
@@ -298,6 +304,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("constants", false);
   options.set_option("intervals", false);
   options.set_option("non-null", false);
+  options.set_option("dependence-graph", false);
 
   if (cmdline.isset("intervals") ||
       cmdline.isset("show-intervals")) 
@@ -307,10 +314,13 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("non-null", true);
   else if (cmdline.isset("constants"))
     options.set_option("constants", true);
+  else if (cmdline.isset("dependence-graph"))
+    options.set_option("dependence-graph", true);
     
   if (!(options.get_bool_option("constants")  ||
 	options.get_bool_option("intervals")  ||
-	options.get_bool_option("non-null")))
+	options.get_bool_option("non-null") ||
+	options.get_bool_option("dependence-graph")))
   {
     status() << "Domain defaults to --constants" << eom;
     options.set_option("constants", true);
@@ -661,11 +671,13 @@ void goto_analyzer_parse_optionst::help()
     " --constants                  constant abstraction\n"
     " --intervals                  interval abstraction\n"
     " --non-null                   non-null abstraction\n"
+    " --dependence-graph           dependency relation between instructions\n"
     "\n"
     "Output options:\n"
     " --text file_name             output results in plain text to given file\n"
     " --json file_name             output results in JSON format to given file\n"
     " --xml file_name              output results in XML format to given file\n"
+    " --dot file_name              output results in DOT format to given file\n"
     "\n"
     "Other analyses:\n"
     " --taint file_name            perform taint analysis using rules in given file\n"
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index d7685f2c2cd..c379cb180ce 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -33,12 +33,13 @@ class optionst;
   "(gcc)(arch):" \
   "(taint):(show-taint)" \
   "(show-local-may-alias)" \
-  "(json):(xml):(text):" \
+  "(json):(xml):(text):(dot):" \
   "(unreachable-instructions)" \
   "(intervals)(show-intervals)" \
   "(non-null)(show-non-null)" \
   "(constants)" \
-  "(show)(verify)(simplify):" \
+  "(dependence-graph)" \
+  "(show)(verify)(simplify):"			\
   "(flow-sensitive)(concurrent)"
 
 class goto_analyzer_parse_optionst:
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index e0b874ff844..d892af68a56 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -14,6 +14,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
+#include <analyses/dependence_graph.h>
 
 #include "static_show_domain.h"
 
@@ -37,6 +38,7 @@ bool static_show_domain(
   std::ostream &out)
 {
   ai_baset *domain = NULL;
+  namespacet ns(goto_model.symbol_table);
   
   if (options.get_bool_option("flow-sensitive"))
   {
@@ -48,7 +50,10 @@ bool static_show_domain(
     
     //else if (options.get_bool_option("non-null"))
     //  domain = new ait<non_null_domaint>();
-    
+
+    else if (options.get_bool_option("dependence-graph"))
+      domain = new dependence_grapht(ns);
+
   }
   else if (options.get_bool_option("concurrent"))
   {
@@ -75,10 +80,18 @@ bool static_show_domain(
   //status() << "performing analysis" << eom;
   (*domain)(goto_model);
 
+
   if(options.get_bool_option("json"))
     out << domain->output_json(goto_model);
   else if(options.get_bool_option("xml"))
     out << domain->output_xml(goto_model);
+  else if(options.get_bool_option("dot") && options.get_bool_option("dependence-graph"))
+  {
+    dependence_grapht *d = dynamic_cast<dependence_grapht*>(domain);
+    assert(d != NULL);
+
+    d->output_dot(out);
+  }
   else
     domain->output(goto_model, out);
 

From 94938ca7f52014bb0547c1f11a63c47ac01c7889 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Tue, 1 Nov 2016 12:46:10 +0000
Subject: [PATCH 24/32] Dot output needs to be in a graph.

---
 src/goto-analyzer/static_show_domain.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index d892af68a56..4bec57b61b4 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -90,7 +90,9 @@ bool static_show_domain(
     dependence_grapht *d = dynamic_cast<dependence_grapht*>(domain);
     assert(d != NULL);
 
+    out << "digraph g {\n";
     d->output_dot(out);
+    out << "}\n";
   }
   else
     domain->output(goto_model, out);

From f17ccbbe7a91afc3ea425f4b1ee0bc6689d4ccab Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 14 Nov 2016 17:32:16 +0000
Subject: [PATCH 25/32] Fix a travis build failure.

---
 src/analyses/constant_propagator.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
index 4a9e070d2bc..a8540906914 100644
--- a/src/analyses/constant_propagator.h
+++ b/src/analyses/constant_propagator.h
@@ -19,7 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset
   virtual void transform(locationt, locationt, ai_baset &, const namespacet &);
   virtual void output(std::ostream &, const ai_baset &, const namespacet &) const;
   bool merge(const constant_propagator_domaint &, locationt, locationt);
-  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false);
+  virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false) const;
 
   struct valuest
   {

From 564a2ed8582b9a634600dd1c7afc2b3a61e9821b Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 14 Nov 2016 18:11:02 +0000
Subject: [PATCH 26/32] Finish fixing the travis issue.

---
 src/analyses/constant_propagator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index df550b167a9..921d0458b9d 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -346,7 +346,7 @@ Function: constant_propagator_domaint::domain_simplify
 
 exprt constant_propagator_domaint::domain_simplify (const exprt &condition,
 						    const namespacet &ns,
-						    const bool lhs)
+						    const bool lhs) const
 {
   if (lhs) {
     // For now do not simplify the left hand sides of assignments

From 699dde8826ba7aa6238f7a51c564da1147b0a235 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 14 Nov 2016 18:51:05 +0000
Subject: [PATCH 27/32] Improve handling of exceptions.

---
 .../goto_analyzer_parse_options.cpp           | 257 ++++++++++--------
 1 file changed, 142 insertions(+), 115 deletions(-)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 48e5aad0a73..bfd86288148 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -342,152 +342,179 @@ Function: goto_analyzer_parse_optionst::doit
 
 int goto_analyzer_parse_optionst::doit()
 {
-  if(cmdline.isset("version"))
-  {
-    std::cout << CBMC_VERSION << std::endl;
-    return 0;
-  }
-  
-  //
-  // command line options
-  //
-
-  optionst options;
-  get_command_line_options(options);
-  eval_verbosity();
-
-  //
-  // Print a banner
-  //
-  status() << "GOTO-ANALYSER version " CBMC_VERSION " "
-           << sizeof(void *)*8 << "-bit "
-           << config.this_architecture() << " "
-           << config.this_operating_system() << eom;
-
-  register_languages();
+  try
+  {  
+    
+    if(cmdline.isset("version"))
+    {
+	std::cout << CBMC_VERSION << std::endl;
+	return 0;
+    }
   
-  goto_model.set_message_handler(get_message_handler());
-
-  if(goto_model(cmdline.args))
-    return 6;
+    //
+    // command line options
+    //
     
-  if(process_goto_program(options))
-    return 6;
-
-  if(cmdline.isset("taint"))
-  {
-    std::string taint_file=cmdline.get_value("taint");
+    optionst options;
+    get_command_line_options(options);
+    eval_verbosity();
+    
+    //
+    // Print a banner
+    //
+    status() << "GOTO-ANALYSER version " CBMC_VERSION " "
+	     << sizeof(void *)*8 << "-bit "
+	     << config.this_architecture() << " "
+	     << config.this_operating_system() << eom;
+    
+    register_languages();
+    
+    goto_model.set_message_handler(get_message_handler());
+    
+    if(goto_model(cmdline.args))
+      return 6;
+    
+    if(process_goto_program(options))
+      return 6;
 
-    if(cmdline.isset("show-taint"))
+    if(cmdline.isset("taint"))
     {
-      taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
-      return 0;
+      std::string taint_file=cmdline.get_value("taint");
+
+      if(cmdline.isset("show-taint"))
+      {
+	taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
+	return 0;
+      }
+      else
+      {
+	std::string json_file=cmdline.get_value("json");
+	bool result=
+	  taint_analysis(goto_model, taint_file, get_message_handler(), false, json_file);
+	return result?10:0;
+      }
     }
-    else
+
+    if(cmdline.isset("unreachable-instructions"))
     {
-      std::string json_file=cmdline.get_value("json");
-      bool result=
-        taint_analysis(goto_model, taint_file, get_message_handler(), false, json_file);
-      return result?10:0;
-    }
-  }
+      const std::string json_file=cmdline.get_value("json");
 
-  if(cmdline.isset("unreachable-instructions"))
-  {
-    const std::string json_file=cmdline.get_value("json");
+      if(json_file.empty())
+	unreachable_instructions(goto_model, false, std::cout);
+      else if(json_file=="-")
+	unreachable_instructions(goto_model, true, std::cout);
+      else
+      {
+	std::ofstream ofs(json_file);
+	if(!ofs)
+	{
+	  error() << "Failed to open json output `"
+		  << json_file << "'" << eom;
+	  return 6;
+	}
+	
+	unreachable_instructions(goto_model, true, ofs);
+      }
 
-    if(json_file.empty())
-      unreachable_instructions(goto_model, false, std::cout);
-    else if(json_file=="-")
-      unreachable_instructions(goto_model, true, std::cout);
-    else
+      return 0;
+    }
+
+    if(cmdline.isset("show-local-may-alias"))
     {
-      std::ofstream ofs(json_file);
-      if(!ofs)
+      namespacet ns(goto_model.symbol_table);
+  
+      forall_goto_functions(it, goto_model.goto_functions)
       {
-        error() << "Failed to open json output `"
-                << json_file << "'" << eom;
-        return 6;
+	std::cout << ">>>>\n";
+	std::cout << ">>>> " << it->first << '\n';
+	std::cout << ">>>>\n";
+	local_may_aliast local_may_alias(it->second);
+	local_may_alias.output(std::cout, it->second, ns);
+	std::cout << '\n';
       }
 
-      unreachable_instructions(goto_model, true, ofs);
+      return 0;
     }
 
-    return 0;
-  }
+    label_properties(goto_model);
 
-  if(cmdline.isset("show-local-may-alias"))
-  {
-    namespacet ns(goto_model.symbol_table);
-  
-    forall_goto_functions(it, goto_model.goto_functions)
+    if(cmdline.isset("show-properties"))
     {
-      std::cout << ">>>>\n";
-      std::cout << ">>>> " << it->first << '\n';
-      std::cout << ">>>>\n";
-      local_may_aliast local_may_alias(it->second);
-      local_may_alias.output(std::cout, it->second, ns);
-      std::cout << '\n';
+      show_properties(goto_model, get_ui());
+      return 0;
     }
 
-    return 0;
-  }
-
-  label_properties(goto_model);
-
-  if(cmdline.isset("show-properties"))
-  {
-    show_properties(goto_model, get_ui());
-    return 0;
-  }
-
-  if(set_properties())
-    return 7;
+    if(set_properties())
+      return 7;
   
-
-  // Output file factory
-  std::ostream *out;
-  const std::string outfile = options.get_option("outfile");
-  if (outfile == "-")
-    out = &std::cout;
-  else
-  {
-    out = new std::ofstream(outfile);
-    if(!*out)
+    
+    // Output file factory
+    std::ostream *out;
+    const std::string outfile = options.get_option("outfile");
+    if (outfile == "-")
+      out = &std::cout;
+    else
     {
-      error() << "Failed to open output file `"
-	      << outfile << "'" << eom;
-      return 6;
+      out = new std::ofstream(outfile);
+      if(!*out)
+      {
+	error() << "Failed to open output file `"
+		<< outfile << "'" << eom;
+	return 6;
+      }
     }
-  }
-
 
-  // Run the analysis
-  bool result = true;
-  if (options.get_bool_option("show"))
-    result = static_show_domain(goto_model, options, get_message_handler(), *out);
 
-  else if (options.get_bool_option("verify"))
-    result =    static_analyzer(goto_model, options, get_message_handler(), *out);
-
-  else if (options.get_bool_option("simplify"))
-    result =  static_simplifier(goto_model, options, get_message_handler(), *out);
-  else
-  {
-    error() << "No task given" << eom;
-    return 6;
-  }
+    // Run the analysis
+    bool result = true;
+    if (options.get_bool_option("show"))
+      result = static_show_domain(goto_model, options, get_message_handler(), *out);
+    
+    else if (options.get_bool_option("verify"))
+      result =    static_analyzer(goto_model, options, get_message_handler(), *out);
+    
+    else if (options.get_bool_option("simplify"))
+      result =  static_simplifier(goto_model, options, get_message_handler(), *out);
+    else
+    {
+      error() << "No task given" << eom;
+      return 6;
+    }
   
-  if (out != &std::cout)
-    delete out;
+    if (out != &std::cout)
+      delete out;
   
   return result?10:0;
-
   
   // Final defensive error case
   error() << "no analysis option given -- consider reading --help"
           << eom;
   return 6;
+  
+  }
+  catch(const char *e)
+  {
+    error() << e << eom;
+    return 6;
+  }
+
+  catch(const std::string e)
+  {
+    error() << e << eom;
+    return 6;
+  }
+  
+  catch(int x)
+  {
+    return x;
+  }
+  
+  catch(std::bad_alloc)
+  {
+    error() << "Out of memory" << eom;
+    return 6;
+  }
+
 }
 
 /*******************************************************************\

From 966f8230429b1c9ef9698aca21592f397d32b4bc Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Mon, 14 Nov 2016 18:52:28 +0000
Subject: [PATCH 28/32] Implement feature request for simpler JSON output.

---
 src/analyses/ai.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 272c271416d..721ed0de1fe 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -110,7 +110,7 @@ jsont ai_baset::output_json(
     {
       result[as_string(f_it->first)] = output_json(ns, f_it->second.body, f_it->first);
     } else {
-      result[as_string(f_it->first)] = json_stringt("no body");
+      result[as_string(f_it->first)] = json_arrayt();
     }
   }
 

From 96c27b7b0e5aff1180f6cc28de98a5b8d0a938d5 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 17 Nov 2016 08:28:34 +0000
Subject: [PATCH 29/32] Add support for reachability slicing after
 simplification; disabled for now.

---
 src/goto-analyzer/Makefile                        |  3 ++-
 src/goto-analyzer/goto_analyzer_parse_options.cpp |  4 ++++
 src/goto-analyzer/goto_analyzer_parse_options.h   |  5 +++--
 src/goto-analyzer/static_simplifier.cpp           | 11 +++++++++++
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index 7d27be382e4..3e6f53b6792 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -13,7 +13,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../util/util$(LIBEXT)
+      ../util/util$(LIBEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
 
 INCLUDES= -I ..
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index bfd86288148..f1d93afe398 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -281,6 +281,10 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show", true);
   }
 
+  // For development allow slicing to be disabled in the simplify task
+  options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
+  options.set_option("simplify-slicing", false); // Disable for now
+
   
   // Abstract interpreter choice
   options.set_option("flow-sensitive", false);
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index c379cb180ce..34d04be182f 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -39,8 +39,9 @@ class optionst;
   "(non-null)(show-non-null)" \
   "(constants)" \
   "(dependence-graph)" \
-  "(show)(verify)(simplify):"			\
-  "(flow-sensitive)(concurrent)"
+  "(show)(verify)(simplify):" \
+  "(flow-sensitive)(concurrent)" \
+  "(no-simplify-slicing)"
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index f183965f4e9..90b03e324ca 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
 
+#include <goto-instrument/reachability_slicer.h>
+
 #include "static_simplifier.h"
 
 template <class analyzerT>
@@ -74,6 +76,15 @@ bool static_simplifiert<analyzerT>::operator()(void)
   status() << "simplifying program" << eom;
   simplify_program();
 
+  // Remove obviously unreachable things and (now) unconditional branches
+  if (options.get_bool_option("simplify-slicing"))
+  {
+    status() << "Performing a reachability slice" << eom;
+    reachability_slicer(goto_functions);
+
+    goto_functions.update();
+  }
+
   status() << "writing goto binary" << eom;
   return write_goto_binary(out, ns.get_symbol_table(), goto_functions);
 }

From 22a3ce384319a282b1d4e79228e16096727c47ad Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 17 Nov 2016 16:54:11 +0000
Subject: [PATCH 30/32] Add a utility function for removing unreachable
 instructions from all goto_programs.

---
 src/goto-programs/remove_unreachable.cpp | 6 ++++++
 src/goto-programs/remove_unreachable.h   | 1 +
 2 files changed, 7 insertions(+)

diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp
index 9f36259c83e..d9bee26e1ec 100644
--- a/src/goto-programs/remove_unreachable.cpp
+++ b/src/goto-programs/remove_unreachable.cpp
@@ -61,3 +61,9 @@ void remove_unreachable(goto_programt &goto_program)
   }
 }
 
+void remove_unreachable(goto_functionst &goto_functions)
+{
+  Forall_goto_functions(f_it, goto_functions)
+    remove_unreachable(f_it->second.body);
+}
+
diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h
index c40b0ded93f..603f7db8808 100644
--- a/src/goto-programs/remove_unreachable.h
+++ b/src/goto-programs/remove_unreachable.h
@@ -12,5 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_functions.h"
 
 void remove_unreachable(goto_programt &goto_program);
+void remove_unreachable(goto_functionst &goto_functions);
 
 #endif

From dc033826ea9c0ed77fbdd03e7760a8847aa8e531 Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 17 Nov 2016 17:13:13 +0000
Subject: [PATCH 31/32] An alternative approach to slicing unreachable
 instructions.

---
 src/goto-analyzer/Makefile                        |  3 +--
 src/goto-analyzer/goto_analyzer_parse_options.cpp |  1 -
 src/goto-analyzer/static_simplifier.cpp           | 13 ++++++++++---
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
index 3e6f53b6792..7d27be382e4 100644
--- a/src/goto-analyzer/Makefile
+++ b/src/goto-analyzer/Makefile
@@ -13,8 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
-      ../util/util$(LIBEXT) \
-      ../goto-instrument/reachability_slicer$(OBJEXT) \
+      ../util/util$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index f1d93afe398..82ca1992c0e 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -283,7 +283,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 
   // For development allow slicing to be disabled in the simplify task
   options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
-  options.set_option("simplify-slicing", false); // Disable for now
 
   
   // Abstract interpreter choice
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 90b03e324ca..9abbc4ce4a4 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -19,7 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
 
-#include <goto-instrument/reachability_slicer.h>
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unreachable.h>
 
 #include "static_simplifier.h"
 
@@ -79,9 +80,15 @@ bool static_simplifiert<analyzerT>::operator()(void)
   // Remove obviously unreachable things and (now) unconditional branches
   if (options.get_bool_option("simplify-slicing"))
   {
-    status() << "Performing a reachability slice" << eom;
-    reachability_slicer(goto_functions);
+    status() << "Removing unreachable instructions" << eom;
 
+    remove_skip(goto_functions);  // Remove goto false
+    goto_functions.update();
+
+    remove_unreachable(goto_functions);  // Unconvert unreachable to skips
+    goto_functions.update();
+
+    remove_skip(goto_functions);  // Remove all of the new skips
     goto_functions.update();
   }
 

From 34a02686f079add59a7d73308d1c710a2f1b2ccd Mon Sep 17 00:00:00 2001
From: martin <martin@raphael>
Date: Thu, 17 Nov 2016 17:15:54 +0000
Subject: [PATCH 32/32] Consistent capitalisation of status messages.

---
 src/goto-analyzer/static_analyzer.cpp    | 2 +-
 src/goto-analyzer/static_show_domain.cpp | 2 +-
 src/goto-analyzer/static_simplifier.cpp  | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp
index c8e6c0a4ca0..ce43c624952 100644
--- a/src/goto-analyzer/static_analyzer.cpp
+++ b/src/goto-analyzer/static_analyzer.cpp
@@ -64,7 +64,7 @@ Function: static_analyzert<analyzerT>::operator()
 template <class analyzerT>
 bool static_analyzert<analyzerT>::operator()()
 {
-  status() << "performing analysis" << eom;
+  status() << "Performing analysis" << eom;
   domain(goto_functions, ns);
 
   
diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp
index 4bec57b61b4..df519f054cf 100644
--- a/src/goto-analyzer/static_show_domain.cpp
+++ b/src/goto-analyzer/static_show_domain.cpp
@@ -77,7 +77,7 @@ bool static_show_domain(
     return true;
   }
 
-  //status() << "performing analysis" << eom;
+  //status() << "Performing analysis" << eom;
   (*domain)(goto_model);
 
 
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 9abbc4ce4a4..093d5ddf985 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -71,10 +71,10 @@ Function: static_simplifiert<analyzerT>::operator()
 template <class analyzerT>
 bool static_simplifiert<analyzerT>::operator()(void)
 {
-  status() << "performing analysis" << eom;
+  status() << "Performing analysis" << eom;
   domain(goto_functions, ns);
 
-  status() << "simplifying program" << eom;
+  status() << "Simplifying program" << eom;
   simplify_program();
 
   // Remove obviously unreachable things and (now) unconditional branches
@@ -92,7 +92,7 @@ bool static_simplifiert<analyzerT>::operator()(void)
     goto_functions.update();
   }
 
-  status() << "writing goto binary" << eom;
+  status() << "Writing goto binary" << eom;
   return write_goto_binary(out, ns.get_symbol_table(), goto_functions);
 }