Skip to content

Commit b6d4c72

Browse files
committed
activate JML parsing in JmlParser
1 parent 8050c4c commit b6d4c72

3 files changed

Lines changed: 8 additions & 6 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,7 @@
44
package de.uka.ilkd.key.java.loader;
55

66
import java.io.Reader;
7-
import java.util.ArrayList;
8-
import java.util.Collection;
9-
import java.util.List;
10-
import java.util.Optional;
7+
import java.util.*;
118

129
import de.uka.ilkd.key.java.Services;
1310
import de.uka.ilkd.key.java.ast.ResolvedLogicalType;
@@ -95,7 +92,11 @@ private ParserConfiguration getConfiguration() {
9592
if (config == null) {
9693
config = new ParserConfiguration();
9794
config.setStoreTokens(true);
95+
config.setKeepJmlDocs(false);
96+
config.setProcessJml(true);
9897
}
98+
// TODO update the activated JML keys with the current settings.
99+
config.setJmlKeys(Collections.singletonList(Collections.singletonList("key")));
99100
config.setLanguageLevel(ParserConfiguration.LanguageLevel.RAW);
100101
config.setSymbolResolver(getSymbolSolver());
101102
return config;

key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ public List<JavaTransformer> getSteps() {
3939
public static KeYJavaPipeline createDefault(TransformationPipelineServices pipelineServices) {
4040
KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices);
4141
p.add(new EnumClassBuilder(pipelineServices));
42-
p.add(new JMLTransformer(pipelineServices));
43-
p.add(new JmlDocRemoval(pipelineServices));
42+
//p.add(new JMLTransformer(pipelineServices));
43+
//p.add(new JmlDocRemoval(pipelineServices));
4444
p.add(new ImplicitFieldAdder(pipelineServices));
4545
p.add(new InstanceAllocationMethodBuilder(pipelineServices));
4646
p.add(new ConstructorNormalformBuilder(pipelineServices));

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
* Objects of this type represent the various JML specification constructs in textual, unprocessed
1919
* form.
2020
*/
21+
@Deprecated
2122
public abstract class TextualJMLConstruct {
2223

2324
protected final ImmutableList<JMLModifier> modifiers;

0 commit comments

Comments
 (0)