From a78664f17864b300fe0d1cb63b42ec80be58363f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 17:02:22 +0000 Subject: [PATCH] TypeCheck: refine type checking to better cope with TypeVoid results Only filter(state, ...) has special handling for TypeVoid results (special results such as e.g. pareto results from multi-objective model checking). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12034 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/visitor/TypeCheck.java | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 187ee59e..65a114ba 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -624,6 +624,11 @@ public class TypeCheck extends ASTTraverse throw new PrismLangException("Type error: Boolean argument not allowed as operand for filter of type \"" + e.getOperatorName() + "\"", e.getOperand()); } + if (t instanceof TypeVoid) { + // e.g., complex results from multi-objective checking + throw new PrismLangException("Type error: Void/complex arguments not allowed as operand for filter of type \"" + e.getOperatorName() + "\"", + e.getOperand()); + } break; case COUNT: case FORALL: @@ -635,8 +640,13 @@ public class TypeCheck extends ASTTraverse case FIRST: case PRINT: case PRINTALL: + if (t instanceof TypeVoid) { + throw new PrismLangException("Type error: Void/complex arguments not allowed as operand for filter of type \"" + e.getOperatorName() + "\"", + e.getOperand()); + } + break; case STATE: - // Anything goes + // Anything goes, has special handling for TypeVoid (e.g., some multi-objective results) break; default: throw new PrismLangException("Cannot type check filter of unknown type", e);