Skip to content

Commit cac4945

Browse files
author
svorenova
committed
Mark java.lang.String.Literals with ID_C_constant
This will also make sure that nondet-static option does not nondet- initialize these
1 parent 6e6fa82 commit cac4945

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

jbmc/src/java_bytecode/java_string_literals.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,7 @@ symbol_exprt get_or_create_string_literal_symbol(
8484
symbolt new_symbol;
8585
new_symbol.name = escaped_symbol_name_with_prefix;
8686
new_symbol.type = string_type;
87+
new_symbol.type.set(ID_C_constant, true);
8788
new_symbol.base_name = escaped_symbol_name;
8889
new_symbol.pretty_name = value;
8990
new_symbol.mode = ID_java;
@@ -131,6 +132,7 @@ symbol_exprt get_or_create_string_literal_symbol(
131132
array_symbol.is_state_var = true;
132133
array_symbol.value = data;
133134
array_symbol.type = array_symbol.value.type();
135+
array_symbol.type.set(ID_C_constant, true);
134136

135137
if(symbol_table.add(array_symbol))
136138
throw "failed to add constarray symbol to symbol table";
@@ -161,6 +163,7 @@ symbol_exprt get_or_create_string_literal_symbol(
161163
java_int_type(),
162164
symbol_table);
163165
return_symbol.type = return_symbol.value.type();
166+
return_symbol.type.set(ID_C_constant, true);
164167
if(symbol_table.add(return_symbol))
165168
throw "failed to add return symbol to symbol table";
166169

0 commit comments

Comments
 (0)