From 97204e3bf13e05db46708d4fa522653a67ae8138 Mon Sep 17 00:00:00 2001 From: Lars Hupel <lars.hupel@mytum.de> Date: Tue, 11 Aug 2015 10:46:13 +0200 Subject: [PATCH] preserve class annotations in Leon's AST Follow-up to 3e4281d. Uses mutable state to imitate similar other properties of ClassDefs. --- src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 2 ++ src/main/scala/leon/purescala/Definitions.scala | 8 ++++++++ 2 files changed, 10 insertions(+) diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index cc2d8938e..a085755c1 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -511,12 +511,14 @@ trait CodeExtraction extends ASTExtractors { classesToClasses += sym -> acd parent.foreach(_.classDef.registerChild(acd)) + acd.setAnnotations(annotationsOf(sym)) acd } else { val ccd = CaseClassDef(id, tparams, parent, sym.isModuleClass).setPos(sym.pos) classesToClasses += sym -> ccd parent.foreach(_.classDef.registerChild(ccd)) + ccd.setAnnotations(annotationsOf(sym)) val fields = args.map { case (fsym, t) => val tpe = leonType(t.tpt.tpe)(defCtx, fsym.pos) diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala index cd1948c26..60d5da277 100644 --- a/src/main/scala/leon/purescala/Definitions.scala +++ b/src/main/scala/leon/purescala/Definitions.scala @@ -224,6 +224,14 @@ object Definitions { def methods = _methods + private var _annotations: Map[String, Seq[Option[Any]]] = Map.empty + + def setAnnotations(annotations: Map[String, Seq[Option[Any]]]) { + _annotations = annotations + } + + def annotations = _annotations + lazy val ancestors: Seq[ClassDef] = parent.toSeq flatMap { p => p.classDef +: p.classDef.ancestors } lazy val root = ancestors.lastOption.getOrElse(this) -- GitLab