@@ -412,7 +412,7 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
412
412
codet java_bytecode_convert_methodt::get_array_bounds_check (
413
413
const exprt &arraystruct,
414
414
const exprt &idx,
415
- const source_locationt& original_sloc)
415
+ const source_locationt & original_sloc)
416
416
{
417
417
constant_exprt intzero=from_integer (0 , java_int_type ());
418
418
binary_relation_exprt gezero (idx, ID_ge, intzero);
@@ -1619,7 +1619,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1619
1619
{
1620
1620
assert (op.empty () && results.size ()==1 );
1621
1621
symbol_exprt symbol_expr (arg0.type ());
1622
- const auto & field_name=arg0.get_string (ID_component_name);
1622
+ const auto & field_name=arg0.get_string (ID_component_name);
1623
1623
symbol_expr.set_identifier (arg0.get_string (ID_class)+" ." +field_name);
1624
1624
results[0 ]=java_bytecode_promotion (symbol_expr);
1625
1625
@@ -1636,7 +1636,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1636
1636
{
1637
1637
assert (op.size ()==1 && results.empty ());
1638
1638
symbol_exprt symbol_expr (arg0.type ());
1639
- const auto & field_name=arg0.get_string (ID_component_name);
1639
+ const auto & field_name=arg0.get_string (ID_component_name);
1640
1640
symbol_expr.set_identifier (arg0.get_string (ID_class)+" ." +field_name);
1641
1641
c=code_assignt (symbol_expr, op[0 ]);
1642
1642
}
@@ -1715,7 +1715,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
1715
1715
}
1716
1716
if (max_array_length!=0 )
1717
1717
{
1718
- constant_exprt size_limit=from_integer (max_array_length, java_int_type ());
1718
+ constant_exprt size_limit=
1719
+ from_integer (max_array_length, java_int_type ());
1719
1720
binary_relation_exprt le_max_size (op[0 ], ID_le, size_limit);
1720
1721
code_assumet assume_le_max_size (le_max_size);
1721
1722
c.move_to_operands (assume_le_max_size);
0 commit comments