From 36390befc26a53a0dfdcf00ac2e5cf5a3fc4d6e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 17 Apr 2012 17:31:04 +0200
Subject: [PATCH] now only accepting instanceOf between compatible case class
---
.../scala/leon/plugin/CodeExtraction.scala | 18 +++++++++++++++++-
1 file changed, 17 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index d410278d9..5f3025c3b 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -607,7 +607,23 @@ trait CodeExtraction extends Extractors {
val ccRec = rec(cc)
val checkType = scalaType2PureScala(unit, silent)(tt.tpe)
checkType match {
- case CaseClassType(cd) => CaseClassInstanceOf(cd, ccRec)
+ case CaseClassType(ccd) => {
+ val rootType: ClassTypeDef = if(ccd.parent != None) ccd.parent.get else ccd
+ if(!ccRec.getType.isInstanceOf[ClassType]) {
+ unit.error(tr.pos, "isInstanceOf can only be used with a case class")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ val testedExprType = ccRec.getType.asInstanceOf[ClassType].classDef
+ val testedExprRootType: ClassTypeDef = if(testedExprType.parent != None) testedExprType.parent.get else testedExprType
+
+ if(rootType != testedExprRootType) {
+ unit.error(tr.pos, "isInstanceOf can only be used with compatible case classes")
+ throw ImpureCodeEncounteredException(tr)
+ } else {
+ CaseClassInstanceOf(ccd, ccRec)
+ }
+ }
+ }
case _ => {
unit.error(tr.pos, "isInstanceOf can only be used with a case class")
throw ImpureCodeEncounteredException(tr)
--
GitLab