Replace all uses of deprecated functions by non-deprecated ones

Author: tautschnig

CMakeLists.txt

@@ -23,7 +23,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     #   Ensure NDEBUG is not set for release builds
     set(CMAKE_CXX_FLAGS_RELEASE "-O2")
     #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
 elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     #   This would be the place to enable warnings for Windows builds, although
     #   config.inc doesn't seem to do that currently

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -67,8 +67,8 @@ janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
 void janalyzer_parse_optionst::register_languages()
 {
   // Need ansi C language for __CPROVER_rounding_mode
-  register_language(new_ansi_c_language);
-  register_language(new_java_bytecode_language);
+  register_language(new_ansi_c_language, get_message_handler());
+  register_language(new_java_bytecode_language, get_message_handler());
 }
 
 void janalyzer_parse_optionst::get_command_line_options(optionst &options)

jbmc/src/java_bytecode/character_refine_preprocess.h

@@ -29,6 +29,11 @@ Date:   March 2017
 class character_refine_preprocesst:public messaget
 {
 public:
+  explicit character_refine_preprocesst(message_handlert &message_handler)
+    : messaget(message_handler)
+  {
+  }
+
   void initialize_conversion_table();
   codet replace_character_call(const code_function_callt &call) const;
 

jbmc/src/java_bytecode/expr2java.cpp

@@ -314,7 +314,7 @@ std::string expr2javat::convert_java_this(
   const exprt &src,
   unsigned precedence)
 {
-  return "this";
+  return id2string(ID_this);
 }
 
 std::string expr2javat::convert_java_instanceof(

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -670,7 +670,11 @@ void java_bytecode_convert_classt::convert(
     }
   }
   else
-    field_type=java_type_from_string(f.descriptor);
+  {
+    auto type_from_string = java_type_from_string(f.descriptor);
+    CHECK_RETURN(type_from_string.has_value());
+    field_type=std::move(*type_from_string);
+  }
 
   // is this a static field?
   if(f.is_static)
@@ -831,11 +835,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     const irep_idt clone_name =
       id2string(struct_tag_type_identifier) + ".clone:()Ljava/lang/Object;";
-    java_method_typet::parametert this_param;
+    java_method_typet::parametert this_param(java_reference_type(struct_tag_type));
     this_param.set_identifier(id2string(clone_name)+"::this");
-    this_param.set_base_name("this");
+    this_param.set_base_name(ID_this);
     this_param.set_this();
-    this_param.type() = java_reference_type(struct_tag_type);
     const java_method_typet clone_type({this_param}, java_lang_object_type());
 
     parameter_symbolt this_symbol;

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -99,7 +99,7 @@ static void assign_parameter_names(
     irep_idt base_name, identifier;
 
     if(i==0 && parameters[i].get_this())
-      base_name="this";
+      base_name=ID_this;
     else
       base_name="stub_ignored_arg"+std::to_string(i);
 
@@ -258,21 +258,21 @@ java_method_typet member_type_lazy(
 
   messaget message(message_handler);
 
-  typet member_type_from_descriptor=java_type_from_string(descriptor);
-  INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
+  auto member_type_from_descriptor=java_type_from_string(descriptor);
+  INVARIANT(member_type_from_descriptor.has_value() && member_type_from_descriptor->id()==ID_code, "Must be code type");
   if(signature.has_value())
   {
     try
     {
-      typet member_type_from_signature=java_type_from_string(
+      auto member_type_from_signature=java_type_from_string(
         signature.value(),
         class_name);
-      INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
+      INVARIANT(member_type_from_signature.has_value() && member_type_from_signature->id()==ID_code, "Must be code type");
       if(
-        to_java_method_type(member_type_from_signature).parameters().size() ==
-        to_java_method_type(member_type_from_descriptor).parameters().size())
+        to_java_method_type(*member_type_from_signature).parameters().size() ==
+        to_java_method_type(*member_type_from_descriptor).parameters().size())
       {
-        return to_java_method_type(member_type_from_signature);
+        return to_java_method_type(*member_type_from_signature);
       }
       else
       {
@@ -293,7 +293,7 @@ java_method_typet member_type_lazy(
                         << message.eom;
     }
   }
-  return to_java_method_type(member_type_from_descriptor);
+  return to_java_method_type(*member_type_from_descriptor);
 }
 
 /// Retrieves the symbol of the lambda method associated with the given
@@ -368,10 +368,9 @@ void java_bytecode_convert_method_lazy(
   if(!m.is_static)
   {
     java_method_typet::parameterst &parameters = member_type.parameters();
-    java_method_typet::parametert this_p;
     const reference_typet object_ref_type =
       java_reference_type(struct_tag_typet(class_symbol.name));
-    this_p.type()=object_ref_type;
+    java_method_typet::parametert this_p(object_ref_type);
     this_p.set_this();
     parameters.insert(parameters.begin(), this_p);
   }
@@ -469,7 +468,7 @@ void java_bytecode_convert_methodt::convert(
         id2string(class_symbol.name));
     }
     else
-      t=java_type_from_string(v.descriptor);
+      t=*java_type_from_string(v.descriptor);
 
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.name;
@@ -516,7 +515,7 @@ void java_bytecode_convert_methodt::convert(
     if(param_index==0 && param.get_this())
     {
       // my.package.ClassName.myMethodName:(II)I::this
-      base_name="this";
+      base_name=ID_this;
       identifier=id2string(method_identifier)+"::"+id2string(base_name);
     }
     else
@@ -1182,7 +1181,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       }
     }
 
-    codet catch_instruction;
+    codet catch_instruction(ID_nil);
 
     if(catch_type!=typet())
     {
@@ -1199,8 +1198,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
           "caught_exception",
           java_reference_type(catch_type));
       stack.push_back(catch_var);
-      code_landingpadt catch_statement(catch_var);
-      catch_instruction=catch_statement;
+      catch_instruction = code_landingpadt(catch_var);
     }
 
     exprt::operandst op = pop(stmt_bytecode_info.pop);
@@ -1656,7 +1654,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     // Finally if this is the beginning of a catch block (already determined
     // before the big bytecode switch), insert the exception 'landing pad'
     // instruction before the actual instruction:
-    if(catch_instruction!=codet())
+    if(catch_instruction.get_statement() != ID_nil)
     {
       c.make_block();
       c.operands().insert(c.operands().begin(), catch_instruction);
@@ -1909,9 +1907,6 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   const source_locationt &location)
 {
   // we turn into switch-case
-  code_switcht code_switch;
-  code_switch.add_source_location() = location;
-  code_switch.value() = op[0];
   code_blockt code_block;
   code_block.add_source_location() = location;
 
@@ -1921,36 +1916,39 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   {
     if(is_label)
     {
-      code_switch_caset code_case;
-      code_case.add_source_location() = location;
-
       const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
       // The switch case does not contain any code, it just branches via a GOTO
       // to the jump target of the tableswitch/lookupswitch case at
       // hand. Therefore we consider this code to belong to the source bytecode
       // instruction and not the target instruction.
       const method_offsett label_number =
         numeric_cast_v<method_offsett>(number);
-      code_case.code() = code_gotot(label(std::to_string(label_number)));
-      code_case.code().add_source_location() = location;
+      code_gotot code(label(std::to_string(label_number)));
+      code.add_source_location() = location;
 
       if(a_it == args.begin())
+      {
+        code_switch_caset code_case(nil_exprt(), std::move(code));
+        code_case.add_source_location() = location;
         code_case.set_default();
+
+        code_block.add(std::move(code_case));
+      }
       else
       {
-        auto prev = a_it;
-        prev--;
-        code_case.case_op() = *prev;
-        if(code_case.case_op().type() != op[0].type())
-          code_case.case_op().make_typecast(op[0].type());
-        code_case.case_op().add_source_location() = location;
-      }
+        exprt case_op = typecast_exprt::conditional_cast(*std::prev(a_it), op[0].type());
+        case_op.add_source_location() = location;
+
+        code_switch_caset code_case(std::move(case_op), std::move(code));
+        code_case.add_source_location() = location;
 
-      code_block.add(code_case);
+        code_block.add(std::move(code_case));
+      }
     }
   }
 
-  code_switch.body() = code_block;
+  code_switcht code_switch(op[0], code_block);
+  code_switch.add_source_location() = location;
   return code_switch;
 }
 
@@ -2095,30 +2093,24 @@ void java_bytecode_convert_methodt::convert_invoke(
       reference_typet object_ref_type = java_reference_type(thistype);
       java_method_typet::parametert this_p(object_ref_type);
       this_p.set_this();
-      this_p.set_base_name("this");
+      this_p.set_base_name(ID_this);
       parameters.insert(parameters.begin(), this_p);
     }
   }
 
-  code_function_callt call;
   location.set_function(method_id);
 
-  call.add_source_location() = location;
-  call.arguments() = pop(parameters.size());
+  code_function_callt::argumentst arguments = pop(parameters.size());
 
   // double-check a bit
-  if(use_this)
-  {
-    const exprt &this_arg = call.arguments().front();
-    INVARIANT(
-      this_arg.type().id() == ID_pointer, "first argument must be a pointer");
-  }
+  INVARIANT(
+    !use_this || arguments.front().type().id() == ID_pointer, "first argument must be a pointer");
 
   // do some type adjustment for the arguments,
   // as Java promotes arguments
   // Also cast pointers since intermediate locals
   // can be void*.
-
+  INVARIANT(parameters.size() <= arguments.size(), "for each parameter there must be an argument");
   for(std::size_t i = 0; i < parameters.size(); i++)
   {
     const typet &type = parameters[i].type();
@@ -2127,21 +2119,20 @@ void java_bytecode_convert_methodt::convert_invoke(
       type == java_byte_type() || type == java_short_type() ||
       type.id() == ID_pointer)
     {
-      assert(i < call.arguments().size());
-      if(type != call.arguments()[i].type())
-        call.arguments()[i].make_typecast(type);
+      if(type != arguments[i].type())
+        arguments[i].make_typecast(type);
     }
   }
 
   // do some type adjustment for return values
-
+  exprt lhs = nil_exprt();
   const typet &return_type = method_type.return_type();
 
   if(return_type.id() != ID_empty)
   {
     // return types are promoted in Java
-    call.lhs() = tmp_variable("return", return_type);
-    exprt promoted = java_bytecode_promotion(call.lhs());
+    lhs = tmp_variable("return", return_type);
+    exprt promoted = java_bytecode_promotion(lhs);
     results.resize(1);
     results[0] = promoted;
   }
@@ -2184,19 +2175,20 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol_table.add(symbol);
   }
 
+  exprt function;
   if(is_virtual)
   {
     // dynamic binding
-    assert(use_this);
-    assert(!call.arguments().empty());
-    call.function() = arg0;
+    PRECONDITION(use_this);
+    PRECONDITION(!arguments.empty());
+    function = arg0;
     // Populate needed methods later,
     // once we know what object types can exist.
   }
   else
   {
     // static binding
-    call.function() = symbol_exprt(arg0.get(ID_identifier), arg0.type());
+    function = symbol_exprt(arg0.get(ID_identifier), arg0.type());
     if(needed_lazy_methods)
     {
       needed_lazy_methods->add_needed_method(arg0.get(ID_identifier));
@@ -2205,6 +2197,8 @@ void java_bytecode_convert_methodt::convert_invoke(
     }
   }
 
+  code_function_callt call(std::move(lhs), std::move(function), std::move(arguments));
+  call.add_source_location() = location;
   call.function().add_source_location() = location;
 
   // Replacing call if it is a function of the Character library,
@@ -2264,16 +2258,14 @@ void java_bytecode_convert_methodt::convert_athrow(
     // we translate athrow into
     // ASSERT false;
     // ASSUME false:
-    code_assertt assert_code;
-    assert_code.assertion() = false_exprt();
+    code_assertt assert_code(false_exprt{});
     source_locationt assert_location = location; // copy
     assert_location.set_comment("assertion at " + location.as_string());
     assert_location.set("user-provided", true);
     assert_location.set_property_class(ID_assertion);
     assert_code.add_source_location() = assert_location;
 
-    code_assumet assume_code;
-    assume_code.assumption() = false_exprt();
+    code_assumet assume_code(false_exprt{});
     source_locationt assume_location = location; // copy
     assume_location.set("user-provided", true);
     assume_code.add_source_location() = assume_location;
@@ -3012,7 +3004,7 @@ void java_bytecode_initialize_parameter_names(
     if(param_index == 0 && param.get_this())
     {
       // my.package.ClassName.myMethodName:(II)I::this
-      base_name = "this";
+      base_name = ID_this;
       identifier = id2string(method_symbol.name) + "::" + id2string(base_name);
     }
     else