initialize JMLTransformer with defined active JML annotation markers

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java

@@ -73,7 +73,8 @@ public final class JMLTransformer extends JavaTransformer {
 
     private static final Logger LOGGER = LoggerFactory.getLogger(JMLTransformer.class);
 
-    private final JmlDocSanitizer sanitizer = new JmlDocSanitizer(Set.of("key"));
+    private final JmlDocSanitizer sanitizer = new JmlDocSanitizer(
+            ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings().getJmlEnabledKeys());
 
     /// KEY for contracts
     public static final DataKey<List<TextualJMLConstruct>> KEY_SPEC_CASE = new DataKey<>() {

key.core/src/test/resources/testcase/loopScopeInvRule/Test.java

@@ -1,35 +1,36 @@
 public class Test {
-  /*@ public normal_behavior
-    @ requires i >= 0;
-    @ ensures (\result == 0 || \result <= -1) && ((flag && \old(i) < 17) ==> \result == -2) ;
-    @*/
-  public static int loopScopeRuleBenchmark(int i, boolean flag) {
-    k: {
-      /*@ loop_invariant
-        @   i >= 0 && i <= \old(i);
-        @ decreases i;
-        @*/
-      l: while (i > 0) {
-        if (i == 17) {
-          i = 0;
-          continue l; // have to prove the invariant
-        } else if (i == 42) {
-          i = -1;
-          break l;    // have to prove the postcondition!
-        } else if (i == 2048) {
-          i = -1;
-          break k;    // have to prove the postcondition
-        }
+    /*@ public normal_behavior
+      @ requires i >= 0;
+      @ ensures (\result == 0 || \result <= -1) && ((flag && \old(i) < 17) ==> \result == -2) ;
+      @*/
+    public static int loopScopeRuleBenchmark(int i, boolean flag) {
+        k:
+        {
+           /*@ loop_invariant
+             @   i >= 0 && i <= \old(i);
+             @ decreases i;
+             @*/
+            l:
+            while (i > 0) {
+                if (i == 17) {
+                    i = 0;
+                    continue l; // have to prove the invariant
+                } else if (i == 42) {
+                    i = -1;
+                    break l;    // have to prove the postcondition!
+                } else if (i == 2048) {
+                    i = -1;
+                    break k;    // have to prove the postcondition
+                }
+                i--;
+            }
 
-        i--;
-      }
+            if (flag) {
+                i = -2;
+                break k;
+            }
+        }
 
-      if (flag) {
-        i = -2;
-        break k;
-      }
+        return i;
     }
-
-    return i;
-  }
 }