JmlClauseIfClause and JmlCallableClause

jmltoolkit · May 2, 2024 · f2ef7f2 · f2ef7f2
1 parent ba3385f
commit f2ef7f2
Show file tree

Hide file tree

Showing 58 changed files with 1,050 additions and 200 deletions.
diff --git a/JmlMetaModel.plantuml b/JmlMetaModel.plantuml
@@ -148,10 +148,16 @@ enum JmlClauseKind {
     DIVERGES_REDUNDANTLY
     DURATION
     DURATION_REDUNDANTLY
+    WHEN
+    WHEN_REDUNDANTLY
     NONE
+
 }
 
-class JmlClauseIf extends JmlClause
+class JmlClauseIf extends JmlClause {
+	then : Java.Expression
+	cond : Java.Expression
+}
 class JmlMultiExprClause extends JmlClause {
         heaps : NodeList<SimpleName>
 }
@@ -174,12 +180,12 @@ class JmlOldClause extends JmlClause {
     declarations : Java.VariableDeclarationExpr
 }
 class JmlCallableClause extends JmlClause {
-
+	pre : Java.Expression
+	methodCalls : List<Java.MethodCallExpr>
 }
 class JmlForallClause extends JmlClause {
     boundedVariables : NodeList<Parameter>
 }
-class JmlCapturesClause extends JmlClause
 class JmlSignalsClause extends JmlClause {
 	parameter: Java.Parameter
 	expression: Java.Expression

diff --git a/javaparser-core-generators/pom.xml b/javaparser-core-generators/pom.xml
@@ -4,7 +4,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/javaparser-core-metamodel-generator/pom.xml b/javaparser-core-metamodel-generator/pom.xml
@@ -4,7 +4,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/...generator/src/main/java/com/github/javaparser/generator/metamodel/MetaModelGenerator.java b/...generator/src/main/java/com/github/javaparser/generator/metamodel/MetaModelGenerator.java
@@ -216,6 +216,8 @@ public class MetaModelGenerator extends AbstractGenerator {
         add(JmlForallClause.class);
         add(JmlOldClause.class);
         add(JmlCallableClause.class);
+        add(JmlClauseIf.class);
+        add(JmlMethodSignature.class);
         add(com.github.javaparser.ast.jml.clauses.JmlContract.class);
 
         //add(com.github.javaparser.ast.JmlBoundVariable.class);

diff --git a/javaparser-core-serialization/pom.xml b/javaparser-core-serialization/pom.xml
@@ -3,7 +3,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/javaparser-core-testing-bdd/pom.xml b/javaparser-core-testing-bdd/pom.xml
@@ -3,7 +3,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/javaparser-core-testing/pom.xml b/javaparser-core-testing/pom.xml
@@ -3,7 +3,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/javaparser-core/pom.xml b/javaparser-core/pom.xml
@@ -3,7 +3,7 @@
 	<parent>
 		<artifactId>jmlparser-parent</artifactId>
 		<groupId>io.github.jmltoolkit</groupId>
-		<version>3.25.10-SNAPSHOT</version>
+		<version>3.25.10-b2-SNAPSHOT</version>
 	</parent>
 	<modelVersion>4.0.0</modelVersion>
 

diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/body/CallableDeclaration.java b/javaparser-core/src/main/java/com/github/javaparser/ast/body/CallableDeclaration.java
@@ -214,12 +214,10 @@ public boolean remove(Node node) {
         if (node == null) {
             return false;
         }
-        if (contracts != null) {
-            for (int i = 0; i < contracts.size(); i++) {
-                if (contracts.get(i) == node) {
-                    contracts.remove(i);
-                    return true;
-                }
+        for (int i = 0; i < contracts.size(); i++) {
+            if (contracts.get(i) == node) {
+                contracts.remove(i);
+                return true;
             }
         }
         for (int i = 0; i < modifiers.size(); i++) {
@@ -355,12 +353,10 @@ public boolean replace(Node node, Node replacementNode) {
         if (node == null) {
             return false;
         }
-        if (contracts != null) {
-            for (int i = 0; i < contracts.size(); i++) {
-                if (contracts.get(i) == node) {
-                    contracts.set(i, (JmlContract) replacementNode);
-                    return true;
-                }
+        for (int i = 0; i < contracts.size(); i++) {
+            if (contracts.get(i) == node) {
+                contracts.set(i, (JmlContract) replacementNode);
+                return true;
             }
         }
         for (int i = 0; i < modifiers.size(); i++) {
@@ -456,6 +452,7 @@ public NodeList<JmlContract> getContracts() {
     @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
     @SuppressWarnings("unchecked")
     public T setContracts(final NodeList<JmlContract> contracts) {
+        assertNotNull(contracts);
         if (contracts == this.contracts) {
             return (T) this;
         }

diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/expr/LambdaExpr.java b/javaparser-core/src/main/java/com/github/javaparser/ast/expr/LambdaExpr.java
@@ -193,6 +193,12 @@ public boolean remove(Node node) {
         if (node == null) {
             return false;
         }
+        for (int i = 0; i < contracts.size(); i++) {
+            if (contracts.get(i) == node) {
+                contracts.remove(i);
+                return true;
+            }
+        }
         for (int i = 0; i < parameters.size(); i++) {
             if (parameters.get(i) == node) {
                 parameters.remove(i);
@@ -236,6 +242,12 @@ public boolean replace(Node node, Node replacementNode) {
             setBody((Statement) replacementNode);
             return true;
         }
+        for (int i = 0; i < contracts.size(); i++) {
+            if (contracts.get(i) == node) {
+                contracts.set(i, (JmlContract) replacementNode);
+                return true;
+            }
+        }
         for (int i = 0; i < parameters.size(); i++) {
             if (parameters.get(i) == node) {
                 parameters.set(i, (Parameter) replacementNode);
@@ -284,14 +296,22 @@ public boolean isExplicitlyTyped() {
         return getParameters().stream().allMatch(p -> !(p.getType().isUnknownType()));
     }
 
-    @Override
+    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
     public NodeList<JmlContract> getContracts() {
         return contracts;
     }
 
-    @Override
-    public LambdaExpr setContracts(NodeList<JmlContract> contracts) {
+    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
+    public LambdaExpr setContracts(final NodeList<JmlContract> contracts) {
+        assertNotNull(contracts);
+        if (contracts == this.contracts) {
+            return this;
+        }
+        notifyPropertyChange(ObservableProperty.CONTRACTS, this.contracts, contracts);
+        if (this.contracts != null)
+            this.contracts.setParentNode(null);
         this.contracts = contracts;
+        setAsParentNodeOf(contracts);
         return this;
     }
 }
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
@@ -3,25 +3,32 @@
 import com.github.javaparser.TokenRange;
 import com.github.javaparser.ast.AllFieldsConstructor;
 import com.github.javaparser.ast.Generated;
+import com.github.javaparser.ast.NodeList;
+import com.github.javaparser.ast.expr.SimpleName;
 import com.github.javaparser.ast.visitor.CloneVisitor;
 import com.github.javaparser.ast.visitor.GenericVisitor;
 import com.github.javaparser.ast.visitor.VoidVisitor;
 import com.github.javaparser.metamodel.JavaParserMetaModel;
 import com.github.javaparser.metamodel.JmlCallableClauseMetaModel;
 import com.github.javaparser.ast.Node;
-
 import java.util.Optional;
 import java.util.function.Consumer;
 
+import com.github.javaparser.ast.observer.ObservableProperty;
+
+import static com.github.javaparser.utils.Utils.assertNotNull;
+
 /**
  * @author Alexander Weigl
  * @version 1 (2/22/21)
  */
 public class JmlCallableClause extends JmlClause {
 
+    private NodeList<JmlMethodSignature> methodSignatures = new NodeList<JmlMethodSignature>();
+
     @AllFieldsConstructor
-    public JmlCallableClause() {
-        this(null);
+    public JmlCallableClause(SimpleName name, NodeList<JmlMethodSignature> methodSignatures) {
+        super(name);
     }
 
     /**
@@ -63,21 +70,85 @@ public JmlClauseKind getKind() {
     }
 
     @Override
+    @Generated("com.github.javaparser.generator.core.node.TypeCastingGenerator")
     public boolean isJmlCallableClause() {
         return true;
     }
 
     @Override
+    @Generated("com.github.javaparser.generator.core.node.TypeCastingGenerator")
     public JmlCallableClause asJmlCallableClause() {
         return this;
     }
 
     @Override
+    @Generated("com.github.javaparser.generator.core.node.TypeCastingGenerator")
     public Optional<JmlCallableClause> toJmlCallableClause() {
         return Optional.of(this);
     }
 
+    @Override
+    @Generated("com.github.javaparser.generator.core.node.TypeCastingGenerator")
     public void ifJmlCallableClause(Consumer<JmlCallableClause> action) {
         action.accept(this);
     }
+
+    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
+    public NodeList<JmlMethodSignature> getMethodSignatures() {
+        return methodSignatures;
+    }
+
+    @Generated("com.github.javaparser.generator.core.node.PropertyGenerator")
+    public JmlCallableClause setMethodSignatures(final NodeList<JmlMethodSignature> methodSignatures) {
+        assertNotNull(methodSignatures);
+        if (methodSignatures == this.methodSignatures) {
+            return this;
+        }
+        notifyPropertyChange(ObservableProperty.METHOD_SIGNATURES, this.methodSignatures, methodSignatures);
+        if (this.methodSignatures != null)
+            this.methodSignatures.setParentNode(null);
+        this.methodSignatures = methodSignatures;
+        setAsParentNodeOf(methodSignatures);
+        return this;
+    }
+
+    @Override
+    @Generated("com.github.javaparser.generator.core.node.RemoveMethodGenerator")
+    public boolean remove(Node node) {
+        if (node == null) {
+            return false;
+        }
+        for (int i = 0; i < methodSignatures.size(); i++) {
+            if (methodSignatures.get(i) == node) {
+                methodSignatures.remove(i);
+                return true;
+            }
+        }
+        return super.remove(node);
+    }
+
+    @Override
+    @Generated("com.github.javaparser.generator.core.node.ReplaceMethodGenerator")
+    public boolean replace(Node node, Node replacementNode) {
+        if (node == null) {
+            return false;
+        }
+        for (int i = 0; i < methodSignatures.size(); i++) {
+            if (methodSignatures.get(i) == node) {
+                methodSignatures.set(i, (JmlMethodSignature) replacementNode);
+                return true;
+            }
+        }
+        return super.replace(node, replacementNode);
+    }
+
+    /**
+     * This constructor is used by the parser and is considered private.
+     */
+    @Generated("com.github.javaparser.generator.core.node.MainConstructorGenerator")
+    public JmlCallableClause(TokenRange tokenRange, SimpleName name, NodeList<JmlMethodSignature> methodSignatures) {
+        super(tokenRange, name);
+        setMethodSignatures(methodSignatures);
+        customInitialization();
+    }
 }
diff --git a/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlCapturesClause.java b/javaparser-core/src/main/java/com/github/javaparser/ast/jml/clauses/JmlCapturesClause.java
@@ -12,6 +12,8 @@
  * @author Alexander Weigl
  * @version 1 (2/22/21)
  */
+// in favour of JmlMultiExprClause
+@Deprecated()
 public class JmlCapturesClause extends JmlClause {
 
     @AllFieldsConstructor