From 75f8490be7388a13fcfe8486ac8368713226b16c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 7 Nov 2020 11:38:55 +0000 Subject: [PATCH] Remove codet::parametert() constructor This constructor has been deprecated since September 2018. There are two residual in-tree uses, which are replaced by the (simple) alternative. --- jbmc/src/java_bytecode/lambda_synthesis.cpp | 5 ++--- .../convert_method.cpp | 18 ++++++------------ src/util/std_types.h | 5 ----- 3 files changed, 8 insertions(+), 20 deletions(-) diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 1b58d570fb1..419de882a7f 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -325,12 +325,11 @@ static symbolt constructor_symbol( id2string(constructor_name) + "::" + id2string(param_basename)); } - java_method_typet::parametert constructor_this_param; + java_method_typet::parametert constructor_this_param( + java_reference_type(struct_tag_typet(synthetic_class_name))); constructor_this_param.set_this(); constructor_this_param.set_base_name("this"); constructor_this_param.set_identifier(id2string(constructor_name) + "::this"); - constructor_this_param.type() = - java_reference_type(struct_tag_typet(synthetic_class_name)); constructor_type.parameters().insert( constructor_type.parameters().begin(), constructor_this_param); diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index 043f73cf308..766755b018c 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -929,13 +929,10 @@ TEST_CASE( irep_idt method_identifier = "someClass.someMethod"; // The parameters should be already populated, but not have names, ids - code_typet::parametert this_param; + code_typet::parametert this_param(java_lang_object_type()); this_param.set_this(); - this_param.type() = java_lang_object_type(); - code_typet::parametert ref_to_inner; - ref_to_inner.type() = java_lang_object_type(); - code_typet::parametert other_param; - other_param.type() = java_lang_object_type(); + code_typet::parametert ref_to_inner(java_lang_object_type()); + code_typet::parametert other_param(java_lang_object_type()); java_method_typet::parameterst parameters{ this_param, ref_to_inner, other_param}; for(const auto ¶m : parameters) @@ -985,17 +982,14 @@ TEST_CASE( // Arrange const irep_idt method_id = "someClass.someMethod"; // The parameters should be already populated, with names, ids - code_typet::parametert this_param; + code_typet::parametert this_param(java_lang_object_type()); this_param.set_this(); - this_param.type() = java_lang_object_type(); this_param.set_identifier(id2string(method_id) + "::this"); this_param.set_base_name("this"); - code_typet::parametert ref_to_inner; - ref_to_inner.type() = java_lang_object_type(); + code_typet::parametert ref_to_inner(java_lang_object_type()); ref_to_inner.set_identifier(id2string(method_id) + "::this$0"); ref_to_inner.set_base_name("this$0"); - code_typet::parametert other_param; - other_param.type() = java_lang_object_type(); + code_typet::parametert other_param(java_lang_object_type()); other_param.set_identifier(id2string(method_id) + "::other"); other_param.set_base_name("other"); java_method_typet::parameterst parameters{ diff --git a/src/util/std_types.h b/src/util/std_types.h index 62e64c33a4b..d193f98e3ae 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -752,11 +752,6 @@ class code_typet:public typet class parametert:public exprt { public: - DEPRECATED(SINCE(2018, 9, 21, "use parametert(type) instead")) - parametert():exprt(ID_parameter) - { - } - explicit parametert(const typet &type):exprt(ID_parameter, type) { }