From 35b2766c74b28b986410d843f8c03be40d1509ac Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 7 Nov 2013 17:37:37 +0100
Subject: [PATCH] Add evaluator tests checking that CodeGenParams work
---
.../test/evaluators/EvaluatorsTests.scala | 35 +++++++++++++++++++
1 file changed, 35 insertions(+)
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index c20a80028..eec8591db 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -434,4 +434,39 @@ class EvaluatorsTests extends LeonTestSuite {
checkEvaluatorError(e, mkCall("c", IL(42)))
}
}
+
+ test("Infinite Recursion") {
+ import codegen._
+
+ val p = """|object Program {
+ | import leon.Utils._
+ |
+ | def c(i : Int) : Int = c(i-1)
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val e = new CodeGenEvaluator(leonContext, prog, CodeGenParams(maxFunctionInvocations = 32))
+ checkEvaluatorError(e, mkCall("c", IL(42)))
+ }
+
+ test("Wrong Contracts") {
+ import codegen._
+
+ val p = """|object Program {
+ | import leon.Utils._
+ |
+ | def c(i : Int) : Int = {
+ | require(i > 0);
+ | c(i-1)
+ | }
+ |}
+ |""".stripMargin
+
+ implicit val prog = parseString(p)
+
+ val e = new CodeGenEvaluator(leonContext, prog, CodeGenParams(checkContracts = true))
+ checkError(e, mkCall("c", IL(-42)))
+ }
}
--
GitLab