Add ghost annotation to toList method of Set in library (#1601)

* Add ghost annotation to toList method of Set in library

* change a benchmark to use now ghost toList method

frontends/benchmarks/verification/valid/Iterables.scala

@@ -5,7 +5,7 @@ import stainless.annotation._
 import stainless.proof._
 
 object Iterables {
-
+  @ghost
   def test_setToList(set: Set[BigInt]) = {
     require(set.contains(1) && set.contains(2) && !set.contains(3))
 
@@ -17,7 +17,7 @@ object Iterables {
     set.toListPost(3)
     assert(!res.contains(3))
   }
-
+  @ghost
   def test_setMap(set: Set[BigInt]) = {
     require(set.contains(1) && set.contains(2) && !set.contains(3))
 
@@ -37,7 +37,7 @@ object Iterables {
   }
 
   val oneToSix = Set[BigInt](1,2,3,4,5,6)
-
+  @ghost
   def test_setFilter(set: Set[BigInt]) = {
     require((set & oneToSix) == oneToSix)
 
@@ -56,7 +56,7 @@ object Iterables {
     set.filterPost(p)(6)
     assert(!res.contains(6))
   }
-
+  @ghost
   def test_mapKeys(map: Map[Int, String]) = {
     require(map.contains(1) && map.contains(2) && !map.contains(3))
 
@@ -69,7 +69,7 @@ object Iterables {
     map.keysPost(3)
     assert(!res.contains(3))
   }
-
+  @ghost
   def test_mapValues(map: Map[Int, String]) = {
     require(map.get(1) == Some("foo") && map.get(2) == Some("bar"))
 
@@ -80,7 +80,7 @@ object Iterables {
     map.valuesPost1(2)
     assert(res.contains("bar"))
   }
-
+  @ghost
   def test_mapToList(map: Map[Int, String]) = {
     require(map.get(1) == Some("foo") && map.get(2) == Some("bar"))
 

frontends/library/stainless/lang/Set.scala

@@ -92,7 +92,7 @@ object Set {
       ()
    }.ensuring(_ => withFilter(p).contains(a) == (p(a) && set.contains(a)))
 
-    @library @extern @pure
+    @library @extern @pure @ghost
     def toList: List[A] = {
       List.fromScala(set.theSet.toList)
    }.ensuring(res => ListOps.noDuplicate(res) && res.content == set)