Skip to content

Commit d959b08

Browse files
Change variables named code_type to method_type
This is for variables that have been changed to java_method_typet from code_typet
1 parent 182a3e6 commit d959b08

File tree

6 files changed

+34
-34
lines changed

6 files changed

+34
-34
lines changed

jbmc/src/java_bytecode/expr2java.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,10 +56,11 @@ std::string expr2javat::convert_code_function_call(
5656
dest+='=';
5757
}
5858

59-
const java_method_typet &code_type =
59+
const java_method_typet &method_type=
6060
to_java_method_type(src.function().type());
6161

62-
bool has_this = code_type.has_this() && !src.arguments().empty();
62+
bool has_this=method_type.has_this() &&
63+
!src.arguments().empty();
6364

6465
if(has_this)
6566
{
@@ -283,7 +284,7 @@ std::string expr2javat::convert_rec(
283284
return q+"byte"+d;
284285
else if(src.id()==ID_code)
285286
{
286-
const java_method_typet &code_type = to_java_method_type(src);
287+
const java_method_typet &method_type=to_java_method_type(src);
287288

288289
// Java doesn't really have syntax for function types,
289290
// so we make one up, loosely inspired by the syntax
@@ -292,7 +293,7 @@ std::string expr2javat::convert_rec(
292293
std::string dest="";
293294

294295
dest+='(';
295-
const java_method_typet::parameterst &parameters = code_type.parameters();
296+
const java_method_typet::parameterst &parameters=method_type.parameters();
296297

297298
for(java_method_typet::parameterst::const_iterator
298299
it=parameters.begin();
@@ -305,7 +306,7 @@ std::string expr2javat::convert_rec(
305306
dest+=convert(it->type());
306307
}
307308

308-
if(code_type.has_ellipsis())
309+
if(method_type.has_ellipsis())
309310
{
310311
if(!parameters.empty())
311312
dest+=", ";
@@ -314,7 +315,7 @@ std::string expr2javat::convert_rec(
314315

315316
dest+=')';
316317

317-
const typet &return_type = code_type.return_type();
318+
const typet &return_type=method_type.return_type();
318319
dest+=" -> "+convert(return_type);
319320

320321
return q + dest;

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 15 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1254,10 +1254,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
12541254
id2string(arg0.get(ID_identifier))==
12551255
"java::org.cprover.CProver.assume:(Z)V")
12561256
{
1257-
const java_method_typet &code_type = to_java_method_type(arg0.type());
1258-
INVARIANT(
1259-
code_type.parameters().size() == 1,
1260-
"function expected to have exactly one parameter");
1257+
const java_method_typet &method_type=to_java_method_type(arg0.type());
1258+
INVARIANT(method_type.parameters().size()==1,
1259+
"function expected to have exactly one parameter");
12611260
c = replace_call_to_cprover_assume(i_it->source_location, c);
12621261
}
12631262
// replace calls to CProver.atomicBegin
@@ -2107,8 +2106,8 @@ void java_bytecode_convert_methodt::convert_invoke(
21072106
const bool is_virtual(
21082107
statement == "invokevirtual" || statement == "invokeinterface");
21092108

2110-
java_method_typet &code_type = to_java_method_type(arg0.type());
2111-
java_method_typet::parameterst &parameters(code_type.parameters());
2109+
java_method_typet &method_type = to_java_method_type(arg0.type());
2110+
java_method_typet::parameterst &parameters(method_type.parameters());
21122111

21132112
if(use_this)
21142113
{
@@ -2124,10 +2123,10 @@ void java_bytecode_convert_methodt::convert_invoke(
21242123
{
21252124
if(needed_lazy_methods)
21262125
needed_lazy_methods->add_needed_class(classname);
2127-
code_type.set_is_constructor();
2126+
method_type.set_is_constructor();
21282127
}
21292128
else
2130-
code_type.set(ID_java_super_method_call, true);
2129+
method_type.set(ID_java_super_method_call, true);
21312130
}
21322131
reference_typet object_ref_type = java_reference_type(thistype);
21332132
java_method_typet::parametert this_p(object_ref_type);
@@ -2172,7 +2171,7 @@ void java_bytecode_convert_methodt::convert_invoke(
21722171

21732172
// do some type adjustment for return values
21742173

2175-
const typet &return_type = code_type.return_type();
2174+
const typet &return_type = method_type.return_type();
21762175

21772176
if(return_type.id() != ID_empty)
21782177
{
@@ -2954,11 +2953,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
29542953
const source_locationt &location,
29552954
const exprt &arg0)
29562955
{
2957-
const java_method_typet &code_type = to_java_method_type(arg0.type());
2956+
const java_method_typet &method_type = to_java_method_type(arg0.type());
29582957

29592958
const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
29602959
lambda_method_handles,
2961-
code_type.get_int(ID_java_lambda_method_handle_index));
2960+
method_type.get_int(ID_java_lambda_method_handle_index));
29622961
if(lambda_method_symbol.has_value())
29632962
debug() << "Converting invokedynamic for lambda: "
29642963
<< lambda_method_symbol.value().name << eom;
@@ -2967,11 +2966,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
29672966
"type"
29682967
<< eom;
29692968

2970-
const java_method_typet::parameterst &parameters(code_type.parameters());
2969+
const java_method_typet::parameterst &parameters(method_type.parameters());
29712970

29722971
pop(parameters.size());
29732972

2974-
const typet &return_type = code_type.return_type();
2973+
const typet &return_type = method_type.return_type();
29752974

29762975
if(return_type.id() == ID_empty)
29772976
return {};
@@ -3030,11 +3029,11 @@ void java_bytecode_initialize_parameter_names(
30303029
{
30313030
// Obtain a std::vector of java_method_typet::parametert objects from the
30323031
// (function) type of the symbol
3033-
java_method_typet &code_type = to_java_method_type(method_symbol.type);
3034-
java_method_typet::parameterst &parameters = code_type.parameters();
3032+
java_method_typet &method_type = to_java_method_type(method_symbol.type);
3033+
java_method_typet::parameterst &parameters = method_type.parameters();
30353034

30363035
// Find number of parameters
3037-
unsigned slots_for_parameters = java_method_parameter_slots(code_type);
3036+
unsigned slots_for_parameters = java_method_parameter_slots(method_type);
30383037

30393038
// Find parameter names in the local variable table:
30403039
typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;

jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,10 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
3838
}
3939
else if(type.id()==ID_code)
4040
{
41-
java_method_typet &code_type = to_java_method_type(type);
42-
typecheck_type(code_type.return_type());
41+
java_method_typet &method_type=to_java_method_type(type);
42+
typecheck_type(method_type.return_type());
4343

44-
java_method_typet::parameterst &parameters = code_type.parameters();
44+
java_method_typet::parameterst &parameters=method_type.parameters();
4545

4646
for(java_method_typet::parameterst::iterator
4747
it=parameters.begin(); it!=parameters.end(); it++)

jbmc/src/java_bytecode/java_types.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -974,13 +974,13 @@ std::string pretty_java_type(const typet &type)
974974
return "?";
975975
}
976976

977-
std::string pretty_signature(const java_method_typet &code_type)
977+
std::string pretty_signature(const java_method_typet &method_type)
978978
{
979979
std::ostringstream result;
980980
result << '(';
981981

982982
bool first = true;
983-
for(const auto p : code_type.parameters())
983+
for(const auto p : method_type.parameters())
984984
{
985985
if(p.get_this())
986986
continue;

jbmc/unit/java-testing-utils/require_type.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ struct_union_typet::componentt require_type::require_component(
5454

5555
/// Checks a type is a code_type (i.e. a function)
5656
/// \param type: The type to check
57-
/// \return The cast version of the type code_type
57+
/// \return The cast version of the type method_type
5858
java_method_typet require_type::require_code(const typet &type)
5959
{
6060
REQUIRE(type.id() == ID_code);
@@ -70,9 +70,9 @@ java_method_typet require_type::require_code(const typet &type)
7070
java_method_typet
7171
require_type::require_code(const typet &type, const size_t num_params)
7272
{
73-
java_method_typet code_type = require_code(type);
74-
REQUIRE(code_type.parameters().size() == num_params);
75-
return code_type;
73+
java_method_typet method_type = require_code(type);
74+
REQUIRE(method_type.parameters().size() == num_params);
75+
return method_type;
7676
}
7777

7878
/// Verify that a function has a parameter of a specific name.

jbmc/unit/util/parameter_indices.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@
1212

1313
void check_consistency(const symbolt &symbol)
1414
{
15-
const auto &code_type = to_java_method_type(symbol.type);
16-
auto parameter_ids = code_type.parameter_identifiers();
17-
auto parameter_indices = code_type.parameter_indices();
15+
const auto &method_type = to_java_method_type(symbol.type);
16+
auto parameter_ids = method_type.parameter_identifiers();
17+
auto parameter_indices = method_type.parameter_indices();
1818

1919
REQUIRE(parameter_ids.size() == parameter_indices.size());
2020
for(std::size_t i = 0; i < parameter_ids.size(); ++i)

0 commit comments

Comments
 (0)