Skip to content

Commit 630100f

Browse files
Stop preprocessing String.hashCode
The internal version is only an over approximation of the behaviour. It's better to use the version from the models.
1 parent 0056df1 commit 630100f

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1517,9 +1517,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
15171517
cprover_equivalent_to_java_string_returning_function[format_signature] =
15181518
ID_cprover_string_format_func;
15191519

1520-
cprover_equivalent_to_java_function
1521-
["java::java.lang.String.hashCode:()I"]=
1522-
ID_cprover_string_hash_code_func;
15231520
cprover_equivalent_to_java_function
15241521
["java::java.lang.String.indexOf:(I)I"]=
15251522
ID_cprover_string_index_of_func;

0 commit comments

Comments
 (0)