Skip to content

Commit 9e6caba

Browse files
author
svorenova
committed
Mark final fields in Java as constants
This will also make sure that they won't get nondet-initialized with nondet-static option
1 parent 48797b0 commit 9e6caba

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -645,6 +645,7 @@ void java_bytecode_convert_classt::convert(
645645
// link matches the method used by java_bytecode_convert_method::convert
646646
// for methods.
647647
new_symbol.type.set(ID_C_class, class_symbol.name);
648+
new_symbol.type.set(ID_C_constant, f.is_final);
648649
new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
649650
"."+id2string(f.name);
650651
new_symbol.mode=ID_java;

0 commit comments

Comments
 (0)