Skip to content

Commit

Permalink
Fix and Test String.equals(Object) Implementation in JPF (#491)
Browse files Browse the repository at this point in the history
* adding a test for equals method

* Add test for equals method in JPF
  • Loading branch information
shreyasCs012 authored Aug 13, 2024
1 parent 6233e3b commit 17cfba7
Show file tree
Hide file tree
Showing 4 changed files with 24 additions and 8 deletions.
Binary file added file
Binary file not shown.
1 change: 1 addition & 0 deletions output.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
After.
16 changes: 8 additions & 8 deletions src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
Original file line number Diff line number Diff line change
Expand Up @@ -165,16 +165,16 @@ public boolean equals0___3C_3CI__Z (MJIEnv env, int clsObjRef, int charsRef1, in

@MJI
public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int argRef) {
if (argRef == MJIEnv.NULL) {
return false;
if (argRef == MJIEnv.NULL) {
return false;
}

String s1 = env.getStringObject(objRef);
String s2 = env.getStringObject(argRef);

return s1.equals(s2);
if (env.isInstanceOf(argRef, "java.lang.String")) {
String s1 = env.getStringObject(objRef);
String s2 = env.getStringObject(argRef);
return s1.equals(s2);
}
return false;
}

@MJI
public boolean equalsIgnoreCase__Ljava_lang_String_2__Z (MJIEnv env, int objref, int anotherString) {
String thisString = env.getStringObject(objref);
Expand Down
15 changes: 15 additions & 0 deletions src/tests/java11/StringEqualsTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package java11;

import gov.nasa.jpf.util.test.TestJPF;
import org.junit.Test;
public class StringEqualsTest extends TestJPF {
@Test
public void testStringEqual_differentObj(){
if(verifyNoPropertyViolation()){
String word="a";
boolean actual=word.equals(new Object());
boolean expected =false;
assertEquals(expected,actual);
}
}
}

0 comments on commit 17cfba7

Please sign in to comment.