From 62b817d401f945c1a16201c337508afd043af372 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 31 Mar 2015 10:43:36 +0200
Subject: [PATCH] Just some FIXME cleanup
---
src/main/scala/leon/codegen/CodeGeneration.scala | 7 ++-----
.../scala/leon/frontends/scalac/CodeExtraction.scala | 7 ++-----
src/main/scala/leon/purescala/Definitions.scala | 10 +++++-----
src/main/scala/leon/purescala/ExprOps.scala | 4 ++--
src/main/scala/leon/repair/Repairman.scala | 4 ++--
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 9 ++++-----
6 files changed, 17 insertions(+), 24 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 023ef61ac..09f33654b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -167,7 +167,7 @@ trait CodeGeneration {
// An offset we introduce to the parameters:
// 1 if this is a method, so we need "this" in position 0 of the stack
- // 1 if we are monitoring // FIXME
+ // 1 if we are monitoring
val paramsOffset = Seq(!isStatic, params.requireMonitor).count(x => x)
val newMapping =
funDef.params.map(_.id).zipWithIndex.toMap.mapValues(_ + paramsOffset)
@@ -624,9 +624,6 @@ trait CodeGeneration {
ch << InvokeSpecial(afName, constructorName, consSig)
// Arithmetic
- /*
- * TODO: Correct code generation for infinite precision operations
- */
case Plus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
@@ -1204,7 +1201,7 @@ trait CodeGeneration {
val body = field.body.getOrElse(throw CompilationException("No body for field?"))
val jvmType = typeToJVM(field.returnType)
- mkExpr(body, ch)(NoLocals(isStatic)) // FIXME Locals?
+ mkExpr(body, ch)(NoLocals(isStatic))
if (isStatic){
ch << PutStatic(className, name, jvmType)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 1e1fa28bf..8d6c9cef9 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -888,18 +888,15 @@ trait CodeExtraction extends ASTExtractors {
s.symbol -> (() => Variable(vd.id))
}
-
val fctx = dctx.withNewVars(newVars)
-
- // If this is a lazy field definition, drop the assignment/ accessing TODO
+ // If this is a lazy field definition, drop the assignment/ accessing
val body =
if (funDef.defType == DefType.LazyFieldDef) { body0 match {
case Block(List(Assign(_, realBody)),_ ) => realBody
case _ => outOfSubsetError(body0, "Wrong form of lazy accessor")
}} else body0
-
-
+
val finalBody = try {
flattenBlocks(extractTree(body)(fctx)) match {
case e if e.getType.isInstanceOf[ArrayType] =>
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index ca74326fe..07769dbad 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -30,15 +30,15 @@ object Definitions {
override def copiedFrom(o : Tree) : this.type = {
super.copiedFrom(o)
o match {
- case df : Definition if df.owner.isDefined => this.setOwner(df.owner.get)
- case _ => this // FIXME should this ever happen?
+ case df : Definition if df.owner.isDefined =>
+ this.setOwner(df.owner.get)
+ case _ =>
+ this
}
}
- // TODO: this seems quite elegant, but make sure it works
def setSubDefOwners() = for (df <- subDefinitions) df.setOwner(this)
-
}
@@ -206,7 +206,7 @@ object Definitions {
def duplicate = copy(defs = defs map {
case f: FunDef => f.duplicate
case cd: ClassDef => cd.duplicate
- case other => other // FIXME: huh?
+ case other => other
})
setSubDefOwners()
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 893192822..32f2c2225 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -409,7 +409,7 @@ object ExprOps {
}).setPos(expr)
// rewrites pattern-matching expressions to use fresh variables for the binders
- // TODO: Unused, and untested
+ // ATTENTION: Unused, and untested
def freshenLocals(expr: Expr) : Expr = {
def rewritePattern(p: Pattern, sm: Map[Identifier,Identifier]) : Pattern = p match {
case InstanceOfPattern(Some(b), ctd) => InstanceOfPattern(Some(sm(b)), ctd)
@@ -2186,7 +2186,7 @@ object ExprOps {
} else {
TuplePattern(ob, subs)
}
- case LiteralPattern(ob, lit) => // TODO: is this correct?
+ case LiteralPattern(ob, lit) =>
if (ob == Some(anchor)) {
sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
pat
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index abcf13841..342cd0629 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -332,7 +332,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
// First is always true, focus on rest
focus(andJoin(exs), env)
case Some(false) =>
- // FIXME: Seems all test break when we evaluate to false, try true???
+ // Seems all test break when we evaluate to false, try true???
(choose, BooleanLiteral(true))
case None =>
// We cannot focus any further
@@ -350,7 +350,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
// First is always false, focus on rest
focus(orJoin(exs), env)
case Some(true) =>
- // FIXME: Seems all test break when we evaluate to true, try false???
+ // Seems all test break when we evaluate to true, try false???
(choose, BooleanLiteral(false))
case None =>
// We cannot focus any further
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 455a6fbdf..c0d799182 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -95,11 +95,10 @@ trait SMTLIBTarget {
def inlinedOptionGet(t : Term, tp: TypeTree): Term = {
FunctionApplication(SSymbol("ite"), Seq(
- FunctionApplication(someTester(tp), Seq(t)),
- FunctionApplication(someSelector(tp), Seq(t)),
- declareVariable(FreshIdentifier("error_value", tp))
- )
- )
+ FunctionApplication(someTester(tp), Seq(t)),
+ FunctionApplication(someSelector(tp), Seq(t)),
+ declareVariable(FreshIdentifier("error_value", tp))
+ ))
}
}
--
GitLab