From 17cfba712280f4df44a08076ae34f321d028f627 Mon Sep 17 00:00:00 2001
From: Shreyas <shreyascs012@gmail.com>
Date: Tue, 13 Aug 2024 17:52:46 +0530
Subject: [PATCH]  Fix and Test String.equals(Object) Implementation in JPF
 (#491)

* adding a test for equals method

* Add test for equals method in JPF
---
 file                                            | Bin 0 -> 211 bytes
 output.txt                                      |   1 +
 .../gov/nasa/jpf/vm/JPF_java_lang_String.java   |  16 ++++++++--------
 src/tests/java11/StringEqualsTest.java          |  15 +++++++++++++++
 4 files changed, 24 insertions(+), 8 deletions(-)
 create mode 100644 file
 create mode 100644 output.txt
 create mode 100644 src/tests/java11/StringEqualsTest.java

diff --git a/file b/file
new file mode 100644
index 0000000000000000000000000000000000000000..c9d5dc60586ef6d0e7846dd19552e39ab0eab3b1
GIT binary patch
literal 211
zcmZ4UmVvdnh`}H|zf3PLu{cpLs~}CUB(=CiFE?2)C9xz?&p#<EHMu0Xq$o8pHv}l5
z;$K>lT2#JUTy;Wm&~_#UCQk;&d>;nZ%)GqRq7nupAD~hCAfxnwM(Kl$($7uS2N|W0
mVU#CGk99=>0|NsiiLL-^U8(ZMf_u8AA`=56&=r|rgO~tvxJKy!

literal 0
HcmV?d00001

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);
+        }
+    }
+}