Various cleanup

Author: tautschnig

src/analyses/goto_check.cpp

@@ -934,8 +934,6 @@ void goto_checkt::pointer_validity_check(
   local_bitvector_analysist::flagst flags=
     local_bitvector_analysis->get(t, pointer);
 
-  const typet &dereference_type=pointer_type.subtype();
-
   // For Java, we only need to check for null
   if(mode==ID_java)
   {
@@ -1044,7 +1042,7 @@ void goto_checkt::pointer_validity_check(
     {
       const or_exprt dynamic_bounds(
         dynamic_object_lower_bound(pointer, ns, access_lb),
-        dynamic_object_upper_bound(pointer, dereference_type, ns, access_ub));
+        dynamic_object_upper_bound(pointer, ns, access_ub));
 
       add_guarded_claim(
         or_exprt(
@@ -1065,7 +1063,7 @@ void goto_checkt::pointer_validity_check(
     {
       const or_exprt object_bounds(
         object_lower_bound(pointer, ns, access_lb),
-        object_upper_bound(pointer, dereference_type, ns, access_ub));
+        object_upper_bound(pointer, ns, access_ub));
 
       add_guarded_claim(
         or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)),

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,8 +22,7 @@ Author: Daniel Kroening, [email protected]
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
   code_blockt &init_code,
-  symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  symbol_tablet &symbol_table)
 {
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
@@ -432,8 +431,7 @@ bool generate_ansi_c_start_function(
       build_function_environment(
         parameters,
         init_code,
-        symbol_table,
-        message_handler);
+        symbol_table);
   }
 
   init_code.move_to_operands(call_main);

src/ansi-c/c_typecast.cpp

@@ -277,7 +277,7 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 c_typecastt::c_typet c_typecastt::get_c_type(
   const typet &type) const
 {
-  unsigned width=type.get_int(ID_width);
+  const std::size_t width = type.get_size_t(ID_width);
 
   if(type.id()==ID_signedbv)
   {
@@ -396,8 +396,13 @@ void c_typecastt::implicit_typecast_arithmetic(
   case RATIONAL:   new_type=rational_typet(); break;
   case REAL:       new_type=real_typet(); break;
   case INTEGER:    new_type=integer_typet(); break;
-  case COMPLEX: return; // do nothing
-  default: return;
+  case COMPLEX:
+  case OTHER:
+  case VOIDPTR:
+  case FIXEDBV:
+  case LARGE_UNSIGNED_INT:
+  case LARGE_SIGNED_INT:
+                   return; // do nothing
   }
 
   if(new_type!=expr_type)

src/ansi-c/c_typecheck_code.cpp

@@ -563,7 +563,7 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
   implicit_typecast(code.op1(), switch_op_type);
 }
 
-void c_typecheck_baset::typecheck_gcc_local_label(codet &code)
+void c_typecheck_baset::typecheck_gcc_local_label(codet &)
 {
   // these are just declarations, e.g.,
   // __label__ here, there;

src/ansi-c/c_typecheck_expr.cpp

@@ -2694,20 +2694,20 @@ exprt c_typecheck_baset::do_special_functions(
       // clang returns 4 for _Bool, gcc treats these as 'int'.
       type_number =
         config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG
-          ? 4
-          : 1;
+          ? 4u
+          : 1u;
     }
     else
     {
       type_number =
-          type.id() == ID_empty ? 0
-        : (type.id() == ID_bool || type.id() == ID_c_bool) ? 4
-        : (type.id() == ID_pointer || type.id() == ID_array) ? 5
-        : type.id() == ID_floatbv ? 8
-        : (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9
-        : type.id() == ID_struct ? 12
-        : type.id() == ID_union ? 13
-        : 1; // int, short, char, enum_tag
+          type.id() == ID_empty ? 0u
+        : (type.id() == ID_bool || type.id() == ID_c_bool) ? 4u
+        : (type.id() == ID_pointer || type.id() == ID_array) ? 5u
+        : type.id() == ID_floatbv ? 8u
+        : (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9u
+        : type.id() == ID_struct ? 12u
+        : type.id() == ID_union ? 13u
+        : 1u; // int, short, char, enum_tag
     }
 
     exprt tmp=from_integer(type_number, expr.type());

src/ansi-c/c_typecheck_type.cpp

@@ -1368,7 +1368,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
       throw 0;
     }
 
-    sub_width=c_enum_type.subtype().get_int(ID_width);
+    sub_width = c_enum_type.subtype().get_size_t(ID_width);
   }
   else
   {

src/ansi-c/expr2c.cpp

@@ -1164,26 +1164,6 @@ std::string expr2ct::convert_unary(
   return dest;
 }
 
-std::string expr2ct::convert_pointer_object_has_type(
-  const exprt &src,
-  unsigned precedence)
-{
-  if(src.operands().size()!=1)
-    return convert_norep(src, precedence);
-
-  unsigned p0;
-  std::string op0=convert_with_precedence(src.op0(), p0);
-
-  std::string dest="POINTER_OBJECT_HAS_TYPE";
-  dest+='(';
-  dest+=op0;
-  dest+=", ";
-  dest+=convert(static_cast<const typet &>(src.find("object_type")));
-  dest+=')';
-
-  return dest;
-}
-
 std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
 {
   if(src.operands().size() != 2)
@@ -3578,9 +3558,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="object_value")
     return convert_function(src, "OBJECT_VALUE", precedence=16);
 
-  else if(src.id()=="pointer_object_has_type")
-    return convert_pointer_object_has_type(src, precedence=16);
-
   else if(src.id()==ID_array_of)
     return convert_array_of(src, precedence=16);
 

src/ansi-c/expr2c_class.h

@@ -102,9 +102,6 @@ class expr2ct
   std::string convert_member(
     const member_exprt &src, unsigned precedence);
 
-  std::string convert_pointer_object_has_type(
-    const exprt &src, unsigned precedence);
-
   std::string convert_array_of(const exprt &src, unsigned precedence);
 
   std::string convert_trinary(

src/ansi-c/padding.cpp

@@ -127,7 +127,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)
     const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
 
     if(c_enum_type.id() == ID_c_enum)
-      return c_enum_type.subtype().get_int(ID_width);
+      return c_enum_type.subtype().get_size_t(ID_width);
     else
       return {};
   }

src/config.inc

@@ -21,7 +21,11 @@ ifeq ($(BUILD_ENV),MSVC)
   # disable warning "behavior change ... called instead of ..."
   CXXFLAGS += /wd4350
   # disable warning "assignment operator could not be generated"
-  CXXFLAGS += /wd4512
+  CXXFLAGS += /wd4512 /wd4626
+  # disable warning "copy constructor could not be generated"
+  CXXFLAGS += /wd4625
+  # disable warning "no override available, function is hidden"
+  CXXFLAGS += /wd4266
 else
   CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations
 endif