Skip to content

Commit e960c50

Browse files
cristina-davidcristina-david
committed
Use better function names
1 parent 3ac8e40 commit e960c50

File tree

4 files changed

+42
-45
lines changed

4 files changed

+42
-45
lines changed

‎src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 31 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -569,7 +569,7 @@ codet java_bytecode_convert_methodt::get_array_bounds_check(
569569

570570
/*******************************************************************\
571571
572-
Function: get_array_access_check
572+
Function: throw_array_access_exception
573573
574574
Inputs:
575575
@@ -581,10 +581,10 @@ Function: get_array_access_check
581581
582582
\*******************************************************************/
583583

584-
codet java_bytecode_convert_methodt::get_array_access_check(
584+
codet java_bytecode_convert_methodt::throw_array_access_exception(
585585
const exprt &array_struct,
586586
const exprt &idx,
587-
const source_locationt &original_sloc)
587+
const source_locationt &original_loc)
588588
{
589589
symbolt exc_symbol;
590590
if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException"))
@@ -601,7 +601,7 @@ codet java_bytecode_convert_methodt::get_array_access_check(
601601

602602
const symbol_exprt &exc=exc_symbol.symbol_expr();
603603
side_effect_expr_throwt throw_expr;
604-
throw_expr.add_source_location()=original_sloc;
604+
throw_expr.add_source_location()=original_loc;
605605
throw_expr.copy_to_operands(exc);
606606

607607
const constant_exprt &zero=from_integer(0, java_int_type());
@@ -611,7 +611,7 @@ codet java_bytecode_convert_methodt::get_array_access_check(
611611
const and_exprt and_expr(lt_zero, ge_length);
612612

613613
code_ifthenelset if_code;
614-
if_code.add_source_location()=original_sloc;
614+
if_code.add_source_location()=original_loc;
615615
if_code.cond()=and_expr;
616616
if_code.then_case()=code_expressiont(throw_expr);
617617

@@ -620,7 +620,7 @@ codet java_bytecode_convert_methodt::get_array_access_check(
620620

621621
/*******************************************************************\
622622
623-
Function: get_array_length_check
623+
Function: throw_array_length_exception
624624
625625
Inputs:
626626
@@ -630,9 +630,9 @@ Function: get_array_length_check
630630
631631
\*******************************************************************/
632632

633-
codet java_bytecode_convert_methodt::get_array_length_check(
633+
codet java_bytecode_convert_methodt::throw_array_length_exception(
634634
const exprt &length,
635-
const source_locationt &original_sloc)
635+
const source_locationt &original_loc)
636636
{
637637
symbolt exc_symbol;
638638
if(!symbol_table.has_symbol("NegativeArraySizeException"))
@@ -649,23 +649,23 @@ codet java_bytecode_convert_methodt::get_array_length_check(
649649

650650
const symbol_exprt &exc=exc_symbol.symbol_expr();
651651
side_effect_expr_throwt throw_expr;
652-
throw_expr.add_source_location()=original_sloc;
652+
throw_expr.add_source_location()=original_loc;
653653
throw_expr.copy_to_operands(exc);
654654

655655
const constant_exprt &zero=from_integer(0, java_int_type());
656656
const binary_relation_exprt ge_zero(length, ID_ge, zero);
657657

658658
code_ifthenelset if_code;
659-
if_code.add_source_location()=original_sloc;
659+
if_code.add_source_location()=original_loc;
660660
if_code.cond()=ge_zero;
661661
if_code.then_case()=code_expressiont(throw_expr);
662-
662+
663663
return if_code;
664664
}
665665

666666
/*******************************************************************\
667667
668-
Function: get_null_dereference_check
668+
Function: throw_null_dereference_exception
669669
670670
Inputs:
671671
@@ -676,9 +676,9 @@ Function: get_null_dereference_check
676676
677677
\*******************************************************************/
678678

679-
codet java_bytecode_convert_methodt::get_null_dereference_check(
679+
codet java_bytecode_convert_methodt::throw_null_dereference_exception(
680680
const exprt &expr,
681-
const source_locationt &original_sloc)
681+
const source_locationt &original_loc)
682682
{
683683
symbolt exc_symbol;
684684
if(!symbol_table.has_symbol("NullPointerException"))
@@ -695,14 +695,14 @@ codet java_bytecode_convert_methodt::get_null_dereference_check(
695695

696696
const symbol_exprt &exc=exc_symbol.symbol_expr();
697697
side_effect_expr_throwt throw_expr;
698-
throw_expr.add_source_location()=original_sloc;
698+
throw_expr.add_source_location()=original_loc;
699699
throw_expr.copy_to_operands(exc);
700700

701701
const equal_exprt equal_expr(
702702
expr,
703703
null_pointer_exprt(pointer_typet(empty_typet())));
704704
code_ifthenelset if_code;
705-
if_code.add_source_location()=original_sloc;
705+
if_code.add_source_location()=original_loc;
706706
if_code.cond()=equal_expr;
707707
if_code.then_case()=code_expressiont(throw_expr);
708708

@@ -711,7 +711,7 @@ codet java_bytecode_convert_methodt::get_null_dereference_check(
711711

712712
/*******************************************************************\
713713
714-
Function: get_class_cast_check
714+
Function: throw_class_cast_exception
715715
716716
Inputs:
717717
@@ -721,10 +721,10 @@ Function: get_class_cast_check
721721
722722
\*******************************************************************/
723723

724-
codet java_bytecode_convert_methodt::get_class_cast_check(
724+
codet java_bytecode_convert_methodt::throw_class_cast_exception(
725725
const exprt &class1,
726726
const exprt &class2,
727-
const source_locationt &original_sloc)
727+
const source_locationt &original_loc)
728728
{
729729
// TODO: use std::move
730730
symbolt exc_symbol;
@@ -743,7 +743,7 @@ codet java_bytecode_convert_methodt::get_class_cast_check(
743743
const symbol_exprt &exc=exc_symbol.symbol_expr();
744744

745745
side_effect_expr_throwt throw_expr;
746-
throw_expr.add_source_location()=original_sloc;
746+
throw_expr.add_source_location()=original_loc;
747747
throw_expr.copy_to_operands(exc);
748748

749749
binary_predicate_exprt class_cast_check(
@@ -760,7 +760,7 @@ codet java_bytecode_convert_methodt::get_class_cast_check(
760760
and_exprt and_expr(op_not_null, class_cast_check);
761761

762762
code_ifthenelset if_code;
763-
if_code.add_source_location()=original_sloc;
763+
if_code.add_source_location()=original_loc;
764764
if_code.cond()=and_expr;
765765
if_code.then_case()=code_expressiont(throw_expr);
766766

@@ -1561,9 +1561,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
15611561
code_blockt block;
15621562
if(throw_runtime_exceptions)
15631563
{
1564-
codet null_dereference_check=get_null_dereference_check(
1565-
op[0],
1566-
i_it->source_location);
1564+
codet null_dereference_check=
1565+
throw_null_dereference_exception(
1566+
op[0],
1567+
i_it->source_location);
15671568
block.move_to_operands(null_dereference_check);
15681569
}
15691570
else
@@ -1598,7 +1599,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
15981599
if(throw_runtime_exceptions)
15991600
{
16001601
codet conditional_check=
1601-
get_class_cast_check(op[0], arg0, i_it->source_location);
1602+
throw_class_cast_exception(op[0], arg0, i_it->source_location);
16021603
c=std::move(conditional_check);
16031604
}
16041605
else
@@ -1844,13 +1845,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
18441845
const dereference_exprt element(data_plus_offset, element_type);
18451846

18461847
c=code_blockt();
1847-
codet bounds_check;
1848-
if(throw_runtime_exceptions)
1849-
bounds_check=
1850-
get_array_access_check(deref, op[1], i_it->source_location);
1851-
else
1852-
bounds_check=
1853-
get_array_bounds_check(deref, op[1], i_it->source_location);
1848+
codet bounds_check=throw_runtime_exceptions?
1849+
throw_array_access_exception(deref, op[1], i_it->source_location):
1850+
get_array_bounds_check(deref, op[1], i_it->source_location);
18541851

18551852
bounds_check.add_source_location()=i_it->source_location;
18561853
c.move_to_operands(bounds_check);
@@ -2460,7 +2457,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
24602457

24612458
if(throw_runtime_exceptions)
24622459
{
2463-
codet array_length_check=get_array_length_check(
2460+
codet array_length_check=throw_array_length_exception(
24642461
op[0],
24652462
i_it->source_location);
24662463
c.move_to_operands(array_length_check);
@@ -2509,7 +2506,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
25092506
c=code_blockt();
25102507
if(throw_runtime_exceptions)
25112508
{
2512-
codet array_length_check=get_array_length_check(
2509+
codet array_length_check=throw_array_length_exception(
25132510
op[0],
25142511
i_it->source_location);
25152512
c.move_to_operands(array_length_check);

‎src/java_bytecode/java_bytecode_convert_method_class.h

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -109,25 +109,25 @@ class java_bytecode_convert_methodt:public messaget
109109
const exprt &idx,
110110
const source_locationt &original_sloc);
111111

112-
codet get_array_access_check(
112+
codet throw_array_access_exception(
113113
const exprt &arraystruct,
114114
const exprt &idx,
115115
const source_locationt &original_sloc);
116116

117-
codet get_array_length_check(
117+
codet throw_array_length_exception(
118118
const exprt &length,
119119
const source_locationt &original_sloc);
120-
121-
codet get_null_dereference_check(
120+
121+
codet throw_null_dereference_exception(
122122
const exprt &expr,
123123
const source_locationt &original_sloc);
124124

125-
codet get_class_cast_check(
125+
codet throw_class_cast_exception(
126126
const exprt &class1,
127-
const exprt &class2,
127+
const exprt &class2,
128128
const source_locationt &original_sloc);
129-
130-
// return corresponding reference of variable
129+
130+
// return corresponding reference of variable
131131
const variablet &find_variable_for_slot(
132132
size_t address,
133133
variablest &var_list);

‎src/java_bytecode/java_bytecode_language.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ Function: java_bytecode_languaget::get_language_options
4242

4343
void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
4444
{
45-
throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
45+
throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
4646
assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
4747
string_refinement_enabled=cmd.isset("refine-strings");
4848
if(cmd.isset("java-max-input-array-length"))

‎src/java_bytecode/java_bytecode_language.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,8 @@ class java_bytecode_languaget:public languaget
5757
java_bytecode_languaget():
5858
max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT),
5959
max_user_array_length(0),
60-
throw_runtime_exceptions(false)
61-
{}
60+
throw_runtime_exceptions(false)
61+
{}
6262

6363
bool from_expr(
6464
const exprt &expr,

0 commit comments

Comments
 (0)