From 2194883a3ac5594e70631ea8f23d7ce7ce1cb729 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Jan 2015 20:56:29 +0100
Subject: [PATCH] Change allowed "passes" arguments
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index f55c5d548..b98faa52f 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1009,8 +1009,13 @@ trait CodeExtraction extends ASTExtractors {
val rc = cases.map(extractMatchCase(_))
val UnwrapTuple(ines) = ine
- (oute +: ines) foreach {
- case Variable(_) => { }
+ ines foreach {
+ case v : Variable if currentFunDef.params.map{ _.toVariable } contains v =>
+ case LeonThis(_) =>
+ case other => ctx.reporter.fatalError(other.getPos, "Only i/o variables are allowed in i/o examples")
+ }
+ oute match {
+ case Variable(_) => // FIXME: this is not strict enough, we need the bound variable of enclosing Ensuring
case other => ctx.reporter.fatalError(other.getPos, "Only i/o variables are allowed in i/o examples")
}
passes(ine, oute, rc)
--
GitLab