Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit ce59649

Browse files
committedJul 20, 2018
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 6b422b1 commit ce59649

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed
 

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

Lines changed: 4 additions & 3 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
/**

0 commit comments

Comments
 (0)
Please sign in to comment.