Skip to content

Commit

Permalink
fix issue, identity with position
Browse files Browse the repository at this point in the history
  • Loading branch information
wadoon committed Apr 27, 2024
1 parent e10cba9 commit 7ac2033
Show file tree
Hide file tree
Showing 3 changed files with 62 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -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());
}
}
}
Original file line number Diff line number Diff line change
@@ -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() {
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -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.
Expand Down

0 comments on commit 7ac2033

Please sign in to comment.