Merge pull request #2700 from romainbrenguier/clean-up/side-effect-location

Always give a location to side effect expr

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -253,7 +253,7 @@ static void instrument_synchronized_code(
   catch_block.add(monitorexit);
 
   // Re-throw exception
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
   throw_expr.copy_to_operands(catch_var);
   catch_block.add(code_expressiont(throw_expr));
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -812,9 +812,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_declt declare_cloned(local_symexpr);
     clone_body.move_to_operands(declare_cloned);
 
+    source_locationt location;
+    location.set_function(local_name);
     side_effect_exprt java_new_array(
-      ID_java_new_array,
-      java_reference_type(symbol_type));
+      ID_java_new_array, java_reference_type(symbol_type), location);
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
     dereference_exprt new_array(local_symexpr, symbol_type);
     member_exprt old_length(
@@ -860,7 +861,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     copy_loop.cond()=
       binary_relation_exprt(index_symexpr, ID_lt, old_length);
 
-    side_effect_exprt inc(ID_assign);
+    side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
     inc.op0()=index_symexpr;
     inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2328,8 +2328,7 @@ void java_bytecode_convert_methodt::convert_athrow(
   }
   else
   {
-    side_effect_expr_throwt throw_expr;
-    throw_expr.add_source_location() = location;
+    side_effect_expr_throwt throw_expr(irept(), typet(), location);
     throw_expr.copy_to_operands(op[0]);
     c = code_expressiont(throw_expr);
   }
@@ -2454,14 +2453,11 @@ void java_bytecode_convert_methodt::convert_multianewarray(
   codet &c,
   exprt::operandst &results)
 {
+  PRECONDITION(!location.get_line().empty());
   const reference_typet ref_type = java_reference_type(arg0.type());
-
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.operands() = op;
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   code_blockt create;
 
   if(max_array_length != 0)
@@ -2516,12 +2512,9 @@ void java_bytecode_convert_methodt::convert_newarray(
 
   const reference_typet ref_type = java_array_type(element_type);
 
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.copy_to_operands(op[0]);
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   c = code_blockt();
 
   if(max_array_length != 0)
@@ -2543,7 +2536,7 @@ void java_bytecode_convert_methodt::convert_new(
   exprt::operandst &results)
 {
   const reference_typet ref_type = java_reference_type(arg0.type());
-  side_effect_exprt java_new_expr(ID_java_new, ref_type);
+  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
 
   if(!location.get_line().empty())
     java_new_expr.add_source_location() = location;

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -122,10 +122,10 @@ codet java_bytecode_instrumentt::throw_exception(
       ID_java,
       symbol_table);
 
-  side_effect_exprt new_instance(ID_java_new, exc_ptr_type);
+  side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
 
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
   throw_expr.copy_to_operands(new_symbol.symbol_expr());
 
   code_blockt throw_code;

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -160,6 +160,6 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
             << component_name << "` in class hierarchy" << eom;
 
   // We replace by a non-det of same type
-  side_effect_expr_nondett nondet(expr.type());
+  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
   expr.swap(nondet);
 }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -162,7 +162,7 @@ static void java_static_lifetime_init(
         // Call the literal initializer method instead of a nondet initializer:
 
         // For arguments we can't parse yet:
-        side_effect_expr_nondett nondet_bool(java_boolean_type());
+        side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);
 
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum