Skip to content

Commit

Permalink
fix test case
Browse files Browse the repository at this point in the history
  • Loading branch information
wadoon committed Feb 8, 2025
1 parent 3456abd commit a0c4f81
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 32 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Original file line number Diff line number Diff line change
@@ -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(""));
}
}

This file was deleted.

0 comments on commit a0c4f81

Please sign in to comment.