Merge pull request #151 from FrNecas/frnecas-cbmc-5.11

Update to CBMC 5.11

Author: peterschrammel

lib/cbmc

@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.15\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.17\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE

regression/memsafety/built_from_end_false/test.desc

@@ -4,4 +4,4 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.pointer_dereference.33\] dereference failure: deallocated dynamic object in \*p: FAILURE
+\[main.pointer_dereference.38\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE

regression/memsafety/simple_false/test.desc

@@ -39,6 +39,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <analyses/goto_check.h>
 
@@ -899,11 +900,11 @@ bool twols_parse_optionst::get_goto_program(
 
   try
   {
-    goto_model=initialize_goto_model(cmdline, ui_message_handler);
+    goto_model=initialize_goto_model(cmdline.args, ui_message_handler, options);
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      show_symbol_table(goto_model.symbol_table, ui_message_handler);
       return true;
     }
 
@@ -1140,8 +1141,11 @@ bool twols_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      const namespacet ns(goto_model.symbol_table);
-      goto_model.goto_functions.output(ns, std::cout);
+      show_goto_functions(
+        goto_model,
+        get_message_handler(),
+        ui_message_handler.get_ui(),
+        false);
       return true;
     }
   }
@@ -1282,7 +1286,7 @@ void twols_parse_optionst::show_counterexample(
   {
   case ui_message_handlert::uit::PLAIN:
     std::cout << std::endl << "Counterexample:" << std::endl;
-    show_goto_trace(std::cout, ns, error_trace);
+    show_goto_trace(result(), ns, error_trace);
     break;
 
   case ui_message_handlert::uit::XML_UI:

src/2ls/2ls_parse_options.cpp

@@ -65,7 +65,7 @@ void horn_encodingt::translate(
          ";\n";
 
   // compute SSA
-  local_SSAt local_SSA(f_it->second, symbol_table, options, "");
+  local_SSAt local_SSA(f_it->first, f_it->second, symbol_table, options, "");
 
   const goto_programt &body=f_it->second.body;
 

src/2ls/horn_encoding.cpp

@@ -59,7 +59,7 @@ void twols_parse_optionst::propagate_constants(goto_modelt &goto_model)
   namespacet ns(goto_model.symbol_table);
   Forall_goto_functions(f_it, goto_model.goto_functions)
   {
-    constant_propagator_ait(f_it->second, ns);
+    constant_propagator_ait(f_it->first, f_it->second, ns);
   }
 }
 
@@ -627,9 +627,9 @@ std::map<symbol_exprt, size_t> twols_parse_optionst::split_dynamic_objects(
     if(!f_it->second.body_available())
       continue;
     namespacet ns(goto_model.symbol_table);
-    ssa_value_ait value_analysis(f_it->second, ns, options);
+    ssa_value_ait value_analysis(f_it->first, f_it->second, ns, options);
     dynobj_instance_analysist do_inst(
-      f_it->second, ns, options, value_analysis);
+      f_it->first, f_it->second, ns, options, value_analysis);
 
     compute_dynobj_instances(
       f_it->second.body, do_inst, dynobj_instances, ns);

src/2ls/preprocessing_util.cpp

@@ -29,13 +29,14 @@ Author: Daniel Kroening, [email protected]
 #include "show.h"
 
 void show_assignments(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   assignmentst assignments(
     goto_function.body,
     ns,
@@ -61,37 +62,38 @@ void show_assignments(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_assignments(f_it->second, ns, options, out);
+      show_assignments(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
     forall_goto_functions(f_it, goto_model.goto_functions)
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_assignments(f_it->second, ns, options, out);
+      show_assignments(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }
   }
 }
 
 void show_defs(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   assignmentst assignments(
     goto_function.body,
     ns,
     options,
     ssa_objects,
     ssa_value_ai);
   ssa_ait ssa_analysis(assignments);
-  ssa_analysis(goto_function, ns);
+  ssa_analysis(function_identifier, goto_function, ns);
   ssa_analysis.output(ns, goto_function.body, out);
 }
 
@@ -111,15 +113,15 @@ void show_defs(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_defs(f_it->second, ns, options, out);
+      show_defs(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
     forall_goto_functions(f_it, goto_model.goto_functions)
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_defs(f_it->second, ns, options, out);
+      show_defs(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }
@@ -166,6 +168,7 @@ void show_guards(
 }
 
 void show_ssa(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   bool simplify,
   const symbol_tablet &symbol_table,
@@ -175,7 +178,11 @@ void show_ssa(
   if(!goto_function.body_available())
     return;
 
-  unwindable_local_SSAt local_SSA(goto_function, symbol_table, options);
+  unwindable_local_SSAt local_SSA(
+    function_identifier,
+    goto_function,
+    symbol_table,
+    options);
   if(simplify)
     ::simplify(local_SSA, local_SSA.ns);
   local_SSA.output_verbose(out);
@@ -197,7 +204,13 @@ void show_ssa(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
+      show_ssa(
+        f_it->first,
+        f_it->second,
+        simplify,
+        goto_model.symbol_table,
+        options,
+        out);
   }
   else
   {
@@ -210,7 +223,13 @@ void show_ssa(
 
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_ssa(f_it->second, simplify, goto_model.symbol_table, options, out);
+      show_ssa(
+        f_it->first,
+        f_it->second,
+        simplify,
+        goto_model.symbol_table,
+        options,
+        out);
 
       out << "\n";
     }
@@ -383,13 +402,14 @@ void show_ssa_symbols(
 }
 
 void show_value_set(
+  const irep_idt &function_identifier,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const optionst &options,
   std::ostream &out)
 {
   ssa_objectst ssa_objects(goto_function, ns);
-  ssa_value_ait ssa_value_ai(goto_function, ns, options);
+  ssa_value_ait ssa_value_ai(function_identifier, goto_function, ns, options);
   ssa_value_ai.output(ns, goto_function, out);
 }
 
@@ -409,15 +429,15 @@ void show_value_sets(
     if(f_it==goto_model.goto_functions.function_map.end())
       out << "function " << function << " not found\n";
     else
-      show_value_set(f_it->second, ns, options, out);
+      show_value_set(f_it->first, f_it->second, ns, options, out);
   }
   else
   {
     forall_goto_functions(f_it, goto_model.goto_functions)
     {
       out << ">>>> Function " << f_it->first << "\n";
 
-      show_value_set(f_it->second, ns, options, out);
+      show_value_set(f_it->first, f_it->second, ns, options, out);
 
       out << "\n";
     }

src/2ls/show.cpp

@@ -16,6 +16,7 @@ Author: Peter Schrammel
 #include <langapi/language_util.h>
 #include <util/prefix.h>
 #include <goto-programs/write_goto_binary.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/flattening/bv_pointers.h>
@@ -501,7 +502,11 @@ void summary_checker_baset::instrument_and_output(
   instrument_gotot instrument_goto(options, ssa_db, summary_db);
   instrument_goto(goto_model);
   if(verbosity==10)
-    goto_model.output(std::cout);
+    show_goto_functions(
+      goto_model,
+      get_message_handler(),
+      ui_message_handlert::uit::PLAIN,
+      false);
   std::string filename=options.get_option("instrument-output");
   status() << "Writing instrumented goto-binary " << filename << eom;
   write_goto_binary(

src/2ls/summary_checker_base.cpp

@@ -12,6 +12,6 @@ Author: Peter Schrammel
 #ifndef CPROVER_2LS_2LS_VERSION_H
 #define CPROVER_2LS_2LS_VERSION_H
 
-#define TWOLS_VERSION "0.9.4"
+#define TWOLS_VERSION "0.9.5"
 
 #endif

src/2ls/version.h

@@ -119,7 +119,9 @@ void dynobj_instance_domaint::rhs_concretisation(
 }
 
 void dynobj_instance_domaint::transform(
+  const irep_idt &function_from,
   ai_domain_baset::locationt from,
+  const irep_idt &function_to,
   ai_domain_baset::locationt to,
   ai_baset &ai,
   const namespacet &ns)

src/ssa/dynobj_instance_analysis.cpp

@@ -151,7 +151,9 @@ class dynobj_instance_domaint:public ai_domain_baset
   std::map<symbol_exprt, std::set<exprt>> live_pointers;
 
   void transform(
+    const irep_idt &,
     locationt from,
+    const irep_idt &,
     locationt to,
     ai_baset &ai,
     const namespacet &ns) override;
@@ -208,14 +210,15 @@ class dynobj_instance_analysist:public ait<dynobj_instance_domaint>
 {
 public:
   dynobj_instance_analysist(
+    const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns,
     const optionst &_options,
     ssa_value_ait &_value_ai):
     options(_options),
     value_analysis(_value_ai)
   {
-    operator()(goto_function, ns);
+    operator()(function_identifier, goto_function, ns);
   }
 
 protected:

src/ssa/dynobj_instance_analysis.h

@@ -30,7 +30,7 @@ Author: Daniel Kroening, [email protected]
 void local_SSAt::build_SSA()
 {
   // perform SSA data-flow analysis
-  ssa_analysis(goto_function, ns);
+  ssa_analysis(function_identifier, goto_function, ns);
 
   forall_goto_program_instructions(i_it, goto_function.body)
   {
@@ -414,10 +414,10 @@ void local_SSAt::build_function_call(locationt loc)
     }
 
     // turn function call into expression
-    function_application_exprt f;
-    f.function()=to_symbol_expr(code_function_call.function());
-    f.type()=code_function_call.lhs().type();
-    f.arguments()=code_function_call.arguments();
+    function_application_exprt f(
+      to_symbol_expr(code_function_call.function()),
+      code_function_call.arguments(),
+      code_function_call.lhs().type());
 
     // access to "new" value in template declarations
     if(code_function_call.function().id()==ID_symbol &&

src/ssa/local_ssa.cpp

@@ -37,21 +37,23 @@ class local_SSAt
   typedef goto_programt::const_targett locationt;
 
   inline local_SSAt(
+    const irep_idt &_function_identifier,
     const goto_functiont &_goto_function,
     const symbol_tablet &_symbol_table,
     const optionst &_options,
     const std::string &_suffix=""):
     ns(_symbol_table), goto_function(_goto_function), options(_options),
     ssa_objects(_goto_function, ns),
-    ssa_value_ai(_goto_function, ns, options),
+    ssa_value_ai(_function_identifier, _goto_function, ns, options),
     assignments(
       _goto_function.body,
       ns,
       options,
       ssa_objects,
       ssa_value_ai),
-    alias_analysis(_goto_function, ns),
+    alias_analysis(_function_identifier, _goto_function, ns),
     guard_map(_goto_function.body),
+    function_identifier(_function_identifier),
     ssa_analysis(assignments),
     suffix(_suffix)
   {
@@ -242,6 +244,7 @@ class local_SSAt
 // protected:
   guard_mapt guard_map;
 
+  const irep_idt &function_identifier;
   ssa_ait ssa_analysis;
   std::string suffix; // an extra suffix