add JML clauses in TypeCastingGenerator

* new tests from issues found by JJBMC
jmltoolkit · May 2, 2024 · 0f20de0 · 0f20de0
1 parent 30ce079
commit 0f20de0
Show file tree

Hide file tree

Showing 19 changed files with 351 additions and 21 deletions.
diff --git a/...erators/src/main/java/com/github/javaparser/generator/core/node/TypeCastingGenerator.java b/...erators/src/main/java/com/github/javaparser/generator/core/node/TypeCastingGenerator.java
@@ -45,7 +45,8 @@ public class TypeCastingGenerator extends NodeGenerator {
             JavaParserMetaModel.typeMetaModel,
             JavaParserMetaModel.moduleDirectiveMetaModel,
             JavaParserMetaModel.bodyDeclarationMetaModel,
-            JavaParserMetaModel.commentMetaModel
+            JavaParserMetaModel.commentMetaModel,
+            JavaParserMetaModel.jmlClauseMetaModel
     );
 
     public TypeCastingGenerator(SourceRoot sourceRoot) {

diff --git a/javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java b/javaparser-core-testing/src/test/java/com/github/javaparser/JKIssue.java
@@ -28,7 +28,7 @@
 import java.nio.file.Paths;
 
 public class JKIssue {
-    @Test()
+    @Test
     void test() throws IOException {
         ParserConfiguration cfg = new ParserConfiguration();
         cfg.setProcessJml(true);
@@ -41,4 +41,16 @@ void test() throws IOException {
             Assertions.assertEquals(1, method.getContracts().get().size());
         }
     }
+
+    @Test
+    void test2() throws IOException {
+        ParserConfiguration cfg = new ParserConfiguration();
+        cfg.setProcessJml(true);
+        JavaParser parser = new JavaParser(cfg);
+        CompilationUnit cu = parser.parse(Paths.get("src/test/test_sourcecode/MissingParentSimpleExprClause.java"))
+                .getResult().get();
+
+        var clause = cu.getType(0).getMethods().get(0).getContracts().get().get(0).getClauses().get(0).asJmlSimpleExprClause();
+        Assertions.assertEquals(1, clause.getChildNodes().size());
+    }
 }
diff --git a/javaparser-core-testing/src/test/test_sourcecode/MissingParentSimpleExprClause.java b/javaparser-core-testing/src/test/test_sourcecode/MissingParentSimpleExprClause.java
@@ -0,0 +1,4 @@
+public class JKIssueDoubleContract {
+    //@ ensures true;
+    private int test() {}
+}
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlCallableClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlCallableClause.java
@@ -10,6 +10,9 @@
 import com.github.javaparser.metamodel.JmlCallableClauseMetaModel;
 import com.github.javaparser.ast.Node;
 
+import java.util.Optional;
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/22/21)
@@ -58,4 +61,23 @@ public JmlCallableClauseMetaModel getMetaModel() {
     public JmlClauseKind getKind() {
         return JmlClauseKind.CALLABLE;
     }
+
+    @Override
+    public boolean isJmlCallableClause() {
+        return true;
+    }
+
+    @Override
+    public JmlCallableClause asJmlCallableClause() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlCallableClause> toJmlCallableClause() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlCallableClause(Consumer<JmlCallableClause> action) {
+        action.accept(this);
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlClause.java
@@ -13,6 +13,10 @@
 import com.github.javaparser.metamodel.OptionalProperty;
 import java.util.Optional;
 
+import static com.github.javaparser.utils.CodeGenerationUtils.f;
+
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/21/21)
@@ -116,4 +120,124 @@ public boolean replace(Node node, Node replacementNode) {
         }
         return super.replace(node, replacementNode);
     }
+
+    public boolean isJmlCallableClause() {
+        return false;
+    }
+
+    public JmlCallableClause asJmlCallableClause() {
+        throw new IllegalStateException(f("%s is not JmlCallableClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlCallableClause> toJmlCallableClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlCallableClause(Consumer<JmlCallableClause> action) {
+    }
+
+    public boolean isJmlClauseLabel() {
+        return false;
+    }
+
+    public JmlClauseLabel asJmlClauseLabel() {
+        throw new IllegalStateException(f("%s is not JmlClauseLabel, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlClauseLabel> toJmlClauseLabel() {
+        return Optional.empty();
+    }
+
+    public void ifJmlClauseLabel(Consumer<JmlClauseLabel> action) {
+    }
+
+    public boolean isJmlForallClause() {
+        return false;
+    }
+
+    public JmlForallClause asJmlForallClause() {
+        throw new IllegalStateException(f("%s is not JmlForallClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlForallClause> toJmlForallClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlForallClause(Consumer<JmlForallClause> action) {
+    }
+
+    public boolean isJmlMultiExprClause() {
+        return false;
+    }
+
+    public JmlMultiExprClause asJmlMultiExprClause() {
+        throw new IllegalStateException(f("%s is not JmlMultiExprClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlMultiExprClause> toJmlMultiExprClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlMultiExprClause(Consumer<JmlMultiExprClause> action) {
+    }
+
+    public boolean isJmlOldClause() {
+        return false;
+    }
+
+    public JmlOldClause asJmlOldClause() {
+        throw new IllegalStateException(f("%s is not JmlOldClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlOldClause> toJmlOldClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlOldClause(Consumer<JmlOldClause> action) {
+    }
+
+    public boolean isJmlSignalsClause() {
+        return false;
+    }
+
+    public JmlSignalsClause asJmlSignalsClause() {
+        throw new IllegalStateException(f("%s is not JmlSignalsClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlSignalsClause> toJmlSignalsClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlSignalsClause(Consumer<JmlSignalsClause> action) {
+    }
+
+    public boolean isJmlSignalsOnlyClause() {
+        return false;
+    }
+
+    public JmlSignalsOnlyClause asJmlSignalsOnlyClause() {
+        throw new IllegalStateException(f("%s is not JmlSignalsOnlyClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlSignalsOnlyClause> toJmlSignalsOnlyClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlSignalsOnlyClause(Consumer<JmlSignalsOnlyClause> action) {
+    }
+
+    public boolean isJmlSimpleExprClause() {
+        return false;
+    }
+
+    public JmlSimpleExprClause asJmlSimpleExprClause() {
+        throw new IllegalStateException(f("%s is not JmlSimpleExprClause, it is %s", this, this.getClass().getSimpleName()));
+    }
+
+    public Optional<JmlSimpleExprClause> toJmlSimpleExprClause() {
+        return Optional.empty();
+    }
+
+    public void ifJmlSimpleExprClause(Consumer<JmlSimpleExprClause> action) {
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlClauseLabel.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlClauseLabel.java
@@ -18,6 +18,8 @@
 import java.util.Optional;
 import static com.github.javaparser.utils.Utils.assertNotNull;
 
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/21/21)
@@ -185,4 +187,23 @@ public JmlClauseLabel setKind(final JmlClauseKind kind) {
         this.kind = kind;
         return this;
     }
+
+    @Override
+    public boolean isJmlClauseLabel() {
+        return true;
+    }
+
+    @Override
+    public JmlClauseLabel asJmlClauseLabel() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlClauseLabel> toJmlClauseLabel() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlClauseLabel(Consumer<JmlClauseLabel> action) {
+        action.accept(this);
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlForallClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlForallClause.java
@@ -14,6 +14,9 @@
 import com.github.javaparser.metamodel.JmlForallClauseMetaModel;
 import static com.github.javaparser.utils.Utils.assertNotNull;
 
+import java.util.Optional;
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/22/21)
@@ -114,4 +117,23 @@ public JmlForallClauseMetaModel getMetaModel() {
     public JmlClauseKind getKind() {
         return JmlClauseKind.FORALL;
     }
+
+    @Override
+    public boolean isJmlForallClause() {
+        return true;
+    }
+
+    @Override
+    public JmlForallClause asJmlForallClause() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlForallClause> toJmlForallClause() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlForallClause(Consumer<JmlForallClause> action) {
+        action.accept(this);
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlMultiExprClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlMultiExprClause.java
@@ -18,6 +18,8 @@
 import java.util.Optional;
 import static com.github.javaparser.utils.Utils.assertNotNull;
 
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (25.02.22)
@@ -192,4 +194,23 @@ public JmlMultiExprClause setExpression(final NodeList<Expression> expressions)
         setAsParentNodeOf(expressions);
         return this;
     }
+
+    @Override
+    public boolean isJmlMultiExprClause() {
+        return true;
+    }
+
+    @Override
+    public JmlMultiExprClause asJmlMultiExprClause() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlMultiExprClause> toJmlMultiExprClause() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlMultiExprClause(Consumer<JmlMultiExprClause> action) {
+        action.accept(this);
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlOldClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlOldClause.java
@@ -13,6 +13,9 @@
 import com.github.javaparser.metamodel.JmlOldClauseMetaModel;
 import static com.github.javaparser.utils.Utils.assertNotNull;
 
+import java.util.Optional;
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (12/12/21)
@@ -101,4 +104,23 @@ public JmlOldClauseMetaModel getMetaModel() {
     public JmlClauseKind getKind() {
         return JmlClauseKind.OLD;
     }
+
+    @Override
+    public boolean isJmlOldClause() {
+        return true;
+    }
+
+    @Override
+    public JmlOldClause asJmlOldClause() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlOldClause> toJmlOldClause() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlOldClause(Consumer<JmlOldClause> action) {
+        action.accept(this);
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlSignalsClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlSignalsClause.java
@@ -15,6 +15,9 @@
 import com.github.javaparser.metamodel.JmlSignalsClauseMetaModel;
 import static com.github.javaparser.utils.Utils.assertNotNull;
 
+import java.util.Optional;
+import java.util.function.Consumer;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/21/21)
@@ -133,4 +136,23 @@ public boolean replace(Node node, Node replacementNode) {
     public JmlSignalsClause clone() {
         return (JmlSignalsClause) accept(new CloneVisitor(), null);
     }
+
+    @Override
+    public boolean isJmlSignalsClause() {
+        return true;
+    }
+
+    @Override
+    public JmlSignalsClause asJmlSignalsClause() {
+        return this;
+    }
+
+    @Override
+    public Optional<JmlSignalsClause> toJmlSignalsClause() {
+        return Optional.of(this);
+    }
+
+    public void ifJmlSignalsClause(Consumer<JmlSignalsClause> action) {
+        action.accept(this);
+    }
 }