Skip to content

Commit 8d09d98

Browse files
Add unit test for assign_from_json
This in particular check that an array field (which is not marked nondet and not a reference) is allocated with a constant size.
1 parent 5efb648 commit 8d09d98

File tree

2 files changed

+413
-0
lines changed

2 files changed

+413
-0
lines changed

jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
4848
java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
4949
java_bytecode/java_object_factory/struct_tag_types.cpp \
5050
java_bytecode/java_replace_nondet/replace_nondet.cpp \
51+
java_bytecode/java_static_initializers/assignments_from_json.cpp \
5152
java_bytecode/java_static_initializers/java_static_initializers.cpp \
5253
java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
5354
java_bytecode/java_trace_validation/java_trace_validation.cpp \

0 commit comments

Comments
 (0)