From a0c4f81b1d396c49c92c6e7b6c13a958601ff432 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 8 Feb 2025 13:44:42 +0100 Subject: [PATCH] fix test case --- .../key/speclang/njml/JmlMarkerDecision.java | 9 +++++ .../speclang/jml/JmlMarkerDecisionTest.java | 35 +++++++++++++++++++ .../speclang/jml/JmlMarkerDecitionTest.java | 32 ----------------- 3 files changed, 44 insertions(+), 32 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecisionTest.java delete mode 100644 key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecitionTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java index 555a64bbde4..18920891d2f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java @@ -129,6 +129,15 @@ private boolean consume(String str) { return false; } + /** + * Given a string of conditions of a JML comment, that method decides whether the conditions are + * met. + * + * @param foundKeys a string of conditions, e.g., {@code "+key+esc-float"}. Should not contain + * whitespaces. + * @return true whether the given conditions are met and the comment should be considered as + * active. + */ public boolean isActiveJmlSpec(String foundKeys) { if (foundKeys.isEmpty()) { // a JML annotation with no keys is always included, diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecisionTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecisionTest.java new file mode 100644 index 00000000000..efb418395cc --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecisionTest.java @@ -0,0 +1,35 @@ +/* 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.speclang.jml; + +import de.uka.ilkd.key.speclang.njml.JmlMarkerDecision; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; + + +public class JmlMarkerDecisionTest { + + @Test + public void testIsActiveJmlSpec() { + JmlMarkerDecision dec = new JmlMarkerDecision(null); + assertFalse(dec.isActiveJmlSpec("+ESC")); + assertFalse(dec.isActiveJmlSpec("+a+b+c")); + assertFalse(dec.isActiveJmlSpec("+a")); + assertFalse(dec.isActiveJmlSpec("-key+key")); + assertFalse(dec.isActiveJmlSpec("-")); + assertFalse(dec.isActiveJmlSpec("+")); + assertFalse(dec.isActiveJmlSpec("+ke y")); + + assertTrue(dec.isActiveJmlSpec("+key-a b")); + assertTrue(dec.isActiveJmlSpec("+a+key")); + assertTrue(dec.isActiveJmlSpec("+key")); + assertTrue(dec.isActiveJmlSpec("+key")); + assertTrue(dec.isActiveJmlSpec("+KEY")); + assertTrue(dec.isActiveJmlSpec("+KEY")); + assertTrue(dec.isActiveJmlSpec("")); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecitionTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecitionTest.java deleted file mode 100644 index 4e781f6be79..00000000000 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/JmlMarkerDecitionTest.java +++ /dev/null @@ -1,32 +0,0 @@ -/* 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.speclang.jml; - -import de.uka.ilkd.key.speclang.njml.JmlMarkerDecision; - -import org.junit.jupiter.api.Assertions; -import org.junit.jupiter.api.Test; - - -public class JmlMarkerDecitionTest { - - @Test - public void testIsActiveJmlSpec() { - JmlMarkerDecision dec = new JmlMarkerDecision(null); - Assertions.assertFalse(dec.isActiveJmlSpec("+ESC")); - Assertions.assertFalse(dec.isActiveJmlSpec("+a+b+c")); - Assertions.assertFalse(dec.isActiveJmlSpec("+a")); - Assertions.assertFalse(dec.isActiveJmlSpec("-key+key")); - Assertions.assertFalse(dec.isActiveJmlSpec("-")); - Assertions.assertFalse(dec.isActiveJmlSpec("+")); - Assertions.assertFalse(dec.isActiveJmlSpec("+ke y")); - Assertions.assertFalse(dec.isActiveJmlSpec("+key-a b")); - Assertions.assertTrue(dec.isActiveJmlSpec("+a+key")); - Assertions.assertTrue(dec.isActiveJmlSpec("+key")); - Assertions.assertTrue(dec.isActiveJmlSpec("+key")); - Assertions.assertTrue(dec.isActiveJmlSpec("+KEY")); - Assertions.assertTrue(dec.isActiveJmlSpec("+KEY")); - Assertions.assertTrue(dec.isActiveJmlSpec("")); - } -}