Skip to content

Commit 4024eee

Browse files
Antonia LechnerAntonia Lechner
Antonia Lechner
authored and
Antonia Lechner
committed
Rename skip_special_string_fields to is_string_type
There are more decisions associated with this variable than whether or not to skip the length and data fields.
1 parent b3967eb commit 4024eee

File tree

1 file changed

+5
-6
lines changed

1 file changed

+5
-6
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -803,12 +803,11 @@ void java_object_factoryt::gen_nondet_struct_init(
803803
java_string_library_preprocesst::implements_java_char_sequence(struct_type);
804804
const bool has_length_and_data =
805805
struct_type.has_component("length") && struct_type.has_component("data");
806-
const bool skip_special_string_fields =
807-
is_char_sequence && has_length_and_data;
806+
const bool is_string_type = is_char_sequence && has_length_and_data;
808807
const bool has_string_input_values =
809808
!object_factory_parameters.string_input_values.empty();
810809

811-
if(skip_special_string_fields && has_string_input_values && !skip_classid)
810+
if(is_string_type && has_string_input_values && !skip_classid)
812811
{ // We're dealing with a string and we should set fixed input values.
813812
// We create a switch statement where each case is an assignment
814813
// of one of the fixed input strings to the input variable in question
@@ -825,7 +824,7 @@ void java_object_factoryt::gen_nondet_struct_init(
825824
else if(
826825
(!is_sub && !skip_classid &&
827826
update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
828-
skip_special_string_fields)
827+
is_string_type)
829828
{
830829
// Add an initial all-zero write. Most of the fields of this will be
831830
// overwritten, but it helps to have a whole-structure write that analysis
@@ -842,7 +841,7 @@ void java_object_factoryt::gen_nondet_struct_init(
842841
// If the initialised type is a special-cased String type (one with length
843842
// and data fields introduced by string-library preprocessing), initialise
844843
// those fields with nondet values
845-
if(skip_special_string_fields)
844+
if(is_string_type)
846845
{ // We're dealing with a string
847846
initialize_nondet_string_fields(
848847
to_struct_expr(*initial_object),
@@ -882,7 +881,7 @@ void java_object_factoryt::gen_nondet_struct_init(
882881
code.add_source_location() = location;
883882
assignments.add(code);
884883
}
885-
else if(skip_special_string_fields && (name == "length" || name == "data"))
884+
else if(is_string_type && (name == "length" || name == "data"))
886885
{
887886
// In this case these were set up above.
888887
continue;

0 commit comments

Comments
 (0)