From 1f0e11f10b6390ed6a2e07ad7e29324af48ff0b2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Sat, 7 Jan 2017 00:52:46 +0000
Subject: [PATCH 01/33] expr2ct hack for SV-COMP: no struct type body output

A proper fix would be done via #354
---
 src/ansi-c/expr2c.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 4080b8a6d81..22f2c1b7051 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -715,6 +715,7 @@ std::string expr2ct::convert_struct_type(
   if(tag!="")
     dest+=" "+id2string(tag);
 
+#if 0
   if(inc_struct_body)
   {
     dest+=" {";
@@ -737,6 +738,7 @@ std::string expr2ct::convert_struct_type(
 
     dest+=" }";
   }
+#endif
 
   dest+=declarator;
 

From 84d600800736d6a8ee59e7edb0cf6888bd4162e6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Mon, 19 Nov 2018 17:43:43 +0000
Subject: [PATCH 02/33] Use clean-C configuration for graphml counterexample

---
 src/goto-programs/graphml_witness.cpp | 29 ++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index b1821cfde78..f86d2ac26e4 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -19,9 +19,23 @@ Author: Daniel Kroening
 #include <util/ssa_expr.h>
 
 #include <langapi/language_util.h>
+#include <langapi/mode.h>
+
+#include <ansi-c/expr2c.h>
 
 #include "goto_program.h"
 
+static std::string expr_to_string(
+  const namespacet &ns,
+  const irep_idt &id,
+  const exprt &expr)
+{
+  if(get_mode_from_identifier(ns, id) == ID_C)
+    return expr2c(expr, ns, expr2c_configurationt::clean_configuration);
+  else
+    return from_expr(ns, id, expr);
+}
+
 void graphml_witnesst::remove_l0_l1(exprt &expr)
 {
   if(expr.id()==ID_symbol)
@@ -130,11 +144,11 @@ std::string graphml_witnesst::convert_assign_rec(
     exprt clean_rhs=assign.rhs();
     remove_l0_l1(clean_rhs);
 
-    std::string lhs=from_expr(ns, identifier, assign.lhs());
+    std::string lhs=expr_to_string(ns, identifier, assign.lhs());
     if(lhs.find('$')!=std::string::npos)
       lhs="\\result";
 
-    result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";
+    result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";";
   }
 
   return result;
@@ -284,8 +298,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "assumption");
-          val.data = from_expr(ns, it->function, it->full_lhs) + " = " +
-                     from_expr(ns, it->function, it->full_lhs_value) + ";";
+          val.data = expr_to_string(ns, it->function, it->full_lhs) + " = " +
+                     expr_to_string(ns, it->function, it->full_lhs_value) + ";";
 
           xmlt &val_s=edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
@@ -296,9 +310,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond = from_expr(ns, it->function, it->cond_expr);
+          const std::string cond =
+            expr_to_string(ns, it->function, it->cond_expr);
           const std::string neg_cond =
-            from_expr(ns, it->function, not_exprt(it->cond_expr));
+            expr_to_string(ns, it->function, not_exprt(it->cond_expr));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -480,7 +495,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
           const std::string cond =
-            from_expr(ns, it->source.function, it->cond_expr);
+            expr_to_string(ns, it->source.function, it->cond_expr);
           val.data="["+cond+"]";
         }
 

From 98463e1598ac61bc3a349da3b7da29938107cdad Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Tue, 28 Nov 2017 09:14:21 +0000
Subject: [PATCH 03/33] Do not output "NULL"

---
 src/ansi-c/expr2c.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 22f2c1b7051..33c184c426b 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1972,14 +1972,14 @@ std::string expr2ct::convert_constant(
   {
     if(value==ID_NULL)
     {
-      dest="NULL";
+      dest="0";
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
     else if(value==std::string(value.size(), '0') &&
             config.ansi_c.NULL_is_zero)
     {
-      dest="NULL";
+      dest="0";
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }

From a171575bd93628afee52ef4d9af018e330a11034 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 13 Nov 2017 23:09:52 +0000
Subject: [PATCH 04/33] No outgoing edges from  violation nodes

---
 src/goto-programs/graphml_witness.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index f86d2ac26e4..0eaf1c9f1e5 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -254,7 +254,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
   {
     const std::size_t from=step_to_node[it->step_nr];
 
-    if(from==sink)
+    // no outgoing edges from sinks or violation nodes
+    if(from==sink || graphml[from].is_violation)
     {
       ++it;
       continue;

From 65da09728fc55029196a9fdbb07870c7360a4d2f Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Fri, 17 Nov 2017 11:56:05 +0000
Subject: [PATCH 05/33] Using cache to speed up generation of grapml file.

---
 src/goto-programs/graphml_witness.cpp | 10 ++++++++
 src/util/std_pair_hash.h              | 35 +++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)
 create mode 100644 src/util/std_pair_hash.h

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 0eaf1c9f1e5..7964bbe068a 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -17,6 +17,8 @@ Author: Daniel Kroening
 #include <util/arith_tools.h>
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
+#include <util/std_pair_hash.h>
+#include <unordered_map>
 
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
@@ -66,6 +68,13 @@ std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
+  static std::unordered_map<std::pair<unsigned int, const irept::dt *>, std::string> cache;
+  {
+      const auto cit = cache.find({identifier.get_no(), &assign.read()});
+      if(cit != cache.end())
+          return cit->second;
+  }
+
   std::string result;
 
   if(assign.rhs().id()==ID_array)
@@ -151,6 +160,7 @@ std::string graphml_witnesst::convert_assign_rec(
     result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";";
   }
 
+  cache.insert({{identifier.get_no(), &assign.read()}, result});
   return result;
 }
 
diff --git a/src/util/std_pair_hash.h b/src/util/std_pair_hash.h
new file mode 100644
index 00000000000..33ea4635004
--- /dev/null
+++ b/src/util/std_pair_hash.h
@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+Module: util/std_pair_hash
+
+Author: Marek Trtik, marek.trtik@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_STD_PAIR_HASH_H
+#define CPROVER_UTIL_STD_PAIR_HASH_H
+
+#include <functional>
+
+template <typename T>
+inline void hash_combine(std::size_t & seed, const T & v)
+{
+  std::hash<T> hasher;
+  seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+}
+
+namespace std
+{
+  template<typename S, typename T> struct hash<pair<S, T> >
+  {
+    inline size_t operator()(const pair<S, T> & v) const
+    {
+      size_t seed = 0;
+      ::hash_combine(seed, v.first);
+      ::hash_combine(seed, v.second);
+      return seed;
+    }
+  };
+}
+
+#endif

From 52e25c76b57461b567c189233308564bfc5ce044 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 15 Nov 2017 23:23:48 +0000
Subject: [PATCH 06/33] Hack to make CPAchecker parse graphml concurrency
 witnesses

---
 src/goto-programs/graphml_witness.cpp | 52 +++++++++++++++++++--------
 src/xmllang/graphml.cpp               | 29 +++++++--------
 src/xmllang/graphml.h                 |  1 -
 3 files changed, 53 insertions(+), 29 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 7964bbe068a..57265f8770e 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening
 /// \file
 /// Witnesses for Traces and Proofs
 
+#include <iostream>
+
 #include "graphml_witness.h"
 
 #include <util/base_type.h>
@@ -206,7 +208,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 
   const graphmlt::node_indext sink=graphml.add_node();
   graphml[sink].node_name="sink";
-  graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
   graphml[sink].has_invariant=false;
 
@@ -248,7 +249,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
       std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
-    graphml[node].thread_nr=it->thread_nr;
     graphml[node].is_violation=
       it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
     graphml[node].has_invariant=false;
@@ -256,6 +256,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     step_to_node[it->step_nr]=node;
   }
 
+  std::size_t thread_id=0;
+
   // build edges
   for(goto_tracet::stepst::const_iterator
       it=goto_trace.steps.begin();
@@ -288,6 +290,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::ASSERT:
     case goto_trace_stept::typet::GOTO:
+    case goto_trace_stept::typet::SPAWN:
       {
         xmlt edge("edge");
         edge.set_attribute("source", graphml[from].node_name);
@@ -301,20 +304,44 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
           xmlt &data_l=edge.new_element("data");
           data_l.set_attribute("key", "startline");
           data_l.data=id2string(graphml[from].line);
+
+          xmlt &data_t=edge.new_element("data");
+          data_t.set_attribute("key", "threadId");
+          data_t.data=std::to_string(it->thread_nr);
         }
 
         if(it->type==goto_trace_stept::typet::ASSIGNMENT &&
            it->full_lhs_value.is_not_nil() &&
            it->full_lhs.is_not_nil())
         {
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "assumption");
-          val.data = expr_to_string(ns, it->function, it->full_lhs) + " = " +
-                     expr_to_string(ns, it->function, it->full_lhs_value) + ";";
-
-          xmlt &val_s=edge.new_element("data");
-          val_s.set_attribute("key", "assumption.scope");
-          val_s.data=id2string(it->pc->source_location.get_function());
+          if(id2string(it->lhs_object.get_identifier())
+             .find("pthread_create::thread")!=std::string::npos)
+          {
+            xmlt &data_t=edge.new_element("data");
+            data_t.set_attribute("key", "createThread");
+            data_t.data=std::to_string(++thread_id);
+          }
+          else if(id2string(it->lhs_object.get_identifier())
+               .find("#return_value")==std::string::npos &&
+             id2string(it->lhs_object.get_identifier())
+               .find("thread")==std::string::npos &&
+             id2string(it->lhs_object.get_identifier())
+               .find("mutex")==std::string::npos &&
+             (!it->lhs_object_value.is_constant() ||
+              !it->lhs_object_value.has_operands() ||
+              !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)),
+                          "INVALID-")))
+          {
+            xmlt &val=edge.new_element("data");
+            val.set_attribute("key", "assumption");
+            code_assignt assign(it->full_lhs, it->full_lhs_value);
+            irep_idt identifier=it->full_lhs.get_identifier();
+            val.data=convert_assign_rec(identifier, assign);
+
+            xmlt &val_s=edge.new_element("data");
+            val_s.set_attribute("key", "assumption.scope");
+            val_s.data=id2string(it->pc->source_location.get_function());
+          }
         }
         else if(it->type==goto_trace_stept::typet::GOTO &&
                 it->pc->is_goto())
@@ -363,7 +390,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     case goto_trace_stept::typet::OUTPUT:
     case goto_trace_stept::typet::SHARED_READ:
     case goto_trace_stept::typet::SHARED_WRITE:
-    case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:
     case goto_trace_stept::typet::ATOMIC_END:
@@ -385,7 +411,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
 
   const graphmlt::node_indext sink=graphml.add_node();
   graphml[sink].node_name="sink";
-  graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
   graphml[sink].has_invariant=false;
 
@@ -431,7 +456,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
       std::to_string(step_nr);
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
-    graphml[node].thread_nr=it->source.thread_nr;
     graphml[node].is_violation=false;
     graphml[node].has_invariant=false;
 
@@ -472,6 +496,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::ASSERT:
     case goto_trace_stept::typet::GOTO:
+    case goto_trace_stept::typet::SPAWN:
       {
         xmlt edge("edge");
         edge.set_attribute("source", graphml[from].node_name);
@@ -524,7 +549,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     case goto_trace_stept::typet::OUTPUT:
     case goto_trace_stept::typet::SHARED_READ:
     case goto_trace_stept::typet::SHARED_WRITE:
-    case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:
     case goto_trace_stept::typet::ATOMIC_END:
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 17dc6fd9577..bf9fc50207a 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -54,7 +54,6 @@ static bool build_graph_rec(
     node.node_name=node_name;
     node.is_violation=false;
     node.has_invariant=false;
-    node.thread_nr=0;
 
     for(xmlt::elementst::const_iterator
         e_it=xml.elements.begin();
@@ -66,8 +65,6 @@ static bool build_graph_rec(
       if(e_it->get_attribute("key")=="violation" &&
          e_it->data=="true")
         node.is_violation=e_it->data=="true";
-      else if(e_it->get_attribute("key")=="threadNumber")
-        node.thread_nr=safe_string2unsigned(e_it->data);
       else if(e_it->get_attribute("key")=="entry" &&
               e_it->data=="true")
         entrynode=node_name;
@@ -337,13 +334,24 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
   }
 
   // <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
-  // TODO: format for multi-threaded programs not defined yet
   {
     xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "threadNumber");
+    key.set_attribute("attr.name", "threadId");
     key.set_attribute("attr.type", "int");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "thread");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "threadId");
+
+    key.new_element("default").data="0";
+  }
+
+  // <key attr.name="createThread" attr.type="string"
+  //      for="edge" id="createThread"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "createThread");
+    key.set_attribute("attr.type", "int");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "createThread");
 
     key.new_element("default").data="0";
   }
@@ -525,13 +533,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
       entry_done=true;
     }
 
-    if(n.thread_nr!=0)
-    {
-      xmlt &entry=node.new_element("data");
-      entry.set_attribute("key", "threadNumber");
-      entry.data=std::to_string(n.thread_nr);
-    }
-
     // <node id="A14">
     //     <data key="violation">true</data>
     // </node>
diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h
index f86dac5648e..cbdcd122828 100644
--- a/src/xmllang/graphml.h
+++ b/src/xmllang/graphml.h
@@ -32,7 +32,6 @@ struct xml_graph_nodet:public graph_nodet<xml_edget>
   std::string node_name;
   irep_idt file;
   irep_idt line;
-  unsigned thread_nr;
   bool is_violation;
   bool has_invariant;
   std::string invariant;

From 9782c4be0419c2eea20aabd09063bc448bcc0ed8 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 20 Nov 2017 15:23:49 +0000
Subject: [PATCH 07/33] Make sure SSA suffixes are stripped off graphml output

---
 src/goto-programs/graphml_witness.cpp | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 57265f8770e..f079b2cddb4 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -155,7 +155,9 @@ std::string graphml_witnesst::convert_assign_rec(
     exprt clean_rhs=assign.rhs();
     remove_l0_l1(clean_rhs);
 
-    std::string lhs=expr_to_string(ns, identifier, assign.lhs());
+    exprt clean_lhs=assign.lhs();
+    remove_l0_l1(clean_lhs);
+    std::string lhs=expr_to_string(ns, identifier, clean_lhs);
     if(lhs.find('$')!=std::string::npos)
       lhs="\\result";
 
@@ -348,10 +350,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            expr_to_string(ns, it->function, it->cond_expr);
-          const std::string neg_cond =
-            expr_to_string(ns, it->function, not_exprt(it->cond_expr));
+          exprt clean_cond=it->cond_expr;
+          remove_l0_l1(clean_cond);
+          const std::string cond=expr_to_string(ns, it->function, clean_cond);
+          const std::string neg_cond=
+            from_expr(ns, it->function, not_exprt(clean_cond));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -530,8 +533,10 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            expr_to_string(ns, it->source.function, it->cond_expr);
+          exprt clean_cond=it->cond_expr;
+          remove_l0_l1(clean_cond);
+          const std::string cond=expr_to_string(ns, it->source.function, clean_cond);
+            from_expr(ns, it->source.function, not_exprt(clean_cond));
           val.data="["+cond+"]";
         }
 

From b5278931f7a8dea00b820844b8d8356a6343da85 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 20 Nov 2017 22:18:45 +0000
Subject: [PATCH 08/33] Remove obsolete graphml frontierNode, nodeType and add
 new cyclehead

---
 src/xmllang/graphml.cpp | 41 ++++++++++++++---------------------------
 1 file changed, 14 insertions(+), 27 deletions(-)

diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index bf9fc50207a..12441ed65f3 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -252,33 +252,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "invariant.scope");
   }
 
-  // <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
-  //     <default>path</default>
-  // </key>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "nodeType");
-    key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "nodetype");
-
-    key.new_element("default").data="path";
-  }
-
-  // <key attr.name="isFrontierNode" attr.type="boolean" for="node"
-  //      id="frontier">
-  //     <default>false</default>
-  // </key>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "isFrontierNode");
-    key.set_attribute("attr.type", "boolean");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "frontier");
-
-    key.new_element("default").data="false";
-  }
-
   // <key attr.name="isViolationNode" attr.type="boolean" for="node"
   //      id="violation">
   //     <default>false</default>
@@ -333,6 +306,20 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="false";
   }
 
+  // <key attr.name="cyclehead" attr.type="boolean" for="edge"
+  //      id="cyclehead">
+  //   <default>false</default>
+  // </key>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "cyclehead");
+    key.set_attribute("attr.type", "boolean");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "cyclehead");
+
+    key.new_element("default").data="false";
+  }
+
   // <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
   {
     xmlt &key=graphml.new_element("key");

From 587b5c71ddf0d2d0afb4f651e07dee178b0b98c9 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 20 Nov 2017 23:22:06 +0000
Subject: [PATCH 09/33] Remove obsolete sourcecode element in graphml

---
 src/goto-programs/graphml_witness.cpp | 29 ---------------------------
 src/xmllang/graphml.cpp               |  9 ---------
 2 files changed, 38 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index f079b2cddb4..689a62167ba 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -348,35 +348,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         else if(it->type==goto_trace_stept::typet::GOTO &&
                 it->pc->is_goto())
         {
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "sourcecode");
-          exprt clean_cond=it->cond_expr;
-          remove_l0_l1(clean_cond);
-          const std::string cond=expr_to_string(ns, it->function, clean_cond);
-          const std::string neg_cond=
-            from_expr(ns, it->function, not_exprt(clean_cond));
-          val.data="["+(it->cond_value ? cond : neg_cond)+"]";
-
-          #if 0
-          xmlt edge2("edge");
-          edge2.set_attribute("source", graphml[from].node_name);
-          edge2.set_attribute("target", graphml[sink].node_name);
-
-          xmlt &data_f2=edge2.new_element("data");
-          data_f2.set_attribute("key", "originfile");
-          data_f2.data=id2string(graphml[from].file);
-
-          xmlt &data_l2=edge2.new_element("data");
-          data_l2.set_attribute("key", "startline");
-          data_l2.data=id2string(graphml[from].line);
-
-          xmlt &val2=edge2.new_element("data");
-          val2.set_attribute("key", "sourcecode");
-          val2.data="["+(it->cond_value ? neg_cond : cond)+"]";
-
-          graphml[sink].in[from].xml_node=edge2;
-          graphml[from].out[sink].xml_node=edge2;
-          #endif
         }
 
         graphml[to].in[from].xml_node=edge;
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 12441ed65f3..4b780b9df8c 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -403,15 +403,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "producer");
   }
 
-  // <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "sourcecode");
-    key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "edge");
-    key.set_attribute("id", "sourcecode");
-  }
-
   // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
   {
     xmlt &key=graphml.new_element("key");

From a4ceecc6c864733d9a8387b2db35094b9ccd2bf6 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 26 Nov 2017 22:55:04 +0000
Subject: [PATCH 10/33] Split array-list into assignments and hide dynamic
 objects

---
 src/goto-programs/graphml_witness.cpp | 73 +++++++++++++++++++++------
 1 file changed, 58 insertions(+), 15 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 689a62167ba..4321fdddb1b 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -79,7 +79,29 @@ std::string graphml_witnesst::convert_assign_rec(
 
   std::string result;
 
-  if(assign.rhs().id()==ID_array)
+  if(assign.rhs().id()=="array-list")
+  {
+    const array_typet &type=
+      to_array_type(ns.follow(assign.rhs().type()));
+
+    const auto ops=assign.rhs().operands();
+    DATA_INVARIANT(
+      ops.size()%2==0,
+      "array-list has odd number of operands");
+
+    for(size_t listidx=0; listidx!=ops.size(); listidx+=2)
+    {
+      index_exprt index(
+        assign.lhs(),
+        ops[listidx],
+        type.subtype());
+      if(!result.empty())
+        result+=' ';
+      result+=
+        convert_assign_rec(identifier, code_assignt(index, ops[listidx+1]));
+    }
+  }
+  else if(assign.rhs().id()==ID_array)
   {
     const array_typet &type=
       to_array_type(ns.follow(assign.rhs().type()));
@@ -163,7 +185,6 @@ std::string graphml_witnesst::convert_assign_rec(
 
     result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";";
   }
-
   cache.insert({{identifier.get_no(), &assign.read()}, result});
   return result;
 }
@@ -203,6 +224,21 @@ static bool filter_out(
   return false;
 }
 
+static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix){
+  if(expr.id()==ID_symbol &&
+     has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix))
+  {
+    return true;
+  }
+
+  forall_operands(it, expr)
+  {
+    if(contains_symbol_prefix(*it, prefix))
+      return true;
+  }
+  return false;
+}
+
 /// counterexample witness
 void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 {
@@ -314,30 +350,37 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 
         if(it->type==goto_trace_stept::typet::ASSIGNMENT &&
            it->full_lhs_value.is_not_nil() &&
-           it->full_lhs.is_not_nil())
+           it->full_lhs.is_not_nil() &&
+           it->full_lhs.id() == ID_symbol)
         {
-          if(id2string(it->lhs_object.get_identifier())
+          const symbol_exprt &lhs_symbol = to_symbol_expr(it->full_lhs);
+          if(id2string(lhs_symbol.get_identifier())
              .find("pthread_create::thread")!=std::string::npos)
           {
             xmlt &data_t=edge.new_element("data");
             data_t.set_attribute("key", "createThread");
             data_t.data=std::to_string(++thread_id);
           }
-          else if(id2string(it->lhs_object.get_identifier())
-               .find("#return_value")==std::string::npos &&
-             id2string(it->lhs_object.get_identifier())
-               .find("thread")==std::string::npos &&
-             id2string(it->lhs_object.get_identifier())
-               .find("mutex")==std::string::npos &&
-             (!it->lhs_object_value.is_constant() ||
-              !it->lhs_object_value.has_operands() ||
-              !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)),
-                          "INVALID-")))
+          else if(
+            id2string(lhs_symbol.get_identifier())
+              .find("#return_value")==std::string::npos &&
+            !contains_symbol_prefix(
+              it->full_lhs_value, "symex_dynamic::dynamic_object") &&
+            !contains_symbol_prefix(
+              it->full_lhs, "symex_dynamic::dynamic_object") &&
+            id2string(lhs_symbol.get_identifier())
+              .find("thread")==std::string::npos &&
+            id2string(lhs_symbol.get_identifier())
+              .find("mutex")==std::string::npos &&
+            (!it->full_lhs_value.is_constant() ||
+             !it->full_lhs_value.has_operands() ||
+             !has_prefix(id2string(it->full_lhs_value.op0().get(ID_value)),
+                         "INVALID-")))
           {
             xmlt &val=edge.new_element("data");
             val.set_attribute("key", "assumption");
             code_assignt assign(it->full_lhs, it->full_lhs_value);
-            irep_idt identifier=it->full_lhs.get_identifier();
+            irep_idt identifier=lhs_symbol.get_identifier();
             val.data=convert_assign_rec(identifier, assign);
 
             xmlt &val_s=edge.new_element("data");

From bb159aed434b14c4e52c4afbef77fca1677fa14b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 26 Nov 2017 23:14:18 +0000
Subject: [PATCH 11/33] Remove obsolete sourcecode element from graphml

---
 src/goto-programs/graphml_witness.cpp | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 4321fdddb1b..d5fbfcfc2a9 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -542,17 +542,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
           graphml[to].invariant_scope=
             id2string(it->source.pc->source_location.get_function());
         }
-        else if(it->is_goto() &&
-                it->source.pc->is_goto())
-        {
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "sourcecode");
-          exprt clean_cond=it->cond_expr;
-          remove_l0_l1(clean_cond);
-          const std::string cond=expr_to_string(ns, it->source.function, clean_cond);
-            from_expr(ns, it->source.function, not_exprt(clean_cond));
-          val.data="["+cond+"]";
-        }
 
         graphml[to].in[from].xml_node=edge;
         graphml[from].out[to].xml_node=edge;

From 154bdad3addcd22b8e07a4521f36c28bbdabb196 Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Mon, 27 Nov 2017 17:59:25 +0000
Subject: [PATCH 12/33] graphml: More precise detection of when to use
 '\result' variable.

---
 src/goto-programs/graphml_witness.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index d5fbfcfc2a9..f315697d86b 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -180,7 +180,9 @@ std::string graphml_witnesst::convert_assign_rec(
     exprt clean_lhs=assign.lhs();
     remove_l0_l1(clean_lhs);
     std::string lhs=expr_to_string(ns, identifier, clean_lhs);
-    if(lhs.find('$')!=std::string::npos)
+    if(lhs.find("#return_value")!=std::string::npos ||
+       (lhs.find('$')!=std::string::npos &&
+        lhs.find("return_value___VERIFIER_nondet_")==0U))
       lhs="\\result";
 
     result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";";

From c38b2dd34d9c4064f0a8324012e052fb1fce3d0d Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Mon, 27 Nov 2017 17:59:25 +0000
Subject: [PATCH 13/33] graphml: Special (hacky) structure of concurrency
 witness.

---
 src/goto-programs/graphml_witness.cpp | 46 +++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index f315697d86b..f2dca139982 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -244,6 +244,18 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
 /// counterexample witness
 void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 {
+  unsigned int max_thread_idx=0U;
+  bool trace_has_violation=false;
+  for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin();
+      it!=goto_trace.steps.end();
+      ++it)
+  {
+    if(it->thread_nr>max_thread_idx)
+      max_thread_idx=it->thread_nr;
+    if(it->type==goto_trace_stept::typet::ASSERT && !it->cond_value)
+      trace_has_violation=true;
+  }
+
   graphml.key_values["sourcecodelang"]="C";
 
   const graphmlt::node_indext sink=graphml.add_node();
@@ -251,6 +263,40 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
   graphml[sink].is_violation=false;
   graphml[sink].has_invariant=false;
 
+  if(max_thread_idx > 0U && trace_has_violation)
+  {
+    std::vector<graphmlt::node_indext> nodes;
+
+    for(unsigned int i=0U; i<=max_thread_idx+1U; ++i)
+    {
+      nodes.push_back(graphml.add_node());
+      graphml[nodes.back()].node_name="N" + std::to_string(i);
+      graphml[nodes.back()].is_violation=(i==max_thread_idx+1U) ? true : false;
+      graphml[nodes.back()].has_invariant=false;
+    }
+
+    for(auto it=nodes.cbegin(); std::next(it)!=nodes.cend(); ++it)
+    {
+      xmlt edge("edge");
+      edge.set_attribute("source", graphml[*it].node_name);
+      edge.set_attribute("target", graphml[*std::next(it)].node_name);
+      const auto thread_id=std::distance(nodes.cbegin(), it);
+      xmlt &data=edge.new_element("data");
+      data.set_attribute("key", "createThread");
+      data.data=std::to_string(thread_id);
+      if(thread_id==0)
+      {
+        xmlt &data=edge.new_element("data");
+        data.set_attribute("key", "enterFunction");
+        data.data="main";
+      }
+      graphml[*std::next(it)].in[*it].xml_node=edge;
+      graphml[*it].out[*std::next(it)].xml_node=edge;
+    }
+
+    return;
+  }
+
   // step numbers start at 1
   std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
 

From c3022b045e691aa5a7c8f9698d41f09e29ebff38 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 24 Nov 2018 19:51:33 +0000
Subject: [PATCH 14/33] Update expected graphml output, to be merged

---
 regression/cbmc/graphml_witness1/test.desc | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index cb22eaba5d0..5203bd00210 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -7,34 +7,21 @@ main.c
 <graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
   <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
   <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
-  <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
-    <default>path</default>
-  </key>
-  <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
-    <default>false</default>
-  </key>
   <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
     <default>false</default>
   </key>
   <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
     <default>false</default>
   </key>
-  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
-    <default>false</default>
-  </key>
   <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
     <default>false</default>
   </key>
-  <key attr.name="threadNumber" attr.type="int" for="node" id="thread">
-    <default>0</default>
-  </key>
   <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
   <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
   <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
   <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
   <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
   <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
-  <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
   <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
   <key attr.name="control" attr.type="string" for="edge" id="control"/>
   <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
@@ -45,7 +32,6 @@ main.c
   <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
   <graph edgedefault="directed">
     <data key="sourcecodelang">C</data>
-    <node id="sink"/>
     <node id="[0-9\.]*">
       <data key="entry">true</data>
     </node>
@@ -68,10 +54,6 @@ main.c
     <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="[0-9\.]*" target="sink">
-      <data key="originfile">main.c</data>
-      <data key="startline">31</data>
-    </edge>
   </graph>
 </graphml>
 --

From 68032187ed62e5294a585d7023d37bdd8e043b71 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Mon, 27 Nov 2017 18:44:45 +0000
Subject: [PATCH 15/33] Add violation node for the memory safety benchmarks

---
 src/goto-programs/graphml_witness.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index f2dca139982..106265cc7aa 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 #include <util/std_pair_hash.h>
@@ -221,7 +222,11 @@ static bool filter_out(
      source_location.get_file().empty() ||
      source_location.is_built_in() ||
      source_location.get_line().empty())
-    return true;
+  {
+    const irep_idt id=source_location.get_function();
+    if(!(has_prefix(id2string(id), CPROVER_PREFIX) && it->is_assert()))
+      return true;
+  }
 
   return false;
 }
@@ -337,6 +342,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     graphml[node].line=source_location.get_line();
     graphml[node].is_violation=
       it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
+
     graphml[node].has_invariant=false;
 
     step_to_node[it->step_nr]=node;

From d1bf5ea53a78ec07a940c48a2b7041852dba464d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Mon, 2 Jan 2017 16:48:51 +0000
Subject: [PATCH 16/33] Ensure that local declarations do not introduce
 spurious dead warnings

---
 regression/cbmc/Local_out_of_scope4/main.c    | 15 ++++++++++
 regression/cbmc/Local_out_of_scope4/test.desc |  8 ++++++
 src/analyses/goto_check.cpp                   | 28 +++++++++++++++++++
 src/goto-symex/symex_decl.cpp                 |  7 ++---
 4 files changed, 53 insertions(+), 5 deletions(-)
 create mode 100644 regression/cbmc/Local_out_of_scope4/main.c
 create mode 100644 regression/cbmc/Local_out_of_scope4/test.desc

diff --git a/regression/cbmc/Local_out_of_scope4/main.c b/regression/cbmc/Local_out_of_scope4/main.c
new file mode 100644
index 00000000000..4117a283b4d
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope4/main.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int *p = 0;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    {
+      int x = 42;
+      p = &x;
+      *p = 1;
+    }
+  }
+
+  return 0;
+}
diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc
new file mode 100644
index 00000000000..39c491ba8bb
--- /dev/null
+++ b/regression/cbmc/Local_out_of_scope4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index ce6f07672a3..fa7eafe7253 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1711,6 +1711,34 @@ void goto_checkt::goto_check(
         }
       }
     }
+    else if(i.is_decl())
+    {
+      if(enable_pointer_check)
+      {
+        assert(i.code.operands().size()==1);
+        const symbol_exprt &variable=to_symbol_expr(i.code.op0());
+
+        // is it dirty?
+        if(local_bitvector_analysis->dirty(variable))
+        {
+          // reset the dead marker
+          goto_programt::targett t=new_code.add_instruction(ASSIGN);
+          exprt address_of_expr=address_of_exprt(variable);
+          exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs=
+            if_exprt(
+              equal_exprt(lhs, address_of_expr),
+              null_pointer_exprt(to_pointer_type(address_of_expr.type())),
+              lhs,
+              lhs.type());
+          t->source_location=i.source_location;
+          t->code=code_assignt(lhs, rhs);
+          t->code.add_source_location()=i.source_location;
+        }
+      }
+    }
     else if(i.is_end_function())
     {
       if(i.function==goto_functionst::entry_point() &&
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index ff2caf9cb4a..8b39b2610f4 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -66,11 +66,8 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   state.propagation.erase(l1_identifier);
 
   // L2 renaming
-  // inlining may yield multiple declarations of the same identifier
-  // within the same L1 context
-  if(state.level2.current_names.find(l1_identifier)==
-     state.level2.current_names.end())
-    state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
+  state.level2.current_names.insert(
+    std::make_pair(l1_identifier, std::make_pair(ssa, 0)));
   state.level2.increase_counter(l1_identifier);
   const bool record_events=state.record_events;
   state.record_events=false;

From 479dd14938fe27e8606788f57fb961d29ee2b845 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Fri, 6 Jan 2017 17:31:07 +0000
Subject: [PATCH 17/33] invalid_object(pointer) is true for all non-existent
 objects

Check whether the object part of a pointer is greater or equal the total
number of objects, or equals a dynamic object that has not actually been
allocated on a given trace.
---
 src/goto-symex/symex_builtin_functions.cpp | 10 ++-
 src/solvers/flattening/bv_pointers.cpp     | 99 ++++++++++++++++++----
 2 files changed, 89 insertions(+), 20 deletions(-)

diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 85d144ad6f1..f062ba553a7 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -184,18 +184,20 @@ void goto_symext::symex_allocate(
 
   exprt rhs;
 
+  symbol_exprt v=value_symbol.symbol_expr();
+  v.add("#dynamic_guard", state.guard);
+
   if(object_type.id()==ID_array)
   {
-    const auto &array_type = to_array_type(object_type);
+    const auto &array_type = to_array_type(value_symbol.type);
     index_exprt index_expr(array_type.subtype());
-    index_expr.array()=value_symbol.symbol_expr();
+    index_expr.array() = v;
     index_expr.index()=from_integer(0, index_type());
     rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
   }
   else
   {
-    rhs=address_of_exprt(
-      value_symbol.symbol_expr(), pointer_type(value_symbol.type));
+    rhs = address_of_exprt(v, pointer_type(value_symbol.type));
   }
 
   if(rhs.type()!=lhs.type())
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 791c06475b1..7236621b7bf 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -12,7 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
+#include <util/invariant.h>
 #include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
 {
@@ -25,24 +29,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
     {
-      const bvt &bv=convert_bv(operands[0]);
-
-      if(!bv.empty())
-      {
-        bvt invalid_bv;
-        encode(pointer_logic.get_invalid_object(), invalid_bv);
-
-        bvt equal_invalid_bv;
-        equal_invalid_bv.resize(object_bits);
+      // we postpone
+      literalt l=prop.new_variable();
 
-        for(std::size_t i=0; i<object_bits; i++)
-        {
-          equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
-                                          invalid_bv[offset_bits+i]);
-        }
+      postponed_list.push_back(postponedt());
+      postponed_list.back().op=convert_bv(operands[0]);
+      postponed_list.back().bv.push_back(l);
+      postponed_list.back().expr=expr;
 
-        return prop.land(equal_invalid_bv);
-      }
+      return l;
     }
   }
   else if(expr.id()==ID_dynamic_object)
@@ -820,6 +815,78 @@ void bv_pointerst::do_postponed(
       prop.l_set_to(prop.limplies(l1, l2), true);
     }
   }
+  else if(postponed.expr.id()==ID_invalid_pointer)
+  {
+    const pointer_logict::objectst &objects=pointer_logic.objects;
+
+    bvt disj;
+    disj.reserve(objects.size());
+
+    bvt saved_bv=postponed.op;
+    saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
+
+    bvt invalid_bv, null_bv;
+    encode(pointer_logic.get_invalid_object(), invalid_bv);
+    invalid_bv.erase(invalid_bv.begin(), invalid_bv.begin()+offset_bits);
+    encode(pointer_logic.get_null_object(),    null_bv);
+    null_bv.erase(null_bv.begin(), null_bv.begin()+offset_bits);
+
+    disj.push_back(bv_utils.equal(saved_bv, invalid_bv));
+    disj.push_back(bv_utils.equal(saved_bv, null_bv));
+
+    // compare object part to non-allocated dynamic objects
+    std::size_t number=0;
+
+    for(pointer_logict::objectst::const_iterator
+        it=objects.begin();
+        it!=objects.end();
+        it++, number++)
+    {
+      const exprt &expr=*it;
+
+      if(!pointer_logic.is_dynamic_object(expr) ||
+         !is_ssa_expr(expr))
+        continue;
+
+      // only compare object part
+      bvt bv;
+      encode(number, bv);
+
+      bv.erase(bv.begin(), bv.begin()+offset_bits);
+      assert(bv.size()==saved_bv.size());
+
+      literalt l1=bv_utils.equal(bv, saved_bv);
+
+      const ssa_exprt &ssa=to_ssa_expr(expr);
+
+      const exprt &guard=
+        static_cast<const exprt&>(
+          ssa.get_original_expr().find("#dynamic_guard"));
+
+      if(guard.is_nil())
+        continue;
+
+      const bvt &guard_bv=convert_bv(guard);
+      assert(guard_bv.size()==1);
+      literalt l_guard=guard_bv[0];
+
+      disj.push_back(prop.land(!l_guard, l1));
+    }
+
+    // compare object part to max object number
+    bvt bv;
+    encode(number, bv);
+
+    bv.erase(bv.begin(), bv.begin()+offset_bits);
+    assert(bv.size()==saved_bv.size());
+
+    disj.push_back(
+      bv_utils.rel(saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED));
+
+    assert(postponed.bv.size()==1);
+    literalt l=postponed.bv.front();
+    prop.l_set_to(prop.lequal(prop.lor(disj), l), true);
+  }
   else
     UNREACHABLE;
 }

From 52de4406f96eef7ffe4c652cb2fd16368da21bf5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 19 Nov 2018 18:35:57 +0000
Subject: [PATCH 18/33] fixup! Do not output "NULL"

---
 src/ansi-c/expr2c.cpp | 8 +++++---
 src/ansi-c/expr2c.h   | 9 +++++++--
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 33c184c426b..e8deeb74c8e 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -39,7 +39,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   true,
   "TRUE",
-  "FALSE"
+  "FALSE",
+  "NULL"
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -48,6 +49,7 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   false,
   "1",
+  "0",
   "0"
 };
 
@@ -1972,14 +1974,14 @@ std::string expr2ct::convert_constant(
   {
     if(value==ID_NULL)
     {
-      dest="0";
+      dest = configuration.null_pointer_string;
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
     else if(value==std::string(value.size(), '0') &&
             config.ansi_c.NULL_is_zero)
     {
-      dest="0";
+      dest = configuration.null_pointer_string;
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h
index 3689c5478bb..818f82737e7 100644
--- a/src/ansi-c/expr2c.h
+++ b/src/ansi-c/expr2c.h
@@ -36,17 +36,22 @@ struct expr2c_configurationt final
   /// This is the string that will be printed for the false boolean expression
   std::string false_string;
 
+  /// This is the string that will be printed for null pointers
+  std::string null_pointer_string;
+
   expr2c_configurationt(
     const bool include_struct_padding_components,
     const bool print_struct_body_in_type,
     const bool include_array_size,
     std::string true_string,
-    std::string false_string)
+    std::string false_string,
+    const std::string &null_pointer_string)
     : include_struct_padding_components(include_struct_padding_components),
       print_struct_body_in_type(print_struct_body_in_type),
       include_array_size(include_array_size),
       true_string(std::move(true_string)),
-      false_string(std::move(false_string))
+      false_string(std::move(false_string)),
+      null_pointer_string(null_pointer_string)
   {
   }
 

From a80f75646bfbfc0245e3b6cba40981ca66056065 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 19 Nov 2018 18:41:02 +0000
Subject: [PATCH 19/33] Add a definition of alloca

Benchmarks not including headers files fail as we only provided a definition of
__builtin_alloca, which alloca expands to in standard libary headers, but none
for alloca directly.
---
 src/ansi-c/library/stdlib.c | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 7f72651a18f..c2576c179ec 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -147,6 +147,18 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   return res;
 }
 
+/* FUNCTION: alloca */
+
+#undef alloca
+
+void *__builtin_alloca(__CPROVER_size_t alloca_size);
+
+inline void *alloca(__CPROVER_size_t alloca_size)
+{
+  __CPROVER_HIDE:;
+  return __builtin_alloca(alloca_size);
+}
+
 /* FUNCTION: free */
 
 #undef free

From 53352cdd2b10cf1e0d35539cb664ee2a95cedc93 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Mon, 26 Dec 2016 12:23:41 +0000
Subject: [PATCH 20/33] Do not perform SSA sanity checks

Iterating over all expression tress has considerable performance cost,
seemingly accounting for up to 10% of runtime (on SV-COMP benchmarks,
with profiling enabled).
---
 src/goto-symex/goto_symex_state.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 125042ff065..56de8162d42 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -38,6 +38,7 @@ goto_symex_statet::goto_symex_statet()
 
 goto_symex_statet::~goto_symex_statet()=default;
 
+#if 0
 /// write to a variable
 static bool check_renaming(const exprt &expr);
 
@@ -120,10 +121,11 @@ static bool check_renaming(const exprt &expr)
 
   return false;
 }
+#endif
 
 static void assert_l1_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming_l1(expr))
   {
     std::cerr << expr.pretty() << '\n';
@@ -136,7 +138,7 @@ static void assert_l1_renaming(const exprt &expr)
 
 static void assert_l2_renaming(const exprt &expr)
 {
-  #if 1
+  #if 0
   if(check_renaming(expr))
   {
     std::cerr << expr.pretty() << '\n';

From 04f9c35e807a4199bff0144d6451427be0c63801 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 23 Mar 2018 19:20:07 +0000
Subject: [PATCH 21/33] irept: Use singly-linked lists with SUB_IS_LIST

This reduces the memory footprint by two pointers for both named_sub and
comments. The cost is that computing the size of lists and add/remove require
additional iterator increments.
---
 src/util/format_expr.cpp         |  1 +
 src/util/irep.cpp                | 60 ++++++++++++++++++++++-----
 src/util/irep.h                  |  4 +-
 src/util/irep_hash_container.cpp | 17 +++++---
 src/util/lispirep.cpp            | 14 +++++--
 src/util/merge_irep.cpp          | 69 ++++++++++++++++++++++++++------
 unit/util/irep.cpp               | 28 +++++++++----
 7 files changed, 154 insertions(+), 39 deletions(-)

diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 1819f13a299..32b250edbdf 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "string2int.h"
 #include "string_utils.h"
 
+#include <map>
 #include <ostream>
 #include <stack>
 
diff --git a/src/util/irep.cpp b/src/util/irep.cpp
index b403ea96550..31d07351b17 100644
--- a/src/util/irep.cpp
+++ b/src/util/irep.cpp
@@ -153,8 +153,8 @@ void irept::nonrecursive_destructor(dt *old_data)
     if(d->ref_count==0)
     {
       stack.reserve(stack.size()+
-                    d->named_sub.size()+
-                    d->comments.size()+
+                    std::distance(d->named_sub.begin(), d->named_sub.end()) +
+                    std::distance(d->comments.begin(), d->comments.end()) +
                     d->sub.size());
 
       for(named_subt::iterator
@@ -275,7 +275,11 @@ void irept::remove(const irep_namet &name)
   named_subt::iterator it=named_subt_lower_bound(s, name);
 
   if(it!=s.end() && it->first==name)
-    s.erase(it);
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    s.erase_after(before);
+  }
   #else
   s.erase(name);
   #endif
@@ -312,7 +316,11 @@ irept &irept::add(const irep_namet &name)
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irept()));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    it = s.emplace_after(before, name, irept());
+  }
 
   return it->second;
   #else
@@ -330,7 +338,11 @@ irept &irept::add(const irep_namet &name, const irept &irep)
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irep));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    it = s.emplace_after(before, name, irep);
+  }
   else
     it->second=irep;
 
@@ -393,10 +405,20 @@ bool irept::full_eq(const irept &other) const
   const irept::named_subt &i1_comments=get_comments();
   const irept::named_subt &i2_comments=other.get_comments();
 
+#ifdef SUB_IS_LIST
+  if(
+    i1_sub.size() != i2_sub.size() ||
+    std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
+    std::distance(i2_named_sub.begin(), i2_named_sub.end()) ||
+    std::distance(i1_comments.begin(), i1_comments.end()) !=
+    std::distance(i2_comments.begin(), i2_comments.end()))
+    return false;
+#else
   if(i1_sub.size()!=i2_sub.size() ||
      i1_named_sub.size()!=i2_named_sub.size() ||
      i1_comments.size()!=i2_comments.size())
     return false;
+#endif
 
   for(std::size_t i=0; i<i1_sub.size(); i++)
     if(!i1_sub[i].full_eq(i2_sub[i]))
@@ -527,8 +549,15 @@ int irept::compare(const irept &i) const
               "Unequal lengths will return before this");
   }
 
+#ifdef SUB_IS_LIST
+  const named_subt::size_type n_size =
+    std::distance(get_named_sub().begin(), get_named_sub().end());
+  const named_subt::size_type i_n_size =
+    std::distance(i.get_named_sub().begin(), i.get_named_sub().end());
+#else
   const named_subt::size_type n_size=get_named_sub().size(),
         i_n_size=i.get_named_sub().size();
+#endif
   if(n_size<i_n_size)
     return -1;
   if(n_size>i_n_size)
@@ -591,7 +620,13 @@ std::size_t irept::hash() const
     result=hash_combine(result, it->second.hash());
   }
 
-  result=hash_finalize(result, named_sub.size()+sub.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   #ifdef HASH_CODE
   read().hash_code=result;
@@ -624,9 +659,16 @@ std::size_t irept::full_hash() const
     result=hash_combine(result, it->second.full_hash());
   }
 
-  result=hash_finalize(
-    result,
-    named_sub.size()+sub.size()+comments.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+  const std::size_t comments_size =
+    std::distance(comments.begin(), comments.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+  const std::size_t comments_size = comments.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size() + comments_size);
 
   return result;
 }
diff --git a/src/util/irep.h b/src/util/irep.h
index 706fb60db26..464651ba8cf 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define SUB_IS_LIST
 
 #ifdef SUB_IS_LIST
-#include <list>
+#include <forward_list>
 #else
 #include <map>
 #endif
@@ -164,7 +164,7 @@ class irept
   // memory and increase efficiency.
 
   #ifdef SUB_IS_LIST
-  typedef std::list<std::pair<irep_namet, irept> > named_subt;
+  typedef std::forward_list<std::pair<irep_namet, irept> > named_subt;
   #else
   typedef std::map<irep_namet, irept> named_subt;
   #endif
diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp
index dc79d098670..b49ef2b105d 100644
--- a/src/util/irep_hash_container.cpp
+++ b/src/util/irep_hash_container.cpp
@@ -51,9 +51,16 @@ void irep_hash_container_baset::pack(
   const irept::named_subt &named_sub=irep.get_named_sub();
   const irept::named_subt &comments=irep.get_comments();
 
-  packed.reserve(
-    1+1+sub.size()+named_sub.size()*2+
-    (full?comments.size()*2:0));
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+  const std::size_t comments_size = full ?
+    std::distance(comments.begin(), comments.end()) : 0;
+#else
+  const std::size_t named_sub_size = named_sub.size();
+  const std::size_t comments_size = full ? comments.size() : 0;
+#endif
+  packed.reserve(1 + 1 + sub.size() + named_sub_size * 2 + comments_size * 2);
 
   packed.push_back(irep_id_hash()(irep.id()));
 
@@ -61,7 +68,7 @@ void irep_hash_container_baset::pack(
   forall_irep(it, sub)
     packed.push_back(number(*it));
 
-  packed.push_back(named_sub.size());
+  packed.push_back(named_sub_size);
   forall_named_irep(it, named_sub)
   {
     packed.push_back(irep_id_hash()(it->first)); // id
@@ -70,7 +77,7 @@ void irep_hash_container_baset::pack(
 
   if(full)
   {
-    packed.push_back(comments.size());
+    packed.push_back(comments_size);
     forall_named_irep(it, comments)
     {
       packed.push_back(irep_id_hash()(it->first)); // id
diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp
index 6f223d0c7f6..35904def2fa 100644
--- a/src/util/lispirep.cpp
+++ b/src/util/lispirep.cpp
@@ -46,9 +46,17 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value="";
   dest.type=lispexprt::List;
 
-  dest.reserve(2+2*src.get_sub().size()
-                +2*src.get_named_sub().size()
-                +2*src.get_comments().size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
+  const std::size_t comments_size =
+    std::distance(src.get_comments().begin(), src.get_comments().end());
+#else
+  const std::size_t named_sub_size = src.get_named_sub().size();
+  const std::size_t comments_size = src.get_comments().size();
+#endif
+  dest.reserve(
+    2 + 2 * src.get_sub().size() + 2 * named_sub_size + 2 * comments_size);
 
   lispexprt id;
   id.type=lispexprt::String;
diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp
index 02e04b461e5..a82846dd006 100644
--- a/src/util/merge_irep.cpp
+++ b/src/util/merge_irep.cpp
@@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const
         result, static_cast<const merged_irept &>(it->second).hash());
   }
 
-  result=hash_finalize(result, named_sub.size()+sub.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   return result;
 }
@@ -44,9 +50,16 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
   const irept::named_subt &o_named_sub=other.get_named_sub();
 
   if(sub.size()!=o_sub.size())
-    return true;
+    return false;
+#ifdef SUB_IS_LIST
+  if(
+    std::distance(named_sub.begin(), named_sub.end()) !=
+    std::distance(o_named_sub.begin(), o_named_sub.end()))
+    return false;
+#else
   if(named_sub.size()!=o_named_sub.size())
-    return true;
+    return false;
+#endif
 
   {
     irept::subt::const_iterator s_it=sub.begin();
@@ -95,13 +108,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
     to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
@@ -140,24 +159,36 @@ const irept &merge_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   const irept::named_subt &src_comments=irep.get_comments();
   irept::named_subt &dest_comments=new_irep.get_comments();
 
+#ifdef SUB_IS_LIST
+  before = dest_comments.before_begin();
+#endif
   forall_named_irep(it, src_comments)
+  {
     #ifdef SUB_IS_LIST
-    dest_comments.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_comments.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_comments[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   return *irep_store.insert(new_irep).first;
 }
@@ -188,24 +219,36 @@ const irept &merge_full_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   const irept::named_subt &src_comments=irep.get_comments();
   irept::named_subt &dest_comments=new_irep.get_comments();
 
+#ifdef SUB_IS_LIST
+  before = dest_comments.before_begin();
+#endif
   forall_named_irep(it, src_comments)
+  {
     #ifdef SUB_IS_LIST
-    dest_comments.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_comments.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_comments[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   return *irep_store.insert(new_irep).first;
 }
diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp
index ea97126f19e..50f7a4e7556 100644
--- a/unit/util/irep.cpp
+++ b/unit/util/irep.cpp
@@ -141,11 +141,15 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       irept irep2("second_irep");
       irep.add("a_new_element", irep2);
       REQUIRE(irep.find("a_new_element").id() == "second_irep");
-      REQUIRE(irep.get_named_sub().size() == 1);
+      std::size_t named_sub_size = std::distance(
+        irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 1);
 
       irep.add("#a_comment", irep2);
       REQUIRE(irep.find("#a_comment").id() == "second_irep");
-      REQUIRE(irep.get_comments().size() == 1);
+      std::size_t comments_size =
+        std::distance(irep.get_comments().begin(), irep.get_comments().end());
+      REQUIRE(comments_size == 1);
 
       irept bak(irep);
       irep.remove("no_such_id");
@@ -159,19 +163,29 @@ SCENARIO("irept_memory", "[core][utils][irept]")
 
       irep.move_to_named_sub("another_entry", irep2);
       REQUIRE(irep.get_sub().size() == 1);
-      REQUIRE(irep.get_named_sub().size() == 1);
-      REQUIRE(irep.get_comments().size() == 1);
+      named_sub_size = std::distance(
+        irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 1);
+      comments_size =
+        std::distance(irep.get_comments().begin(), irep.get_comments().end());
+      REQUIRE(comments_size == 1);
 
       irept irep3;
       irep.move_to_named_sub("#a_comment", irep3);
       REQUIRE(irep.find("#a_comment").id().empty());
       REQUIRE(irep.get_sub().size() == 1);
-      REQUIRE(irep.get_named_sub().size() == 1);
-      REQUIRE(irep.get_comments().size() == 1);
+      named_sub_size = std::distance(
+        irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 1);
+      comments_size =
+        std::distance(irep.get_comments().begin(), irep.get_comments().end());
+      REQUIRE(comments_size == 1);
 
       irept irep4;
       irep.move_to_named_sub("#another_comment", irep4);
-      REQUIRE(irep.get_comments().size() == 2);
+      comments_size =
+        std::distance(irep.get_comments().begin(), irep.get_comments().end());
+      REQUIRE(comments_size == 2);
     }
 
     THEN("Setting and getting works")

From 28255e42e1f51c9bb593c95da3511682333710b2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Mon, 26 Dec 2016 12:30:50 +0000
Subject: [PATCH 22/33] Avoid repeated hash computation, reduce irept::dt size

On SV-COMP benchmarks, hashing accounts for >22% of CPU time (with
profiling enabled).
---
 src/util/irep.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/irep.h b/src/util/irep.h
index 464651ba8cf..3398ddfb947 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "irep_ids.h"
 
 #define SHARING
-// #define HASH_CODE
+#define HASH_CODE
 #define USE_MOVE
-// #define SUB_IS_LIST
+#define SUB_IS_LIST
 
 #ifdef SUB_IS_LIST
 #include <forward_list>

From 7d439f4a3913cd51e2baf6f9a08b33259861907f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 25 Nov 2018 08:06:43 +0000
Subject: [PATCH 23/33] C library: model pthread_key_create,
 pthread_{get,set}specific

This is used by pthread-divine/tls_basic_true-unreach-call in SV-COMP.
---
 .../constant_propagation_01/test.desc         |   4 +-
 .../constant_propagation_02/test.desc         |   4 +-
 src/ansi-c/ansi_c_internal_additions.cpp      |   6 +
 src/ansi-c/library/pthread_lib.c              | 127 ++++++++++++++++--
 src/cpp/cpp_internal_additions.cpp            |  10 ++
 5 files changed, 137 insertions(+), 14 deletions(-)

diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
index a4a79f28ab1..f7de54ad46b 100644
--- a/regression/goto-analyzer/constant_propagation_01/test.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
index 6a28820a4b0..47aea19e28b 100644
--- a/regression/goto-analyzer/constant_propagation_02/test.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index b22dafa554e..74196f2b8dc 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -136,6 +136,12 @@ void ansi_c_internal_additions(std::string &code)
     CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
       CPROVER_PREFIX "constant_infinity_uint];\n"
     "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
+    CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
+    CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors["
+      CPROVER_PREFIX "constant_infinity_uint])(void *);\n"
+    CPROVER_PREFIX "thread_local unsigned long "
+      CPROVER_PREFIX "next_thread_key = 0;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 97194052a54..77a2d341ab5 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -293,10 +293,21 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex)
 extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*);
+extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+
 inline void pthread_exit(void *value_ptr)
 {
   __CPROVER_HIDE:;
   if(value_ptr!=0) (void)*(char*)value_ptr;
+  for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
+  {
+    const void *key = __CPROVER_thread_keys[i];
+    __CPROVER_thread_keys[i] = 0;
+    if(__CPROVER_thread_key_dtors[i] && key)
+      __CPROVER_thread_key_dtors[i](key);
+  }
   __CPROVER_threads_exited[__CPROVER_thread_id]=1;
   __CPROVER_assume(0);
 }
@@ -522,6 +533,40 @@ extern __CPROVER_bool __CPROVER_threads_exited[];
 extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
 extern unsigned long __CPROVER_next_thread_id;
 
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*);
+extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+
+inline void __spawned_thread(
+  unsigned long this_thread_id,
+  void (**thread_key_dtors)(void*),
+  unsigned long next_thread_key,
+  void * (*start_routine)(void *),
+  void *arg)
+{
+  __CPROVER_HIDE:;
+  __CPROVER_thread_id = this_thread_id;
+  __CPROVER_next_thread_key = next_thread_key;
+  for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
+    __CPROVER_thread_key_dtors[i] = thread_key_dtors[i];
+  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+  // Clear all locked mutexes; locking must happen in same thread.
+  __CPROVER_clear_must(0, "mutex-locked");
+  __CPROVER_clear_may(0, "mutex-locked");
+  #endif
+  start_routine(arg);
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
+                  "WWcumul", "RRcumul", "RWcumul", "WRcumul");
+  for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
+  {
+    const void *key = __CPROVER_thread_keys[i];
+    __CPROVER_thread_keys[i] = 0;
+    if(__CPROVER_thread_key_dtors[i] && key)
+      __CPROVER_thread_key_dtors[i](key);
+  }
+  __CPROVER_threads_exited[this_thread_id] = 1;
+}
+
 inline int pthread_create(
   pthread_t *thread, // must not be null
   const pthread_attr_t *attr, // may be null
@@ -543,17 +588,12 @@ inline int pthread_create(
 
   if(attr) (void)*attr;
 
+  unsigned long next_thread_key = __CPROVER_next_thread_key;
+  void (**thread_key_dtors)(void*) = __CPROVER_thread_key_dtors;
+
   __CPROVER_ASYNC_1:
-    __CPROVER_thread_id=this_thread_id,
-    #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-    // Clear all locked mutexes; locking must happen in same thread.
-    __CPROVER_clear_must(0, "mutex-locked"),
-    __CPROVER_clear_may(0, "mutex-locked"),
-    #endif
-    start_routine(arg),
-    __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
-                    "WWcumul", "RRcumul", "RWcumul", "WRcumul"),
-    __CPROVER_threads_exited[this_thread_id]=1;
+    __spawned_thread(
+      this_thread_id, thread_key_dtors, next_thread_key, start_routine, arg);
 
   return 0;
 }
@@ -807,3 +847,70 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier)
   return result;
 }
 #endif
+
+/* FUNCTION: pthread_key_create */
+
+#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#include <pthread.h>
+#define __CPROVER_PTHREAD_H_INCLUDED
+#endif
+
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void*);
+extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+
+inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void*))
+{
+  __CPROVER_HIDE:;
+  __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0;
+  __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor;
+  *key = __CPROVER_next_thread_key++;
+  return 0;
+}
+
+/* FUNCTION: pthread_key_delete */
+
+#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#include <pthread.h>
+#define __CPROVER_PTHREAD_H_INCLUDED
+#endif
+
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+
+inline int pthread_key_delete(pthread_key_t key)
+{
+  __CPROVER_HIDE:;
+  __CPROVER_thread_keys[key] = 0;
+  return 0;
+}
+
+/* FUNCTION: pthread_getspecific */
+
+#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#include <pthread.h>
+#define __CPROVER_PTHREAD_H_INCLUDED
+#endif
+
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+
+inline void* pthread_getspecific(pthread_key_t key)
+{
+  __CPROVER_HIDE:;
+  return (void *)__CPROVER_thread_keys[key];
+}
+
+/* FUNCTION: pthread_setspecific */
+
+#ifndef __CPROVER_PTHREAD_H_INCLUDED
+#include <pthread.h>
+#define __CPROVER_PTHREAD_H_INCLUDED
+#endif
+
+extern __CPROVER_thread_local const void* __CPROVER_thread_keys[];
+
+inline int pthread_setspecific(pthread_key_t key, const void *value)
+{
+  __CPROVER_HIDE:;
+  __CPROVER_thread_keys[key] = value;
+  return 0;
+}
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index f62f0880a25..e1cea42ea9a 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -72,6 +72,16 @@ void cpp_internal_additions(std::ostream &out)
       << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];"
       << '\n';
   out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n';
+  // TODO: thread_local is still broken
+  out << "void* "
+      << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];"
+      << '\n';
+  // TODO: thread_local is still broken
+  out << "void (*"
+      << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])"
+      << "(void *);" << '\n';
+  // TODO: thread_local is still broken
+  out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n';
   out << "extern unsigned char "
       << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n';
 

From 53e4f609c97ce29b59c2b21d0ea4f31c3843c97f Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 24 Nov 2018 09:43:57 +0000
Subject: [PATCH 24/33] Factor out memory leak instrumentation into separate
 function

---
 src/analyses/goto_check.cpp | 52 +++++++++++++++++++++----------------
 1 file changed, 29 insertions(+), 23 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index fa7eafe7253..2421635c74d 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -103,6 +103,7 @@ class goto_checkt
 
   void bounds_check(const index_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
+  void memory_leak_check(const irep_idt &function_id);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const exprt &, const guardt &);
@@ -1515,6 +1516,30 @@ void goto_checkt::rw_ok_check(exprt &expr)
   }
 }
 
+void goto_checkt::memory_leak_check(const irep_idt &function_id)
+{
+  const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
+  const symbol_exprt leak_expr = leak.symbol_expr();
+
+  // add self-assignment to get helpful counterexample output
+  goto_programt::targett t = new_code.add_instruction();
+  t->make_assignment();
+  t->code = code_assignt(leak_expr, leak_expr);
+
+  source_locationt source_location;
+  source_location.set_function(function_id);
+
+  equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
+
+  add_guarded_claim(
+    eq,
+    "dynamically allocated memory never freed",
+    "memory-leak",
+    source_location,
+    eq,
+    guardt());
+}
+
 void goto_checkt::goto_check(
   goto_functiont &goto_function,
   const irep_idt &_mode)
@@ -1741,30 +1766,11 @@ void goto_checkt::goto_check(
     }
     else if(i.is_end_function())
     {
-      if(i.function==goto_functionst::entry_point() &&
-         enable_memory_leak_check)
+      if(
+        i.function == goto_functionst::entry_point() &&
+        enable_memory_leak_check)
       {
-        const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
-        const symbol_exprt leak_expr=leak.symbol_expr();
-
-        // add self-assignment to get helpful counterexample output
-        goto_programt::targett t=new_code.add_instruction();
-        t->make_assignment();
-        t->code=code_assignt(leak_expr, leak_expr);
-
-        source_locationt source_location;
-        source_location.set_function(i.function);
-
-        equal_exprt eq(
-          leak_expr,
-          null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_claim(
-          eq,
-          "dynamically allocated memory never freed",
-          "memory-leak",
-          source_location,
-          eq,
-          guardt());
+        memory_leak_check(i.function);
       }
     }
 

From 1672dbcffce7b2a2c587fce36a804eb5be0caff7 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 24 Nov 2018 15:14:35 +0000
Subject: [PATCH 25/33] Add memory leak instrumentation to abort and exit

---
 regression/cbmc/Memory_leak_abort/main.c    | 16 ++++++++++++++++
 regression/cbmc/Memory_leak_abort/test.desc | 12 ++++++++++++
 scripts/delete_failing_smt2_solver_tests    |  1 +
 src/analyses/goto_check.cpp                 |  9 +++++++++
 4 files changed, 38 insertions(+)
 create mode 100644 regression/cbmc/Memory_leak_abort/main.c
 create mode 100644 regression/cbmc/Memory_leak_abort/test.desc

diff --git a/regression/cbmc/Memory_leak_abort/main.c b/regression/cbmc/Memory_leak_abort/main.c
new file mode 100644
index 00000000000..1d0f062e0a7
--- /dev/null
+++ b/regression/cbmc/Memory_leak_abort/main.c
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  if(*p == 0)
+    abort();
+  if(*p == 1)
+    exit(1);
+  if(*p == 2)
+    _Exit(1);
+  free(p);
+  return 0;
+}
diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/regression/cbmc/Memory_leak_abort/test.desc
new file mode 100644
index 00000000000..355cc9690b8
--- /dev/null
+++ b/regression/cbmc/Memory_leak_abort/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--memory-leak-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+_Exit\.memory-leak\.1.*FAILURE
+__CPROVER__start\.memory-leak\.1.*SUCCESS
+abort\.memory-leak\.1.*FAILURE
+exit\.memory-leak\.1.*FAILURE
+--
+^warning: ignoring
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index c47cd9128e7..b7c6fc1e7ba 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -53,6 +53,7 @@ rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
+rm Memory_leak_abort/test.desc
 rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Multi_Dimensional_Array3/test.desc
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 2421635c74d..1e11dacc423 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1703,6 +1703,15 @@ void goto_checkt::goto_check(
     }
     else if(i.is_assume())
     {
+      // These are further 'exit points' of the program
+      const exprt simplified_guard = simplify_expr(i.guard, ns);
+      if(
+        enable_memory_leak_check && simplified_guard.is_false() &&
+        (i.function == "abort" || i.function == "exit" ||
+         i.function == "_Exit"))
+      {
+        memory_leak_check(i.function);
+      }
       if(!enable_assumptions)
       {
         i.make_skip();

From 7e3b18a18d3fef1fda032e18c01a4d1ce3b9c591 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 24 Nov 2018 17:15:14 +0000
Subject: [PATCH 26/33] Fix memory leak check for __VERIFIER_error

---
 regression/cbmc/Memory_leak_abort/main.c    | 4 +++-
 regression/cbmc/Memory_leak_abort/test.desc | 4 +++-
 src/analyses/goto_check.cpp                 | 3 ++-
 src/goto-programs/builtin_functions.cpp     | 1 +
 4 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc/Memory_leak_abort/main.c b/regression/cbmc/Memory_leak_abort/main.c
index 1d0f062e0a7..2db9de9621b 100644
--- a/regression/cbmc/Memory_leak_abort/main.c
+++ b/regression/cbmc/Memory_leak_abort/main.c
@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_error() __attribute__((__noreturn__));
 
 int main()
 {
@@ -11,6 +11,8 @@ int main()
     exit(1);
   if(*p == 2)
     _Exit(1);
+  if(*p == 3)
+    __VERIFIER_error();
   free(p);
   return 0;
 }
diff --git a/regression/cbmc/Memory_leak_abort/test.desc b/regression/cbmc/Memory_leak_abort/test.desc
index 355cc9690b8..778831b5ce3 100644
--- a/regression/cbmc/Memory_leak_abort/test.desc
+++ b/regression/cbmc/Memory_leak_abort/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---memory-leak-check
+--memory-leak-check --no-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
@@ -8,5 +8,7 @@ _Exit\.memory-leak\.1.*FAILURE
 __CPROVER__start\.memory-leak\.1.*SUCCESS
 abort\.memory-leak\.1.*FAILURE
 exit\.memory-leak\.1.*FAILURE
+main\.memory-leak\.1.*FAILURE
 --
+main\.assertion\.1.*FAILURE
 ^warning: ignoring
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 1e11dacc423..ffdff96f7be 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1708,7 +1708,8 @@ void goto_checkt::goto_check(
       if(
         enable_memory_leak_check && simplified_guard.is_false() &&
         (i.function == "abort" || i.function == "exit" ||
-         i.function == "_Exit"))
+         i.function == "_Exit" ||
+         (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
       {
         memory_leak_check(i.function);
       }
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index a638c1d094e..c6f9100d22b 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -711,6 +711,7 @@ void goto_convertt::do_function_call_symbol(
     // are being checked
     goto_programt::targett a=dest.add_instruction(ASSUME);
     a->guard=false_exprt();
+    a->labels.push_back("__VERIFIER_abort");
     a->source_location=function.source_location();
     a->source_location.set("user-provided", true);
   }

From 4d6d81f2fbfa020189d3f577e32468b5fd7ef52f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Tue, 27 Dec 2016 02:41:18 +0000
Subject: [PATCH 27/33] Needs more profiling: Do not sort operands as part of
 simplification

---
 src/util/simplify_expr.cpp  | 2 +-
 src/util/simplify_utils.cpp | 5 +++--
 src/util/simplify_utils.h   | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 3be87c69f00..9716c550d0f 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2127,7 +2127,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
 
   bool result=true;
 
-  result=sort_and_join(expr) && result;
+  result = sort_and_join(expr, false) && result;
 
   if(expr.id()==ID_typecast)
     result=simplify_typecast(expr) && result;
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 53b2f38f7e1..83e086e6959 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -119,7 +119,7 @@ static const struct saj_tablet &sort_and_join(
   return saj_table[i];
 }
 
-bool sort_and_join(exprt &expr)
+bool sort_and_join(exprt &expr, bool do_sort)
 {
   bool result=true;
 
@@ -158,8 +158,9 @@ bool sort_and_join(exprt &expr)
   }
 
   // sort it
+  if(do_sort)
+    result = sort_operands(new_ops) && result;
 
-  result=sort_operands(new_ops) && result;
   expr.operands().swap(new_ops);
 
   return result;
diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h
index 33e294f4e96..6f0af7865b9 100644
--- a/src/util/simplify_utils.h
+++ b/src/util/simplify_utils.h
@@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool sort_operands(exprt::operandst &operands);
 
-bool sort_and_join(exprt &expr);
+bool sort_and_join(exprt &expr, bool do_sort=true);
 
 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H

From ca9673f0d95847c31344e046d98c5f586d36fcc4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 26 Nov 2018 14:37:41 +0000
Subject: [PATCH 28/33] Detect use of free() with alloca-allocated objects

As we internally use dynamic allocation, we previously did not distinguish
alloca-allocated from malloc/calloc-allocated ones.
---
 regression/cbmc/alloca1/main.c           |  8 ++++++++
 regression/cbmc/alloca1/test.desc        | 10 ++++++++++
 src/ansi-c/ansi_c_internal_additions.cpp |  1 +
 src/ansi-c/library/stdlib.c              | 11 +++++++++++
 src/cpp/cpp_internal_additions.cpp       |  1 +
 5 files changed, 31 insertions(+)
 create mode 100644 regression/cbmc/alloca1/main.c
 create mode 100644 regression/cbmc/alloca1/test.desc

diff --git a/regression/cbmc/alloca1/main.c b/regression/cbmc/alloca1/main.c
new file mode 100644
index 00000000000..bc30d7624a1
--- /dev/null
+++ b/regression/cbmc/alloca1/main.c
@@ -0,0 +1,8 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = alloca(sizeof(int));
+  *p = 42;
+  free(p);
+}
diff --git a/regression/cbmc/alloca1/test.desc b/regression/cbmc/alloca1/test.desc
new file mode 100644
index 00000000000..66fa40a9537
--- /dev/null
+++ b/regression/cbmc/alloca1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+free called for stack-allocated object: FAILURE$
+^\*\* 1 of 12 failed
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 74196f2b8dc..99102773d75 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -154,6 +154,7 @@ void ansi_c_internal_additions(std::string &code)
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
+    "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index c2576c179ec..39739733553 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -128,6 +128,7 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 /* FUNCTION: __builtin_alloca */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+extern void *__CPROVER_alloca_object;
 
 inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
@@ -144,6 +145,10 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   __CPROVER_malloc_size=record_malloc?alloca_size:__CPROVER_malloc_size;
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
 
+  // record alloca to detect invalid free
+  __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
+  __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
+
   return res;
 }
 
@@ -164,6 +169,7 @@ inline void *alloca(__CPROVER_size_t alloca_size)
 #undef free
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+extern void *__CPROVER_alloca_object;
 
 inline void free(void *ptr)
 {
@@ -185,6 +191,11 @@ inline void free(void *ptr)
                          !__CPROVER_malloc_is_new_array,
                          "free called for new[] object");
 
+  // catch people who try to use free(...) with alloca
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_alloca_object != ptr,
+    "free called for stack-allocated object");
+
   if(ptr!=0)
   {
     // non-deterministically record as deallocated
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index e1cea42ea9a..b1a376f455d 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -95,6 +95,7 @@ void cpp_internal_additions(std::ostream &out)
   out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
   out << "void *" CPROVER_PREFIX "allocate("
       << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
+  out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n';
 
   // auxiliaries for new/delete
   out << "void *__new(__CPROVER::size_t);" << '\n';

From bc2c2be113bb29b34be3b2ff6d1046658558cd77 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 26 Nov 2018 18:12:31 +0000
Subject: [PATCH 29/33] pthread_cond_wait may return spuriously

---
 src/ansi-c/library/pthread_lib.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 77a2d341ab5..c608deae963 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -674,8 +674,8 @@ inline int pthread_cond_wait(
   #endif
 
   __CPROVER_atomic_begin();
-  __CPROVER_assume(*((unsigned *)cond));
-  (*((unsigned *)cond))--;
+  if(*((unsigned *)cond))
+    (*((unsigned *)cond))--;
   __CPROVER_atomic_end();
 
   return 0; // we never fail

From 443dfdbd56c43f10a2015273a3e1c1151e10b3f8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 27 Nov 2018 06:20:37 +0000
Subject: [PATCH 30/33] Don't implement pthread_keyt destructors

They are too expensive due to extensive shared-variable use.
---
 src/ansi-c/library/pthread_lib.c | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index c608deae963..e8c25a4a009 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -301,6 +301,7 @@ inline void pthread_exit(void *value_ptr)
 {
   __CPROVER_HIDE:;
   if(value_ptr!=0) (void)*(char*)value_ptr;
+#if 0
   for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
   {
     const void *key = __CPROVER_thread_keys[i];
@@ -308,6 +309,7 @@ inline void pthread_exit(void *value_ptr)
     if(__CPROVER_thread_key_dtors[i] && key)
       __CPROVER_thread_key_dtors[i](key);
   }
+#endif
   __CPROVER_threads_exited[__CPROVER_thread_id]=1;
   __CPROVER_assume(0);
 }
@@ -539,7 +541,7 @@ extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
 
 inline void __spawned_thread(
   unsigned long this_thread_id,
-  void (**thread_key_dtors)(void*),
+  // void (**thread_key_dtors)(void*),
   unsigned long next_thread_key,
   void * (*start_routine)(void *),
   void *arg)
@@ -547,8 +549,10 @@ inline void __spawned_thread(
   __CPROVER_HIDE:;
   __CPROVER_thread_id = this_thread_id;
   __CPROVER_next_thread_key = next_thread_key;
+#if 0
   for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
     __CPROVER_thread_key_dtors[i] = thread_key_dtors[i];
+#endif
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   // Clear all locked mutexes; locking must happen in same thread.
   __CPROVER_clear_must(0, "mutex-locked");
@@ -557,6 +561,7 @@ inline void __spawned_thread(
   start_routine(arg);
   __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
                   "WWcumul", "RRcumul", "RWcumul", "WRcumul");
+#if 0
   for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i)
   {
     const void *key = __CPROVER_thread_keys[i];
@@ -564,6 +569,7 @@ inline void __spawned_thread(
     if(__CPROVER_thread_key_dtors[i] && key)
       __CPROVER_thread_key_dtors[i](key);
   }
+#endif
   __CPROVER_threads_exited[this_thread_id] = 1;
 }
 
@@ -589,11 +595,15 @@ inline int pthread_create(
   if(attr) (void)*attr;
 
   unsigned long next_thread_key = __CPROVER_next_thread_key;
-  void (**thread_key_dtors)(void*) = __CPROVER_thread_key_dtors;
+  // void (**thread_key_dtors)(void*) = __CPROVER_thread_key_dtors;
 
   __CPROVER_ASYNC_1:
     __spawned_thread(
-      this_thread_id, thread_key_dtors, next_thread_key, start_routine, arg);
+      this_thread_id,
+      // thread_key_dtors,
+      next_thread_key,
+      start_routine,
+      arg);
 
   return 0;
 }
@@ -863,7 +873,8 @@ inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void*))
 {
   __CPROVER_HIDE:;
   __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0;
-  __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor;
+  // __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor;
+  __CPROVER_precondition(destructor == 0, "destructors are not yet supported");
   *key = __CPROVER_next_thread_key++;
   return 0;
 }

From f2139d33970a9c2b6c54c875f056e5b4bd0f1674 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 May 2018 11:50:29 +0100
Subject: [PATCH 31/33] Non-deterministic initialisation of argc/argv/envp

---
 regression/goto-instrument/print_global_state_size1/main.c | 2 +-
 src/ansi-c/c_typecheck_argc_argv.cpp                       | 4 ++++
 src/linking/static_lifetime_init.cpp                       | 6 +-----
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/regression/goto-instrument/print_global_state_size1/main.c b/regression/goto-instrument/print_global_state_size1/main.c
index 68f16e02519..08f28f20724 100644
--- a/regression/goto-instrument/print_global_state_size1/main.c
+++ b/regression/goto-instrument/print_global_state_size1/main.c
@@ -3,7 +3,7 @@
 uint32_t some_global_var;
 int8_t other_global_var;
 
-int main(int argc, char *argv[])
+int main()
 {
   return 0;
 }
diff --git a/src/ansi-c/c_typecheck_argc_argv.cpp b/src/ansi-c/c_typecheck_argc_argv.cpp
index dfc752c8e19..7ff32a4810d 100644
--- a/src/ansi-c/c_typecheck_argc_argv.cpp
+++ b/src/ansi-c/c_typecheck_argc_argv.cpp
@@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argc_symbol.type=op0.type();
     argc_symbol.is_static_lifetime=true;
     argc_symbol.is_lvalue=true;
+    argc_symbol.value = side_effect_expr_nondett(op0.type());
 
     if(argc_symbol.type.id()!=ID_signedbv &&
        argc_symbol.type.id()!=ID_unsignedbv)
@@ -81,6 +82,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argv_symbol.type=argv_type;
     argv_symbol.is_static_lifetime=true;
     argv_symbol.is_lvalue=true;
+    argv_symbol.value = side_effect_expr_nondett(argv_type);
 
     symbolt *argv_new_symbol;
     move_symbol(argv_symbol, argv_new_symbol);
@@ -99,6 +101,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     envp_size_symbol.name="envp_size'";
     envp_size_symbol.type=op0.type(); // same type as argc!
     envp_size_symbol.is_static_lifetime=true;
+    envp_size_symbol.value = side_effect_expr_nondett(op0.type());
     move_symbol(envp_size_symbol, envp_new_size_symbol);
 
     if(envp_symbol.type.id()!=ID_pointer)
@@ -113,6 +116,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
 
     envp_symbol.type.id(ID_array);
     envp_symbol.type.add(ID_size).swap(size_expr);
+    envp_symbol.value = side_effect_expr_nondett(envp_symbol.type);
 
     symbolt *envp_new_symbol;
     move_symbol(envp_symbol, envp_new_symbol);
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index b9bb0828e64..995910183a5 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -67,11 +67,7 @@ void static_lifetime_init(
        identifier==CPROVER_PREFIX "memory" ||
        identifier=="__func__" ||
        identifier=="__FUNCTION__" ||
-       identifier=="__PRETTY_FUNCTION__" ||
-       identifier=="argc'" ||
-       identifier=="argv'" ||
-       identifier=="envp'" ||
-       identifier=="envp_size'")
+       identifier=="__PRETTY_FUNCTION__")
       continue;
 
     // just for linking

From 95f18597112bab912e5cbeda888141eb028499da Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 4 Oct 2018 07:42:54 +0000
Subject: [PATCH 32/33] clang-format cleanup

---
 src/linking/static_lifetime_init.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index 995910183a5..5120dfafd0e 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -63,12 +63,13 @@ void static_lifetime_init(
       continue;
 
     // special values
-    if(identifier==CPROVER_PREFIX "constant_infinity_uint" ||
-       identifier==CPROVER_PREFIX "memory" ||
-       identifier=="__func__" ||
-       identifier=="__FUNCTION__" ||
-       identifier=="__PRETTY_FUNCTION__")
+    if(
+      identifier == CPROVER_PREFIX "constant_infinity_uint" ||
+      identifier == CPROVER_PREFIX "memory" || identifier == "__func__" ||
+      identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__")
+    {
       continue;
+    }
 
     // just for linking
     if(has_prefix(id, CPROVER_PREFIX "architecture_"))

From ce20fbe64eea81751a246cad22c9d681c97b2537 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 May 2018 11:59:23 +0100
Subject: [PATCH 33/33] Skip phi assignment if one of the merged states has an
 uninitialised object

With level-2 counters incremented on declaration and non-deterministic
initialisation upon allocation, the only remaining sources are pointer
dereferencing, where uninitialised objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077d2e. Removing only the code
introduced in 369f077d2e would yield a wrong result for
regression/cbmc/Local_out_of_scope3.
---
 src/goto-symex/symex_assign.cpp | 11 -----------
 src/goto-symex/symex_goto.cpp   | 22 ++++++++++++++--------
 2 files changed, 14 insertions(+), 19 deletions(-)

diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 03a2819b3e2..bb49c557e4b 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -218,17 +218,6 @@ void goto_symext::symex_assign_symbol(
   guardt &guard,
   assignment_typet assignment_type)
 {
-  // do not assign to L1 objects that have gone out of scope --
-  // pointer dereferencing may yield such objects; parameters do not
-  // have an L2 entry set up beforehand either, so exempt them from
-  // this check (all other L1 objects should have seen a declaration)
-  const symbolt *s;
-  if(!ns.lookup(lhs.get_object_name(), s) &&
-     !s->is_parameter &&
-     !lhs.get_level_1().empty() &&
-     state.level2.current_count(lhs.get_identifier())==0)
-    return;
-
   exprt ssa_rhs=rhs;
 
   // put assignment guard into the rhs
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index ec7f61a3f43..d2524cfc111 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -452,17 +452,23 @@ void goto_symext::phi_function(
     //  1. Either guard is false, so we can't follow that branch.
     //  2. Either identifier is of generation zero, and so hasn't been
     //     initialized and therefor an invalid target.
-    if(dest_state.guard.is_false())
-      rhs=goto_state_rhs;
-    else if(goto_state.guard.is_false())
-      rhs=dest_state_rhs;
-    else if(goto_state.level2_current_count(l1_identifier) == 0)
+    if(
+      dest_state.guard.is_false() ||
+      dest_state.level2.current_count(l1_identifier) == 0)
     {
-      rhs = dest_state_rhs;
+      if(goto_state.level2_current_count(l1_identifier) == 0)
+        continue;
+
+      rhs = goto_state_rhs;
     }
-    else if(dest_state.level2.current_count(l1_identifier) == 0)
+    else if(
+      goto_state.guard.is_false() ||
+      goto_state.level2_current_count(l1_identifier) == 0)
     {
-      rhs = goto_state_rhs;
+      if(dest_state.level2.current_count(l1_identifier) == 0)
+        continue;
+
+      rhs = dest_state_rhs;
     }
     else
     {