From 60f7ac7c3cc1ad4810cf29f42b18b00ae5f79bec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 10 Feb 2016 13:58:50 +0100
Subject: [PATCH] Added a verification testcases for testing conversion.
---
.../strings/invalid/CompatibleListChar.scala | 29 +++++++++++++++++++
1 file changed, 29 insertions(+)
create mode 100644 testcases/verification/strings/invalid/CompatibleListChar.scala
diff --git a/testcases/verification/strings/invalid/CompatibleListChar.scala b/testcases/verification/strings/invalid/CompatibleListChar.scala
new file mode 100644
index 000000000..86eec34cd
--- /dev/null
+++ b/testcases/verification/strings/invalid/CompatibleListChar.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object CompatibleListChar {
+ def rec[T](l : List[T], f : T => String): String = l match {
+ case Cons(head, tail) => f(head) + rec(tail, f)
+ case Nil() => ""
+ }
+ def customToString[T](l : List[T], p: List[Char], d: String, fd: String => String, fp: List[Char] => String, pf: String => List[Char], f : T => String): String = rec(l, f) ensuring {
+ (res : String) => (p == Nil[Char]() || d == "" || fd(d) == "" || fp(p) == "" || pf(d) == Nil[Char]()) && ((l, res) passes {
+ case Cons(a, Nil()) => f(a)
+ })
+ }
+ def customPatternMatching(s: String): Boolean = {
+ s match {
+ case "" => true
+ case b => List(b) match {
+ case Cons("", Nil()) => true
+ case Cons(s, Nil()) => false // StrOps.length(s) < BigInt(2) // || (s == "\u0000") //+ "a"
+ case Cons(_, Cons(_, Nil())) => true
+ case _ => false
+ }
+ case _ => false
+ }
+ } holds
+}
\ No newline at end of file
--
GitLab