Skip to content

Commit 97aaf65

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 97aaf65

File tree

1 file changed

+26
-4
lines changed

1 file changed

+26
-4
lines changed

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

Lines changed: 26 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1390,11 +1390,33 @@ 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 (this == anObject) {
1396+
// return true;
1397+
// }
1398+
// if (anObject instanceof String) {
1399+
// String anotherString = (String)anObject;
1400+
// int n = value.length;
1401+
// if (n == anotherString.value.length) {
1402+
// char v1[] = value;
1403+
// char v2[] = anotherString.value;
1404+
// int i = 0;
1405+
// while (n-- != 0) {
1406+
// if (v1[i] != v2[i])
1407+
// return false;
1408+
// i++;
1409+
// }
1410+
// return true;
1411+
// }
1412+
// }
1413+
// return false;
1414+
1415+
// DIFFBLUE MODEL LIBRARY Use CProverString function
1416+
if (anObject instanceof String) {
1417+
return CProverString.equals((String) anObject, this);
1418+
}
1419+
return false;
13981420
}
13991421

14001422
/**
@@ -1611,7 +1633,7 @@ public int compareTo(String anotherString) {
16111633
// DIFFBLUE MODEL LIBRARY For some reason this needs to be not null for
16121634
// FileReader tests to pass.
16131635
public static final Comparator<String> CASE_INSENSITIVE_ORDER
1614-
= CProver.nondetWithoutNullForNotModelled();
1636+
= null;
16151637
// DIFFBLUE MODEL LIBRARY Not needed for modelling
16161638
// private static class CaseInsensitiveComparator
16171639
// implements Comparator<String>, java.io.Serializable {

0 commit comments

Comments
 (0)