File tree Expand file tree Collapse file tree 1 file changed +26
-4
lines changed
Expand file tree Collapse file tree 1 file changed +26
-4
lines changed Original file line number Diff line number Diff 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 {
You can’t perform that action at this time.
0 commit comments