From 33f404202f3e5d14cb59209ac0b4071bfb5fc8a8 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 11 Oct 2024 11:02:21 +0200
Subject: [PATCH] Detect only AOperationCallSubstitution with return values as
unsupported
---
src/main/java/de/tlc4b/analysis/MachineContext.java | 4 ++++
.../java/de/tlc4b/analysis/UnsupportedConstructsFinder.java | 1 -
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 3f87105..57e89bf 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -11,6 +11,7 @@ import de.tlc4b.MP;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.transformation.DefinitionsSorter;
import de.tlc4b.analysis.transformation.MachineClauseSorter;
+import de.tlc4b.exceptions.NotSupportedException;
import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
@@ -652,6 +653,9 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAOperationCallSubstitution(AOperationCallSubstitution node) {
+ if (!node.getResultIdentifiers().isEmpty()) {
+ throw new NotSupportedException("Operation calls with return values are not supported.");
+ }
String name = Utils.getTIdentifierListAsString(node.getOperation());
Node o = operations.get(name);
if (o != null) {
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index 69d7ea1..21ddc60 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -25,7 +25,6 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
add(AWhileSubstitution.class);
add(AVarSubstitution.class);
add(ACaseSubstitution.class);
- add(AOperationCallSubstitution.class);
add(AImplementationMachineParseUnit.class);
--
GitLab