diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java index 3f871052c716d8aefb97d65eab1883b8ee379e22..57e89bf5da8b910e39c48ca3105b9313b7cfceb3 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 69d7ea1972ca4700d52b2e136cf7cdabaf2375ee..21ddc60bca560bdd8223a0e7f5e239fe0586d3ee 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);