diffblue · peterschrammel · Mar 12, 2021 · Mar 3, 2021 · Mar 3, 2021
diff --git a/lib/cbmc b/lib/cbmc
diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc
@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.11\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.15\] dereference failure: deallocated dynamic object in \*p: FAILURE
diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc
@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.23\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.33\] dereference failure: deallocated dynamic object in \*p: FAILURE
diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
@@ -125,7 +125,7 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("slice", false);
 
   // all checks supported by goto_check
-  GOTO_CHECK_PARSE_OPTIONS(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
   // check assertions
   if(cmdline.isset("no-assertions"))
@@ -1087,10 +1087,14 @@ bool twols_parse_optionst::process_goto_program(
       goto_inlinet goto_inline(
         goto_model.goto_functions,
         ns,
-        ui_message_handler);
+        ui_message_handler,
+        false);
       goto_inline();
 #if IGNORE_RECURSION
       recursion_detected=goto_inline.recursion_detected();
+      // since CBMC 5.7, inlining doesn't update location and loop numbers
+      goto_model.goto_functions.update();
+      goto_model.goto_functions.compute_loop_numbers();
 #endif
     }
 
@@ -1559,7 +1563,7 @@ void twols_parse_optionst::help()
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
     "Program instrumentation options:\n"
-    GOTO_CHECK_HELP
+    HELP_GOTO_CHECK
     " --error-label label          check that label is unreachable\n"
     " --show-properties            show the properties\n"
     " --no-assertions              ignore user assertions\n"

diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h
@@ -31,7 +31,7 @@ class optionst;
   "(function):" \
   "D:I:" \
   "(depth):(context-bound):(unwind):" \
-  GOTO_CHECK_OPTIONS \
+  OPT_GOTO_CHECK \
   "(non-incremental)" \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \

diff --git a/src/2ls/dynamic_cfg.h b/src/2ls/dynamic_cfg.h
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 
 #include <util/std_expr.h>
 #include <util/graph.h>
-#include <util/i2string.h>
 #include <goto-programs/goto_program.h>
 
 #include <ssa/ssa_unwinder.h>
@@ -35,9 +34,9 @@ struct dynamic_cfg_idt
   std::string to_string() const
   {
     std::ostringstream sid;
-    sid << i2string(pc->location_number);
+    sid << std::to_string(pc->location_number);
     for(const auto &i : iteration_stack)
-      sid << "." <<i2string(i);
+      sid << "." <<std::to_string(i);
     return sid.str();
   }
 };
@@ -51,7 +50,7 @@ struct dynamic_cfg_nodet:public graph_nodet<dynamic_cfg_edget>
   exprt assumption;
 };
 
-class dynamic_cfgt:public graph<dynamic_cfg_nodet>
+class dynamic_cfgt:public grapht<dynamic_cfg_nodet>
 {
 public:
   inline dynamic_cfg_nodet& operator[](const dynamic_cfg_idt &id)

diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp
@@ -190,7 +190,7 @@ void twols_parse_optionst::remove_multiple_dereferences(
       {
         symbolt new_symbol;
         new_symbol.type=member_expr.type();
-        new_symbol.name="$deref"+i2string(var_counter++);
+        new_symbol.name="$deref"+std::to_string(var_counter++);
         new_symbol.base_name=new_symbol.name;
         new_symbol.pretty_name=new_symbol.name;
         goto_model.symbol_table.add(new_symbol);
@@ -465,7 +465,7 @@ void twols_parse_optionst::split_same_symbolic_object_assignments(
           {
             symbolt tmp_symbol;
             tmp_symbol.type=assign.lhs().type();
-            tmp_symbol.name="$symderef_tmp"+i2string(counter++);
+            tmp_symbol.name="$symderef_tmp"+std::to_string(counter++);
             tmp_symbol.base_name=tmp_symbol.name;
             tmp_symbol.pretty_name=tmp_symbol.name;
 

diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/options.h>
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/string2int.h>
 
 #include <goto-programs/read_goto_binary.h>

diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp
@@ -12,7 +12,6 @@ Author: Peter Schrammel
 #include <iostream>
 
 #include <util/options.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/language_util.h>
 #include <util/prefix.h>

diff --git a/src/2ls/summary_checker_nonterm.cpp b/src/2ls/summary_checker_nonterm.cpp
@@ -11,7 +11,6 @@ Author: Stefan Marticek
 
 #include "summary_checker_nonterm.h"
 
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <util/prefix.h>
 

diff --git a/src/2ls/version.h b/src/2ls/version.h
@@ -12,6 +12,6 @@ Author: Peter Schrammel
 #ifndef CPROVER_2LS_2LS_VERSION_H
 #define CPROVER_2LS_2LS_VERSION_H
 
-#define TWOLS_VERSION "0.9.1"
+#define TWOLS_VERSION "0.9.2"
 
 #endif
diff --git a/src/domains/domain.h b/src/domains/domain.h
@@ -16,7 +16,6 @@ Author: Peter Schrammel
 #include <set>
 
 #include <util/std_expr.h>
-#include <util/i2string.h>
 #include <langapi/language_util.h>
 #include <util/replace_expr.h>
 #include <util/namespace.h>

diff --git a/src/domains/incremental_solver.cpp b/src/domains/incremental_solver.cpp
@@ -16,7 +16,6 @@ Author: Peter Schrammel
 #include <set>
 
 #include <solvers/flattening/bv_pointers.h>
-#include <util/i2string.h>
 
 #include "incremental_solver.h"
 
@@ -35,7 +34,7 @@ void incremental_solvert::new_context()
     solver->convert(
       symbol_exprt(
         "goto_symex::\\act$"+
-        i2string(activation_literal_counter++), bool_typet()));
+        std::to_string(activation_literal_counter++), bool_typet()));
 
 #ifdef DEBUG_OUTPUT
     debug() << "new context: " << activation_literal<< eom;

diff --git a/src/domains/lexlinrank_domain.cpp b/src/domains/lexlinrank_domain.cpp
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -372,7 +371,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
 
     symb_values[elm].c[0]=symbol_exprt(
       SYMB_COEFF_VAR+std::string("c!")+
-      i2string(row)+"$"+i2string(elm)+"$0",
+      std::to_string(row)+"$"+std::to_string(elm)+"$0",
       signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 
 #ifdef DIFFERENCE_ENCODING
@@ -388,7 +387,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint(
     {
       symb_values[elm].c[i]=symbol_exprt(
         SYMB_COEFF_VAR+std::string("c!")+
-        i2string(row)+"$"+i2string(elm)+"$"+i2string(i),
+        std::to_string(row)+"$"+std::to_string(elm)+"$"+std::to_string(i),
         signedbv_typet(COEFF_C_SIZE));
 #ifdef DIFFERENCE_ENCODING
       sum=plus_exprt(

diff --git a/src/domains/linrank_domain.cpp b/src/domains/linrank_domain.cpp
@@ -14,7 +14,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 #include <util/cprover_prefix.h>
@@ -231,7 +230,7 @@ exprt linrank_domaint::get_row_symb_constraint(
   symb_values.c.resize(smt_model_values.size()/2);
   assert(!symb_values.c.empty());
   symb_values.c[0]=symbol_exprt(
-    SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$0",
+    SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$0",
     signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 
 #ifdef DIFFERENCE_ENCODING
@@ -245,7 +244,8 @@ exprt linrank_domaint::get_row_symb_constraint(
   for(unsigned i=1, vals_i=2; i<symb_values.c.size(); ++i, vals_i+=2)
   {
     symb_values.c[i]=symbol_exprt(
-      SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$"+i2string(i),
+      SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$"+
+      std::to_string(i),
       signedbv_typet(COEFF_C_SIZE));  // coefficients are signed integers
 #ifdef DIFFERENCE_ENCODING
     sum=plus_exprt(

diff --git a/src/domains/predabs_domain.cpp b/src/domains/predabs_domain.cpp
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 
 #include <util/find_symbols.h>
 #include <util/prefix.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 #include <langapi/languages.h>
 

diff --git a/src/domains/strategy_solver_binsearch2.cpp b/src/domains/strategy_solver_binsearch2.cpp
@@ -17,8 +17,6 @@ Author: Peter Schrammel
 
 #include <cassert>
 
-#include <util/i2string.h>
-
 #include "strategy_solver_binsearch2.h"
 #include "ssa/local_ssa.h"
 #include "util.h"
@@ -163,7 +161,7 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv)
   assert(sum.type()==lower.type());
 
   symbol_exprt sum_bound(
-    SUM_BOUND_VAR+i2string(sum_bound_counter++),
+    SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
     sum.type());
   solver << equal_exprt(sum_bound, sum);
 

diff --git a/src/domains/strategy_solver_binsearch3.cpp b/src/domains/strategy_solver_binsearch3.cpp
@@ -15,8 +15,6 @@ Author: Peter Schrammel
 
 #include <cassert>
 
-#include <util/i2string.h>
-
 #include "strategy_solver_binsearch3.h"
 #include "util.h"
 
@@ -164,7 +162,7 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv)
   assert(sum.type()==lower.type());
 
   symbol_exprt sum_bound(
-    SUM_BOUND_VAR+i2string(sum_bound_counter++),
+    SUM_BOUND_VAR+std::to_string(sum_bound_counter++),
     sum.type());
   solver << equal_exprt(sum_bound, sum);
 

diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/find_symbols.h>
-#include <util/i2string.h>
 #include <util/simplify_expr.h>
 
 #include "tpolyhedra_domain.h"
@@ -186,7 +185,7 @@ symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row)
   assert(row<templ.size());
   auto &row_expr=dynamic_cast<template_row_exprt &>(*templ[row].expr);
   return symbol_exprt(
-    SYMB_BOUND_VAR+i2string(domain_number)+"$"+i2string(row),
+    SYMB_BOUND_VAR+std::to_string(domain_number)+"$"+std::to_string(row),
     row_expr.type());
 }
 
@@ -358,7 +357,7 @@ void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row)
     const std::string &old_id=expr.get_string(ID_identifier);
     if(old_id.find(SYMB_BOUND_VAR)==std::string::npos)
     {
-      irep_idt id=old_id+"_"+i2string(row);
+      irep_idt id=old_id+"_"+std::to_string(row);
       expr.set(ID_identifier, id);
     }
   }

diff --git a/src/solver/summarizer_fw_contexts.cpp b/src/solver/summarizer_fw_contexts.cpp
@@ -19,7 +19,6 @@ Author: Peter Schrammel
 
 #include <util/xml.h>
 #include <util/xml_expr.h>
-#include <util/i2string.h>
 
 #include "summarizer_fw_contexts.h"
 #include "summary_db.h"
@@ -86,7 +85,7 @@ void summarizer_fw_contextst::inline_summaries(
           xmlt xml_cc("calling-context");
           xml_cc.set_attribute("function", id2string(fname));
           xml_cc.set_attribute(
-            "goto_location", i2string(n_it->location->location_number));
+            "goto_location", std::to_string(n_it->location->location_number));
 
           // location
           const source_locationt &source_location=

diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp
@@ -206,7 +206,7 @@ bool dynobj_instance_domaint::merge(
   ai_domain_baset::locationt from,
   ai_domain_baset::locationt to)
 {
-  bool result=false;
+  bool result=has_values.is_false() && !other.has_values.is_false();
   for(auto &obj : other.must_alias_relations)
   {
     if(must_alias_relations.find(obj.first)==must_alias_relations.end())

diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h
@@ -25,6 +25,7 @@ Description: In some cases, multiple instances must be used so that the
 #include <analyses/ai.h>
 #include <util/union_find.h>
 #include <util/options.h>
+#include <util/threeval.h>
 #include "ssa_object.h"
 #include "ssa_value_set.h"
 
@@ -159,6 +160,28 @@ class dynobj_instance_domaint:public ai_domain_baset
     locationt from,
     locationt to);
 
+  void make_bottom() override
+  {
+    must_alias_relations.clear();
+    live_pointers.clear();
+    has_values=tvt(false);
+  }
+
+  void make_top() override
+  {
+    must_alias_relations.clear();
+    live_pointers.clear();
+    has_values=tvt(true);
+  }
+
+  void make_entry() override
+  {
+    make_top();
+  }
+
+protected:
+  tvt has_values;
+
 private:
   void rhs_concretisation(
     const exprt &guard,