We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 465e5dc commit 42c079dCopy full SHA for 42c079d
src/goto-programs/builtin_functions.cpp
@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
31
32
#include <util/c_types.h>
33
#include <ansi-c/string_constant.h>
34
+#include <java_bytecode/java_types.h>
35
36
#include "format_strings.h"
37
@@ -627,7 +628,7 @@ void goto_convertt::do_java_new_array(
627
628
t_n->source_location=location;
629
630
const struct_typet &struct_type=to_struct_type(ns.follow(object_type));
- PRECONDITION(struct_type.components().size() == 3);
631
+ PRECONDITION(is_valid_java_array(struct_type));
632
633
// Init base class:
634
dereference_exprt deref(lhs, object_type);
0 commit comments