Skip to content

Commit d7ddf59

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location
Always give a location to side effect expr
2 parents e448db6 + 119e88b commit d7ddf59

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+301
-213
lines changed

‎jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ static void instrument_synchronized_code(
253253
catch_block.add(monitorexit);
254254

255255
// Re-throw exception
256-
side_effect_expr_throwt throw_expr;
256+
side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
257257
throw_expr.copy_to_operands(catch_var);
258258
catch_block.add(code_expressiont(throw_expr));
259259

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -812,9 +812,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
812812
code_declt declare_cloned(local_symexpr);
813813
clone_body.move_to_operands(declare_cloned);
814814

815+
source_locationt location;
816+
location.set_function(local_name);
815817
side_effect_exprt java_new_array(
816-
ID_java_new_array,
817-
java_reference_type(symbol_type));
818+
ID_java_new_array, java_reference_type(symbol_type), location);
818819
dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
819820
dereference_exprt new_array(local_symexpr, symbol_type);
820821
member_exprt old_length(
@@ -860,7 +861,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
860861
copy_loop.cond()=
861862
binary_relation_exprt(index_symexpr, ID_lt, old_length);
862863

863-
side_effect_exprt inc(ID_assign);
864+
side_effect_exprt inc(ID_assign, typet(), location);
864865
inc.operands().resize(2);
865866
inc.op0()=index_symexpr;
866867
inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp‎

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2328,8 +2328,7 @@ void java_bytecode_convert_methodt::convert_athrow(
23282328
}
23292329
else
23302330
{
2331-
side_effect_expr_throwt throw_expr;
2332-
throw_expr.add_source_location() = location;
2331+
side_effect_expr_throwt throw_expr(irept(), typet(), location);
23332332
throw_expr.copy_to_operands(op[0]);
23342333
c = code_expressiont(throw_expr);
23352334
}
@@ -2454,14 +2453,11 @@ void java_bytecode_convert_methodt::convert_multianewarray(
24542453
codet &c,
24552454
exprt::operandst &results)
24562455
{
2456+
PRECONDITION(!location.get_line().empty());
24572457
const reference_typet ref_type = java_reference_type(arg0.type());
2458-
2459-
side_effect_exprt java_new_array(ID_java_new_array, ref_type);
2458+
side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
24602459
java_new_array.operands() = op;
24612460

2462-
if(!location.get_line().empty())
2463-
java_new_array.add_source_location() = location;
2464-
24652461
code_blockt create;
24662462

24672463
if(max_array_length != 0)
@@ -2516,12 +2512,9 @@ void java_bytecode_convert_methodt::convert_newarray(
25162512

25172513
const reference_typet ref_type = java_array_type(element_type);
25182514

2519-
side_effect_exprt java_new_array(ID_java_new_array, ref_type);
2515+
side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
25202516
java_new_array.copy_to_operands(op[0]);
25212517

2522-
if(!location.get_line().empty())
2523-
java_new_array.add_source_location() = location;
2524-
25252518
c = code_blockt();
25262519

25272520
if(max_array_length != 0)
@@ -2543,7 +2536,7 @@ void java_bytecode_convert_methodt::convert_new(
25432536
exprt::operandst &results)
25442537
{
25452538
const reference_typet ref_type = java_reference_type(arg0.type());
2546-
side_effect_exprt java_new_expr(ID_java_new, ref_type);
2539+
side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
25472540

25482541
if(!location.get_line().empty())
25492542
java_new_expr.add_source_location() = location;

‎jbmc/src/java_bytecode/java_bytecode_instrument.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,10 @@ codet java_bytecode_instrumentt::throw_exception(
122122
ID_java,
123123
symbol_table);
124124

125-
side_effect_exprt new_instance(ID_java_new, exc_ptr_type);
125+
side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
126126
code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
127127

128-
side_effect_expr_throwt throw_expr;
128+
side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
129129
throw_expr.copy_to_operands(new_symbol.symbol_expr());
130130

131131
code_blockt throw_code;

‎jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,6 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
160160
<< component_name << "` in class hierarchy" << eom;
161161

162162
// We replace by a non-det of same type
163-
side_effect_expr_nondett nondet(expr.type());
163+
side_effect_expr_nondett nondet(expr.type(), expr.source_location());
164164
expr.swap(nondet);
165165
}

‎jbmc/src/java_bytecode/java_entry_point.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ static void java_static_lifetime_init(
162162
// Call the literal initializer method instead of a nondet initializer:
163163

164164
// For arguments we can't parse yet:
165-
side_effect_expr_nondett nondet_bool(java_boolean_type());
165+
side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);
166166

167167
// Argument order is: name, isAnnotation, isArray, isInterface,
168168
// isSynthetic, isLocalClass, isMemberClass, isEnum

0 commit comments

Comments
 (0)