Merge pull request #5177 from diffblue/jbmc-deprecated

jbmc: avoid deprecated constructors

Author: Daniel Kroening

jbmc/src/java_bytecode/code_with_references.cpp

@@ -40,7 +40,7 @@ reference_allocationt::to_code(reference_substitutiont &references) const
   // the file.
   code_blockt code;
   code.add(code_assignt{*reference.array_length,
-                        side_effect_expr_nondett{java_int_type()}});
+                        side_effect_expr_nondett{java_int_type(), loc}});
   code.add(code_assumet{binary_predicate_exprt{
     *reference.array_length, ID_ge, from_integer(0, java_int_type())}});
   code.add(allocate_array(reference.expr, *reference.array_length, loc));

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -28,10 +28,10 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
   const index_exprt valid_index =
     index_exprt(valid_symbol_expr, valid_constant);
   const index_exprt index_plain = index_exprt(exprt(), exprt());
-  const byte_extract_exprt byte_little_endian =
-    byte_extract_exprt(ID_byte_extract_little_endian);
+  const byte_extract_exprt byte_little_endian = byte_extract_exprt(
+    ID_byte_extract_little_endian, exprt(), exprt(), typet());
   const byte_extract_exprt byte_big_endian =
-    byte_extract_exprt(ID_byte_extract_big_endian);
+    byte_extract_exprt(ID_byte_extract_big_endian, exprt(), exprt(), typet());
   const address_of_exprt valid_address = address_of_exprt(valid_symbol_expr);
   const address_of_exprt invalid_address = address_of_exprt(exprt());
   const struct_exprt struct_plain =