Skip to content

Commit b3c08d3

Browse files
author
svorenova
committed
Mark internal Java variables with ID_C_no_nondet_initialization
This sets the flag to be true for java::@inflight_exception and static initializer internal variables (including clinit_already_run)
1 parent f2dc978 commit b3c08d3

File tree

2 files changed

+2
-0
lines changed

2 files changed

+2
-0
lines changed

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ void java_internal_additions(symbol_table_baset &dest)
5151
symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME;
5252
symbol.mode = ID_java;
5353
symbol.type = pointer_type(empty_typet());
54+
symbol.type.set(ID_C_no_nondet_initialization, true);
5455
symbol.value = null_pointer_exprt(to_pointer_type(symbol.type));
5556
symbol.is_file_local = false;
5657
symbol.is_static_lifetime = true;

jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ static symbolt add_new_variable_symbol(
9191
new_symbol.pretty_name = name;
9292
new_symbol.base_name = name;
9393
new_symbol.type = type;
94+
new_symbol.type.set(ID_C_no_nondet_initialization, true);
9495
new_symbol.value = value;
9596
new_symbol.is_lvalue = true;
9697
new_symbol.is_state_var = true;

0 commit comments

Comments
 (0)