diff --git a/file b/file new file mode 100644 index 00000000..c9d5dc60 Binary files /dev/null and b/file differ diff --git a/output.txt b/output.txt new file mode 100644 index 00000000..39e2f69b --- /dev/null +++ b/output.txt @@ -0,0 +1 @@ +After. diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java index a165c772..ee0e6d26 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java @@ -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); diff --git a/src/tests/java11/StringEqualsTest.java b/src/tests/java11/StringEqualsTest.java new file mode 100644 index 00000000..d2d3369e --- /dev/null +++ b/src/tests/java11/StringEqualsTest.java @@ -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); + } + } +}