Skip to content

Commit c77e6a1

Browse files
codebyzebromainbrenguier
authored andcommitted
Implement model for String.equals
String.equals is currently handled internally by CBMC, here we update the model so that String.equals is supported when we move support to models-library.
1 parent c86885c commit c77e6a1

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/main/java/java/lang/String.java

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1390,11 +1390,12 @@ public byte[] getBytes() {
13901390
* @see #equalsIgnoreCase(String)
13911391
*
13921392
* @diffblue.fullSupport
1393-
* @diffblue.untested
13941393
*/
13951394
public boolean equals(Object anObject) {
1396-
// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
1397-
return CProver.nondetBoolean();
1395+
if (anObject instanceof String) {
1396+
return CProverString.equals((String)anObject, this);
1397+
}
1398+
return false;
13981399
}
13991400

14001401
/**
@@ -1611,7 +1612,7 @@ public int compareTo(String anotherString) {
16111612
// DIFFBLUE MODEL LIBRARY For some reason this needs to be not null for
16121613
// FileReader tests to pass.
16131614
public static final Comparator<String> CASE_INSENSITIVE_ORDER
1614-
= CProver.nondetWithoutNullForNotModelled();
1615+
= null;
16151616
// DIFFBLUE MODEL LIBRARY Not needed for modelling
16161617
// private static class CaseInsensitiveComparator
16171618
// implements Comparator<String>, java.io.Serializable {

0 commit comments

Comments
 (0)