File tree Expand file tree Collapse file tree 1 file changed +5
-2
lines changed
Expand file tree Collapse file tree 1 file changed +5
-2
lines changed Original file line number Diff line number Diff line change 3131
3232#include < util/c_types.h>
3333#include < ansi-c/string_constant.h>
34- #include < java_bytecode/java_types.h>
3534
3635#include " format_strings.h"
3736
@@ -628,7 +627,11 @@ void goto_convertt::do_java_new_array(
628627 t_n->source_location =location;
629628
630629 const struct_typet &struct_type=to_struct_type (ns.follow (object_type));
631- PRECONDITION (is_valid_java_array (struct_type));
630+
631+ // Ideally we would have a check for `is_valid_java_array(struct_type)` but
632+ // `is_valid_java_array is part of the java_bytecode module and we cannot
633+ // introduce such dependencies. We do this simple check instead:
634+ PRECONDITION (struct_type.components ().size ()==3 );
632635
633636 // Init base class:
634637 dereference_exprt deref (lhs, object_type);
You can’t perform that action at this time.
0 commit comments