From 7ac20333683a4bf849fcf9d69b2363f73b7aa310 Mon Sep 17 00:00:00 2001
From: Alexander Weigl <weigl@kit.edu>
Date: Sat, 27 Apr 2024 18:31:54 +0200
Subject: [PATCH] fix issue, identity with position

---
 .../java/com/github/javaparser/JKIssue.java   | 44 +++++++++++++++++++
 .../JKIssueDoubleContract.java                | 14 ++++++
 .../github/javaparser/jml/JmlProcessor.java   |  5 ++-
 3 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java
 create mode 100644 javaparser-core-testing/src/test/test_sourcecode/JKIssueDoubleContract.java

diff --git a/javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java b/javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java
new file mode 100644
index 0000000000..92c543fec2
--- /dev/null
+++ b/javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java
@@ -0,0 +1,44 @@
+/*
+ * Copyright (C) 2013-2024 The JavaParser Team.
+ *
+ * This file is part of JavaParser.
+ *
+ * JavaParser can be used either under the terms of
+ * a) the GNU Lesser General Public License as published by
+ *     the Free Software Foundation, either version 3 of the License, or
+ *     (at your option) any later version.
+ * b) the terms of the Apache License
+ *
+ * You should have received a copy of both licenses in LICENCE.LGPL and
+ * LICENCE.APACHE. Please refer to those files for details.
+ *
+ * JavaParser is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU Lesser General Public License for more details.
+ */
+
+package com.github.javaparser;
+
+import com.github.javaparser.ast.CompilationUnit;
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.Test;
+
+import java.io.IOException;
+import java.nio.file.Paths;
+
+public class JKIssue {
+    @Test()
+    void test() throws IOException {
+        ParserConfiguration cfg = new ParserConfiguration();
+        cfg.setProcessJml(true);
+        JavaParser parser = new JavaParser(cfg);
+        CompilationUnit cu = parser.parse(Paths.get("src/test/test_sourcecode/JKIssueDoubleContract.java"))
+                .getResult().get();
+
+        var methods = cu.getPrimaryType().get().getMethods();
+        for (var method : methods) {
+            Assertions.assertEquals(1, method.getContracts().get().size());
+        }
+    }
+}
diff --git a/javaparser-core-testing/src/test/test_sourcecode/JKIssueDoubleContract.java b/javaparser-core-testing/src/test/test_sourcecode/JKIssueDoubleContract.java
new file mode 100644
index 0000000000..4c6962358c
--- /dev/null
+++ b/javaparser-core-testing/src/test/test_sourcecode/JKIssueDoubleContract.java
@@ -0,0 +1,14 @@
+/**
+ * Created by jklamroth on 12/18/18.
+ */
+public class JKIssueDoubleContract {
+
+    //@ ensures \result == 56;
+    private int test() {
+    }
+
+
+    //@ ensures \result == 56;
+    private int test1() {
+    }
+}
\ No newline at end of file
diff --git a/javaparser-core/src/main/java/com/github/javaparser/jml/JmlProcessor.java b/javaparser-core/src/main/java/com/github/javaparser/jml/JmlProcessor.java
index 5fe04cedab..c24a4d39e1 100644
--- a/javaparser-core/src/main/java/com/github/javaparser/jml/JmlProcessor.java
+++ b/javaparser-core/src/main/java/com/github/javaparser/jml/JmlProcessor.java
@@ -23,6 +23,7 @@
 import com.github.javaparser.ast.visitor.Visitable;
 import org.jetbrains.annotations.Nullable;
 import java.util.*;
+import java.util.stream.IntStream;
 
 /**
  * Here happens the JML magic. This post-processor consumes {@link JmlDoc}
@@ -143,7 +144,9 @@ public JmlDocDeclaration visit(JmlDocDeclaration n, Void arg) {
                 setJmlTags(t);
                 TypeDeclaration<?> parent = (TypeDeclaration<?>) n.getParentNode().get();
                 NodeList<BodyDeclaration<?>> members = parent.getMembers();
-                int pos = members.indexOf(n);
+                int pos = IntStream.range(0, members.size())
+                        .filter(i -> members.get(i) == n)
+                        .findFirst().orElse(-1);
                 assert pos >= 0;
                 if (pos + 1 >= members.size()) {
                     //JML Documentation is last element, therefore it can only refer to upper element.