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 0dafac2 commit 1fa64a9Copy full SHA for 1fa64a9
src/goto-programs/builtin_functions.cpp
@@ -31,7 +31,6 @@ 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
@@ -628,7 +627,11 @@ void goto_convertt::do_java_new_array(
628
627
t_n->source_location=location;
629
630
const struct_typet &struct_type=to_struct_type(ns.follow(object_type));
631
- PRECONDITION(is_valid_java_array(struct_type));
+
+ // 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);
635
636
// Init base class:
637
dereference_exprt deref(lhs, object_type);
0 commit comments