Skip to content

Commit 1aa5bfd

Browse files
mgudemannDaniel Kroening
authored and
Daniel Kroening
committed
assert known Java object size
1 parent c54f78a commit 1aa5bfd

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#define DEBUG
10-
119
#ifdef DEBUG
1210
#include <iostream>
1311
#endif

src/java_bytecode/java_object_factory.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,8 +126,9 @@ exprt java_object_factoryt::allocate_object(
126126
// build size expression
127127
exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table));
128128

129-
if(allocate_type.id()!=ID_empty && !object_size.is_nil())
129+
if(allocate_type.id()!=ID_empty)
130130
{
131+
assert(!object_size.is_nil() && "size of Java objects should be known");
131132
// malloc expression
132133
exprt malloc_expr=side_effect_exprt(ID_malloc);
133134
malloc_expr.copy_to_operands(object_size);

0 commit comments

Comments
 (0)