From 7e348b6052432d823cbc5db7083dc4e0c3608b74 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Dec 2007 10:58:21 +0000 Subject: [PATCH] Redefining built-in labels is an error. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@550 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/LabelList.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/LabelList.java b/prism/src/parser/LabelList.java index 24565af4..f4f8caa8 100644 --- a/prism/src/parser/LabelList.java +++ b/prism/src/parser/LabelList.java @@ -141,13 +141,18 @@ public class LabelList public void check() throws PrismException { int i, n; + String s; Expression e; // go thru all labels n = labels.size(); for (i = 0; i < n; i++) { - e = getLabel(i); + // make sure name doesn't clash with a built-in one + s = getLabelName(i); + if ("deadlock".equals(s)) throw new PrismException("Cannot define a label called \"deadlock\" - this is a built-in label"); + if ("init".equals(s)) throw new PrismException("Cannot define a label called \"init\" - this is a built-in label"); // is expression ok? + e = getLabel(i); e.check(); // and does it type check ok? if (e.getType() != Expression.BOOLEAN) {