From c74ec30d1ab0abd640df1f98cae62467a0bcb2c6 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 21 Sep 2022 10:50:06 +0200
Subject: [PATCH] exception when expression in recursive op case empty
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
de.prob.core/src/de/prob/eventb/translator/Theories.java | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
index 15d6ace4..453e0c83 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -377,8 +377,13 @@ public class Theories {
prologOutput.openTerm("case");
prologOutput.printAtom(indArg);
prologOutput.openList();
- for (FreeIdentifier fi : ex.getFreeIdentifiers()) {
- prologOutput.printAtom(fi.getName());
+ if(ex==null) {
+ throw new IllegalStateException("Empty expression for axiomatic recursive definition case " + es +
+ " and inductive argument " + indArg);
+ } else {
+ for (FreeIdentifier fi : ex.getFreeIdentifiers()) {
+ prologOutput.printAtom(fi.getName());
+ }
}
prologOutput.closeList();
printExpression(prologOutput, ex);
--
GitLab