Temp commit

Trying to get the hw-cbmc to work. No luck so far.

Author: petr-bauch

src/hw-cbmc/hw_cbmc_parse_options.cpp

@@ -17,9 +17,13 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/goto_verifier.h>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/solver_factory.h>
+
+#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
+
 #include <langapi/mode.h>
+
 #include <trans-word-level/show_modules.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
@@ -74,8 +78,6 @@ int hw_cbmc_parse_optionst::doit()
   if(cmdline.isset("vcd"))
     options.set_option("vcd", cmdline.get_value("vcd"));
 
-  symbol_tablet symbol_table;
-
   std::unique_ptr<goto_verifiert> verifier = nullptr;
   verifier = util_make_unique<
       all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
@@ -87,18 +89,33 @@ int hw_cbmc_parse_optionst::doit()
   prop_convt &prop_conv =
       static_cast<prop_convt &>(*my_solver->decision_procedure_ptr);
 
-  goto_functionst &goto_functions = goto_model.goto_functions;
   int get_goto_program_ret =
       get_goto_program(goto_model, options, cmdline, ui_message_handler);
   if (get_goto_program_ret != -1)
     return get_goto_program_ret;
 
+  std::list<exprt> constraints;
+  int get_modules_ret = get_modules(constraints);
+  if (get_modules_ret != -1)
+    return get_modules_ret;
+
+  goto_convert(goto_model.symbol_table, goto_model.goto_functions,
+               ui_message_handler);
+
   unwind_no_timeframes = get_bound();
   unwind_module = get_top_module();
-
   do_unwind_module(prop_conv);
 
-  label_properties(goto_functions);
+  // the 'extra constraints'
+  if (!constraints.empty()) {
+    log.status() << "converting constraints" << messaget::eom;
+
+    for (const auto &constraint : constraints) {
+      prop_conv.set_to_true(constraint);
+    }
+  }
+
+  label_properties(goto_model.goto_functions);
 
   if (cmdline.isset("show-properties")) {
     show_properties(goto_model, ui_message_handler);
@@ -112,7 +129,6 @@ int hw_cbmc_parse_optionst::doit()
 
   const resultt result = (*verifier)();
   verifier->report();
-  show_unwind_trace(options, prop_conv);
   return result_to_exit_code(result);
 }
 

src/hw-cbmc/map_vars.cpp

@@ -694,7 +694,9 @@ void map_varst::map_vars(const irep_idt &top_module)
             << top_module_symbol.base_name << "'" << eom;
     return;
   }
-  
+
+  namespacet ns(symbol_table);
+
   {
     symbolt &s=lookup(struct_symbol);
 
@@ -712,7 +714,6 @@ void map_varst::map_vars(const irep_idt &top_module)
 
     exprt timeframe_expr=from_integer(0, index_type());
 
-    namespacet ns(symbol_table);
     index_exprt expr(
       symbol_expr, timeframe_expr, ns.follow(symbol_expr.type()).subtype());
 
@@ -725,6 +726,8 @@ void map_varst::map_vars(const irep_idt &top_module)
     if (entry.second.mode == ID_C || entry.second.mode == ID_cpp) {
       const irep_idt &base_name = entry.second.base_name;
       symbolt &symbol = symbol_table.get_writeable_ref(entry.first);
+      if (symbol.type.id() == ID_struct_tag)
+        symbol.type = ns.follow(symbol.type);
       if (base_name == "next_timeframe" && symbol.type.id() == ID_code) {
         namespacet ns(symbol_table);
         add_next_timeframe(symbol, struct_symbol, top_level_inputs, ns);

src/hw-cbmc/next_timeframe.cpp

@@ -50,18 +50,19 @@ void add_next_timeframe(
   code_blockt block;
   block.add(assignment_increase);
 
+  const struct_typet &struct_type =
+      to_struct_type(ns.follow(struct_symbol.type));
+
   // now assign the non-inputs in the module symbol
-  const index_exprt index_expr(
-    array_symbol.symbol_expr(),
-    timeframe_symbol.symbol_expr(),
-    struct_symbol.type);
+  const index_exprt index_expr(array_symbol.symbol_expr(),
+                               timeframe_symbol.symbol_expr(), struct_type);
 
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(struct_symbol.type));
-    
   const struct_typet::componentst &components=
     struct_type.components();
 
+  symbol_exprt struct_symbol_expr{struct_type};
+  struct_symbol_expr.set_identifier(struct_symbol.name);
+
   for(struct_typet::componentst::const_iterator
       c_it=components.begin();
       c_it!=components.end();
@@ -72,10 +73,11 @@ void add_next_timeframe(
     const typet &type=c_it->type();
 
     if(top_level_inputs.find(name)!=top_level_inputs.end()) continue;
-  
-    const exprt member_expr1=member_exprt(struct_symbol.symbol_expr(), name, type);
+
+    const exprt member_expr1 = member_exprt(struct_symbol_expr, name, type);
     const exprt member_expr2=member_exprt(index_expr, name, type);
-  
+
+    CHECK_RETURN(member_expr1.op0().type() == member_expr2.op0().type());
     const code_assignt member_assignment(member_expr1, member_expr2);
     block.add(member_assignment);
   }