-
Notifications
You must be signed in to change notification settings - Fork 29
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
10 changed files
with
220 additions
and
45 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,44 @@ | ||
| /* This file is part of KeY - https://key-project.org | ||
| * KeY is licensed under the GNU General Public License Version 2 | ||
| * SPDX-License-Identifier: GPL-2.0-only */ | ||
| package de.uka.ilkd.key.util; | ||
|
|
||
| import java.util.LinkedList; | ||
| import java.util.Queue; | ||
|
|
||
| import de.uka.ilkd.key.logic.Term; | ||
| import de.uka.ilkd.key.logic.op.Operator; | ||
|
|
||
| import org.jspecify.annotations.NonNull; | ||
|
|
||
| /** | ||
| * @author Alexander Weigl | ||
| * @version 1 (06.02.25) | ||
| */ | ||
| public class TermUtil { | ||
|
|
||
| /** | ||
| * Checks if a given term contains a specific operator. | ||
| * | ||
| * This method performs a breadth-first search on the term's subterms to find | ||
| * the specified operator. | ||
| * | ||
| * Caveat: It does not return true if op (only) occurs as the target of an update in term. | ||
| * | ||
| * @param term the term to be checked | ||
| * @param op the operator to search for | ||
| * @return true if the term or any of its subterms contains the operator, false otherwise | ||
| */ | ||
| public static boolean contains(@NonNull Term term, @NonNull Operator op) { | ||
| Queue<Term> queue = new LinkedList<>(); | ||
| queue.add(term); | ||
| while (!queue.isEmpty()) { | ||
| Term current = queue.poll(); | ||
| if (current.op() == op) { | ||
| return true; | ||
| } | ||
| queue.addAll(current.subs().toList()); | ||
| } | ||
| return false; | ||
| } | ||
| } |
57 changes: 57 additions & 0 deletions
57
key.core/src/test/java/de/uka/ilkd/key/nparser/Issue3452Test.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,57 @@ | ||
| /* This file is part of KeY - https://key-project.org | ||
| * KeY is licensed under the GNU General Public License Version 2 | ||
| * SPDX-License-Identifier: GPL-2.0-only */ | ||
| package de.uka.ilkd.key.nparser; | ||
|
|
||
| import java.io.File; | ||
|
|
||
| import de.uka.ilkd.key.control.KeYEnvironment; | ||
| import de.uka.ilkd.key.java.Services; | ||
| import de.uka.ilkd.key.logic.Namespace; | ||
| import de.uka.ilkd.key.logic.op.JFunction; | ||
| import de.uka.ilkd.key.proof.init.ProofInputException; | ||
| import de.uka.ilkd.key.proof.io.ProblemLoaderException; | ||
|
|
||
| import org.junit.jupiter.api.Test; | ||
|
|
||
| import static org.junit.jupiter.api.Assertions.*; | ||
|
|
||
| /** | ||
| * @author Alexander Weigl | ||
| * @version 1 (31.01.25) | ||
| */ | ||
| public class Issue3452Test { | ||
|
|
||
|
|
||
| @Test | ||
| void testNoStateParsedCorrectly() throws ProblemLoaderException, ProofInputException { | ||
| final var input = | ||
| new File( | ||
| "src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java"); | ||
| var env = KeYEnvironment.load(input, null, null, null); | ||
| final var contract = env.getProofContracts().getFirst(); | ||
| var po = contract.createProofObl(env.getInitConfig(), contract); | ||
| var proof = env.createProof(po); // just to ensure there is exception | ||
| Services services = proof.getInitConfig().getServices(); | ||
| Namespace<JFunction> functions = services.getNamespaces().functions(); | ||
| assertEquals("[int]", functions.lookup("A::b").argSorts().toString()); | ||
| assertEquals("[Heap,int]", functions.lookup("A::c").argSorts().toString()); | ||
| } | ||
|
|
||
| @Test | ||
| void testIllegalNoState() throws ProblemLoaderException, ProofInputException { | ||
| final var input = | ||
| new File( | ||
| "src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java"); | ||
|
|
||
| ProblemLoaderException exception = assertThrows(ProblemLoaderException.class, () -> { | ||
| var env = KeYEnvironment.load(input, null, null, null); | ||
| System.err.println(env); | ||
| System.err.println("Unexpected load success"); | ||
| }); | ||
|
|
||
| if (!exception.getMessage().startsWith("Heap used in a `no_state` method.")) { | ||
| fail("Unexpected exception message: " + exception.getMessage()); | ||
| } | ||
| } | ||
| } |
30 changes: 30 additions & 0 deletions
30
key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| class A { | ||
| /*@ public model_behaviour | ||
| @ requires n >= 0; | ||
| @ ensures \result.length == n; | ||
| @ measured_by n; | ||
| @ public no_state static model \seq b(\bigint n) { | ||
| @ return n == 0 ? \seq_empty : \seq_concat(b(n-1), \seq(0)); | ||
| @ } | ||
| @*/ | ||
|
|
||
| /*@ public model_behaviour | ||
| @ requires n >= 0; | ||
| @ ensures \result.length == n; | ||
| @ accessible \nothing; | ||
| @ measured_by n; | ||
| @ public static model \seq c(\bigint n) { | ||
| @ return n == 0 ? \seq_empty : \seq_concat(c(n-1), \seq(0)); | ||
| @ } | ||
| @*/ | ||
|
|
||
| int someHeapField; | ||
|
|
||
| //@ ensures true; | ||
| void m() { | ||
| //@ ghost \seq x = c(5); | ||
| someHeapField = 42; | ||
| //@ assert x == c(5); | ||
| } | ||
|
|
||
| } |
10 changes: 10 additions & 0 deletions
10
...e/src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| class A { | ||
|
|
||
| /*@ public static no_state model int obs() { | ||
| @ return A.someHeapField; | ||
| @ } | ||
| @*/ | ||
|
|
||
| static int someHeapField; | ||
|
|
||
| } |