bump CBMC dependency

Author: kroening

lib/cbmc

@@ -243,8 +243,8 @@ bool map_varst::array_types_eq(
 
   namespacet ns(symbol_table);
 
-  const typet &s1 = ns.follow(type1.element_type());
-  const typet &s2 = ns.follow(type2.element_type());
+  const typet &s1 = type1.element_type();
+  const typet &s2 = type2.element_type();
 
   if(s1.id()==ID_array && s2.id()==ID_array)
     return array_types_eq(to_array_type(s1), to_array_type(s2), error_msg);
@@ -279,12 +279,6 @@ bool map_varst::check_types_rec(
 {
   namespacet ns(symbol_table);
 
-  if(type1.id()==ID_symbol)
-    return check_types_rec(ns.follow(type1), type2, error_msg);
-
-  if(type2.id()==ID_symbol)
-    return check_types_rec(type1, ns.follow(type2), error_msg);
-
   // type is the same?
   if(type1 == type2)
     return false;
@@ -357,8 +351,8 @@ void map_varst::add_constraint_rec(
 {
   namespacet ns(symbol_table);
 
-  const typet &t1=ns.follow(program_symbol.type());
-  const typet &t2=ns.follow(module_symbol.type());
+  const typet &t1=program_symbol.type();
+  const typet &t2=module_symbol.type();
 
   // check the type
   if(t1==t2)
@@ -426,7 +420,7 @@ const symbolt &map_varst::add_array(symbolt &symbol)
 {
   const namespacet ns(symbol_table);
 
-  const typet &full_type=ns.follow(symbol.type);
+  const typet &full_type=symbol.type;
 
   if(full_type.id()==ID_incomplete_array)
   {
@@ -514,7 +508,7 @@ void map_varst::map_var_rec(
   const irep_idt &prefix)
 {
   const namespacet ns(symbol_table);
-  const typet &expr_type=ns.follow(expr.type());
+  const typet &expr_type=expr.type();
   const struct_typet &struct_type=to_struct_type(expr_type);
   const struct_typet::componentst &components=struct_type.components();
 
@@ -535,7 +529,7 @@ void map_varst::map_var_rec(
     else
       base_name=name;
 
-    bool module_instance=ns.follow(c_it->type()).id()==ID_struct;
+    bool module_instance=c_it->type().id()==ID_struct;
 
     irep_idt full_name=id2string(prefix)+"."+id2string(base_name);
 
@@ -603,8 +597,8 @@ void map_varst::map_var(
 
   const namespacet ns(symbol_table);
 
-  const typet &type1=ns.follow(program_symbol.type());
-  const typet &type2=ns.follow(module_symbol.type);
+  const typet &type1=program_symbol.type();
+  const typet &type2=module_symbol.type;
 
   std::string error_msg;
   if(check_types_rec(type1, type2, error_msg))
@@ -721,7 +715,7 @@ void map_varst::map_vars(const irep_idt &top_module)
     index_exprt expr(
       symbol_expr,
       timeframe_expr,
-      to_array_type(ns.follow(symbol_expr.type())).element_type());
+      to_array_type(symbol_expr.type()).element_type());
 
     top_level_inputs.clear();
 
@@ -733,7 +727,7 @@ void map_varst::map_vars(const irep_idt &top_module)
       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);
+        symbol.type = 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/map_vars.cpp

@@ -51,7 +51,7 @@ void add_next_timeframe(
   block.add(assignment_increase);
 
   const struct_typet &struct_type =
-      to_struct_type(ns.follow(struct_symbol.type));
+      to_struct_type(struct_symbol.type);
 
   // now assign the non-inputs in the module symbol
   const index_exprt index_expr(array_symbol.symbol_expr(),

src/hw-cbmc/next_timeframe.cpp

@@ -40,7 +40,7 @@ void add_set_inputs(
   const symbolt &timeframe_symbol=ns.lookup("hw-cbmc::timeframe");
 
   const struct_typet &struct_type=
-    to_struct_type(ns.follow(struct_symbol.type));
+    to_struct_type(struct_symbol.type);
 
   // We now assume current input values to be equal,
   // with the goal of adding assumptions on inputs.

src/hw-cbmc/set_inputs.cpp

@@ -387,14 +387,10 @@ static mp_integer vcd_width(
   const typet &type,
   const namespacet &ns)
 {
-  if(type.id()==ID_symbol)
-    return vcd_width(ns.follow(type), ns);
-  else if(type.id()==ID_unsignedbv ||
-          type.id()==ID_signedbv ||
-          type.id()==ID_bv ||
-          type.id()==ID_fixedbv ||
-          type.id()==ID_floatbv ||
-          type.id()==ID_pointer)
+  if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_bv || type.id() == ID_fixedbv || type.id() == ID_floatbv ||
+    type.id() == ID_pointer)
   {
     return to_bitvector_type(type).get_width();
   }
@@ -456,8 +452,8 @@ static std::string as_vcd_binary(
   const exprt &expr,
   const namespacet &ns)
 {
-  const typet &type=ns.follow(expr.type());
-  
+  const auto &type = expr.type();
+
   if(expr.id()==ID_constant)
   {
     if(

src/trans-netlist/trans_trace.cpp

@@ -103,7 +103,12 @@ constant_exprt convert_real_literal(const irep_idt &value)
   // adjust exponent
   exponent -= str_fraction_part.size();
 
-  ieee_floatt ieee_float{ieee_float_spect::double_precision()};
+  // IEEE 1800-2017 5.7.2 says that real literal constants
+  // are IEEE 754 double-precision, but doesn't specify
+  // how to round when converting decimals.
+  ieee_floatt ieee_float{
+    ieee_float_spect::double_precision(),
+    ieee_floatt::rounding_modet::ROUND_TO_EVEN};
 
   ieee_float.from_base10(significand, exponent);
 

src/verilog/convert_literals.cpp

@@ -1246,8 +1246,7 @@ expr2verilogt::convert_constant(const constant_exprt &src)
   {
     constant_exprt tmp = src;
     tmp.type() = ieee_float_spect::double_precision().to_type();
-    ieee_floatt ieee_float;
-    ieee_float.from_expr(tmp);
+    auto ieee_float = ieee_float_valuet{tmp};
     return {precedence, ieee_float.to_ansi_c_string()};
   }
   else if(type.id() == ID_string)