Update to CBMC 5.61

Add missing symbolt include
Remove usage of deprecated goto_instructiont::get_assign()
Remove usage of deprecated goto_instructiont::get_function_call()
Add missing include for side_effect_exprt
Fix usage of goto_instructiont::source_location
Fix usage of goto_instructiontt:type
Update usage of goto_checkt
Remove deprecated calls to initiallize malloc_may_fail variables. This
feature is now handled differently in CBMC, see:
    diffblue/cbmc#6576
Make tests containing argc less strict, the C standard does not
guarantee that it is >= 1, just that it is non-negative. For more
information, refer to the CBMC commit:
    788cb496ee573cc4182273d1513c5a5eb68a383a
Make use of refactored update_assumptions_assertions of goto_check
Adjust heap domain to newly returned annotated_pointer_constant type.
For more information about this constant, see CBMC commit:
    112f1d0aaa5a4606aa0e6a06a9e1ee853ebc20ab
Update goto_check includes
Add removed make_assertions_false to preprocessing
Fix goto_check usage
Remove direct access to goto_instructiont::guard
Do not use soon-to-be-deprecated goto_instructiont::get_code
Fix collection of record free variables
Remove usage of base_type, it's deprecated

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

lib/cbmc

@@ -3,4 +3,4 @@ main.c
 --context-sensitive --preconditions
 ^EXIT=5$
 ^SIGNAL=0$
-^\[__CPROVER__start\]: argc' <= 268435456 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -2$
+^\[__CPROVER__start\]: argc' <= 2147483647 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= 0$

regression/preconditions/precond_contextsensitive2/test.desc

@@ -1,14 +1,14 @@
 int foo(int x)
 {
   int y;
-  if(x<1) while(1) y++;
+  if(x<0) while(1) y++;
   return x;
 }
 
 int main(int argc, char** argv)
 {
   int x = argc;
   x = foo(x);
-  assert(x>=1);
+  assert(x>=0);
   return x;
 }

regression/termination/abort1/main.c

@@ -11,7 +11,7 @@ int foo(int x)
 int main(int argc, char** argv)
 {
   int x = argc;
-  if(x>=1) x = foo(x);
+  if(x>=0) x = foo(x);
   else bar(); //unreachable
   return x;
 }

regression/termination/abort2/main.c

@@ -42,9 +42,9 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 
-#include <analyses/goto_check.h>
+#include <ansi-c/goto_check_c.h>
+#include <goto-programs/goto_check.h>
 
 #include <langapi/mode.h>
 
@@ -494,7 +494,7 @@ int twols_parse_optionst::doit()
       Forall_goto_program_instructions(i_it, body)
       {
         if(i_it->is_assert())
-          i_it->type=goto_program_instruction_typet::ASSUME;
+          i_it->turn_into_assume();
       }
     }
   }
@@ -855,23 +855,22 @@ void twols_parse_optionst::show_stats(
       if(i_it->is_backwards_goto())
         nr_loops++;
 
-      switch(instruction.type)
+      switch(instruction.type())
       {
       case ASSIGN:
       {
-        const code_assignt &assign=instruction.get_assign();
-        expr_stats_rec(assign.lhs(), stats);
-        expr_stats_rec(assign.rhs(), stats);
+        expr_stats_rec(instruction.assign_lhs(), stats);
+        expr_stats_rec(instruction.assign_rhs(), stats);
         break;
       }
       case ASSUME:
-        expr_stats_rec(instruction.guard, stats);
+        expr_stats_rec(instruction.condition(), stats);
         break;
       case ASSERT:
-        expr_stats_rec(instruction.guard, stats);
+        expr_stats_rec(instruction.condition(), stats);
         break;
       case GOTO:
-        expr_stats_rec(instruction.guard, stats);
+        expr_stats_rec(instruction.condition(), stats);
         break;
 
       case DECL:
@@ -963,11 +962,6 @@ bool twols_parse_optionst::get_goto_program(
     status() << "Adding CPROVER library" << eom;
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
 
-    // TODO: 2LS currently does not support the possibility of malloc failing,
-    //       we always initialize the CPROVER variables related to failure
-    //       to default (no fail). See if there is a way to improve this.
-    add_malloc_may_fail_variable_initializations(goto_model);
-
     if(process_goto_program(options, goto_model))
       return true;
   }
@@ -1065,7 +1059,8 @@ bool twols_parse_optionst::process_goto_program(
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
-    goto_check(options, goto_model);
+    goto_check_c(options, goto_model, *message_handler);
+    transform_assertions_assumptions(options, goto_model);
 
 #if UNWIND_GOTO_INTO_LOOP
     unwind_goto_into_loop(goto_model, 2);
@@ -1273,7 +1268,7 @@ void twols_parse_optionst::report_properties(
     else
     {
       status() << "[" << it->first << "] "
-               << it->second.pc->source_location.get_comment()
+               << it->second.pc->source_location().get_comment()
                << ": "
                << as_string(it->second.status)
                << eom;

src/2ls/2ls_parse_options.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <util/parse_options.h>
 #include <util/replace_symbol.h>
 
-#include <analyses/goto_check.h>
+#include <goto-programs/goto_check.h>
 #include <ssa/dynamic_objects.h>
 
 class goto_modelt;
@@ -187,6 +187,7 @@ class twols_parse_optionst:
   void assert_no_builtin_functions(goto_modelt &goto_model);
   void assert_no_atexit(goto_modelt &goto_model);
   void fix_goto_targets(goto_modelt &goto_model);
+  void make_assertions_false(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/2ls_parse_options.h

@@ -32,7 +32,7 @@ struct goalt
 
   explicit goalt(const goto_programt::instructiont &instruction)
   {
-    description=id2string(instruction.source_location.get_comment());
+    description=id2string(instruction.source_location().get_comment());
   }
 
   goalt()

src/2ls/cover_goals_ext.h

@@ -104,7 +104,7 @@ void dynamic_cfgt::build_cfg(
           incoming_edges[it->get_target()].insert(new_node);
         goto_programt::const_targett next=it; ++next;
         if(next!=goto_program.instructions.end() &&
-           (!it->is_goto() || !it->guard.is_true()))
+           (!it->is_goto() || !it->condition().is_true()))
           incoming_edges[next].insert(new_node);
 
         continue;
@@ -124,7 +124,7 @@ void dynamic_cfgt::build_cfg(
       incoming_edges[it->get_target()].insert(node);
     goto_programt::const_targett next=it; ++next;
     if(next!=goto_program.instructions.end() &&
-       (!it->is_goto() || !it->guard.is_true()))
+       (!it->is_goto() || !it->condition().is_true()))
       incoming_edges[next].insert(node);
 
     // alternative loop head detection when unwinder was not used

src/2ls/dynamic_cfg.cpp

@@ -48,7 +48,7 @@ void graphml_witness_extt::operator()(
   index_map.resize(cfg.size());
   for(std::size_t i=0; i<cfg.size(); ++i)
   {
-    const source_locationt &source_location=cfg[i].id.pc->source_location;
+    const source_locationt &source_location=cfg[i].id.pc->source_location();
 
     if(source_location.is_nil() ||
        source_location.get_file().empty() ||
@@ -95,7 +95,8 @@ void graphml_witness_extt::add_edge(
   const graphmlt::node_indext &to,
   const dynamic_cfg_nodet &to_cfg_node)
 {
-  const source_locationt &source_location=from_cfg_node.id.pc->source_location;
+  const source_locationt &source_location=
+    from_cfg_node.id.pc->source_location();
 
   xmlt edge("edge");
   edge.set_attribute("source", graphml[from].node_name);

src/2ls/graphml_witness_ext.cpp

@@ -117,7 +117,7 @@ void horn_encodingt::translate(
     const local_SSAt::nodet &node=*local_SSA.find_node(loc);
 #endif
     out << "; PC " << loc->location_number
-        << " " << loc->source_location << '\n';
+        << " " << loc->source_location() << '\n';
 
     out << "(assert (forall (";
 
@@ -152,7 +152,7 @@ void horn_encodingt::translate(
 
     if(loc->is_goto())
     {
-      if(loc->guard.is_true())
+      if(loc->condition().is_true())
       {
         out << "(h-" << function_id << '-'
             << loc->get_target()->location_number;
@@ -169,7 +169,7 @@ void horn_encodingt::translate(
         out << ')';
       }
 
-      if(!loc->guard.is_true())
+      if(!loc->condition().is_true())
       {
         goto_programt::instructionst::const_iterator next=loc;
         next++;

src/2ls/horn_encoding.cpp

@@ -67,8 +67,9 @@ void instrument_gotot::instrument_instruction(
 
   auto assumption=tmp.insert_after(
     target,
-    goto_programt::make_assumption(expr, target->source_location));
-  assumption->source_location.set_comment("invariant generated by 2LS");
+    goto_programt::make_assumption(expr, target->source_location()));
+  assumption->source_location_nonconst().set_comment(
+    "invariant generated by 2LS");
 
   dest.insert_before_swap(where, tmp);