fixes

Author: Daniel Kroening

lib/cbmc

@@ -116,6 +116,8 @@ int hw_cbmc_parse_optionst::doit()
   // do actual BMC
   return do_bmc(hw_bmc, goto_functions);
   #endif
+
+  return false;
 }
 
 /*******************************************************************\
@@ -143,7 +145,7 @@ irep_idt hw_cbmc_parse_optionst::get_top_module()
     return irep_idt();
 
   return get_module(
-    symbol_table, top_module, get_message_handler()).name;
+    goto_model.symbol_table, top_module, get_message_handler()).name;
 }
 
 /*******************************************************************\
@@ -194,7 +196,7 @@ int hw_cbmc_parse_optionst::get_modules(
       if(cmdline.isset("gen-interface"))
       {
         const symbolt &symbol=
-          namespacet(symbol_table).lookup(top_module);
+          namespacet(goto_model.symbol_table).lookup(top_module);
 
         if(cmdline.isset("outfile"))
         {
@@ -205,10 +207,10 @@ int hw_cbmc_parse_optionst::get_modules(
             return 6;
           }
 
-          gen_interface(symbol_table, symbol, true, out, std::cerr);
+          gen_interface(goto_model.symbol_table, symbol, true, out, std::cerr);
         }
         else
-          gen_interface(symbol_table, symbol, true, std::cout, std::cerr);
+          gen_interface(goto_model.symbol_table, symbol, true, std::cout, std::cerr);
 
         return 0; // done
       }
@@ -220,7 +222,7 @@ int hw_cbmc_parse_optionst::get_modules(
       status() << "Mapping variables" << eom;
 
       map_vars(
-        symbol_table,
+        goto_model.symbol_table,
         top_module,
         bmc_constraints,
         get_message_handler(),
@@ -236,7 +238,7 @@ int hw_cbmc_parse_optionst::get_modules(
   }
   else if(cmdline.isset("show-modules"))
   {
-    show_modules(symbol_table, ui_message_handler.get_ui());
+    show_modules(goto_model.symbol_table, ui_message_handler.get_ui());
     return 0; // done
   }
 

src/hw-cbmc/hw_cbmc_parse_options.cpp

@@ -439,9 +439,7 @@ const symbolt &map_varst::add_array(symbolt &symbol)
 
   exprt array_size=from_integer(no_timeframes, index_type());
 
-  array_typet new_type;
-  new_type.size()=array_size;
-  new_type.subtype()=full_type;
+  array_typet new_type(full_type, array_size);
 
   new_symbol.type=new_type;
   new_symbol.value=exprt(ID_nondet);