Skip to content

Commit 44087c2

Browse files
committed
Treat duplicate predicate declarations as error.
1 parent a22b3d4 commit 44087c2

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,9 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) {
7878

7979
if (lookup(p.name()) == null) {
8080
functions().add(p);
81+
} else {
82+
// weigl: agreement on KaKeY meeting: this should be an error.
83+
semanticError(ctx, "Predicate '" + p.name() + "' is already defined!");
8184
}
8285
return null;
8386
}

0 commit comments

Comments
 (0)