Update benchmarks

Author: drganam

core/src/main/scala/stainless/extraction/trace/Trace.scala

@@ -96,17 +96,21 @@ trait Trace extends CachingPhase with IdentityFunctions with IdentitySorts { sel
       var funInv: Option[s.FunctionInvocation] = None
       fd.flags.filter(elem => elem.name == "traceInduct").head match {
         case s.Annotation("traceInduct", fun) => {
-          s.exprOps.preTraversal {
-            case _ if funInv.isDefined => // do nothing
-            case fi @ s.FunctionInvocation(tfd, _, args) if symbols.isRecursive(tfd) && (fun.contains(StringLiteral(tfd.name)) || fun.contains(StringLiteral("")))
-            => {
-                  val paramVars = fd.params.map(_.toVariable)
-                  val argCheck = args.forall(paramVars.contains) && args.toSet.size == args.size
-                  if (argCheck) 
-                    funInv = Some(fi)
-                }
+          BodyWithSpecs(fd.fullBody).getSpec(PostconditionKind) match {
+            case Some(Postcondition(post)) => 
+              s.exprOps.preTraversal {
+                case _ if funInv.isDefined => // do nothing
+                case fi @ s.FunctionInvocation(tfd, _, args) if symbols.isRecursive(tfd) && (fun.contains(StringLiteral(tfd.name)) || fun.contains(StringLiteral("")))
+                => {
+                      val paramVars = fd.params.map(_.toVariable)
+                      val argCheck = args.forall(paramVars.contains) && args.toSet.size == args.size
+                      if (argCheck) 
+                        funInv = Some(fi)
+                    }
+                case _ => 
+              }(post)
             case _ => 
-          }(fd.fullBody)
+          }
         }
       }
 
@@ -161,17 +165,11 @@ trait Trace extends CachingPhase with IdentityFunctions with IdentitySorts { sel
     val returnType = model.returnType
     val flags = Seq(s.Derived(lemma.id), s.Derived(model.id))
 
-    val fi = FunctionInvocation(model.id, newParamTps, newParamVars)
-
-    /*val body = FunctionInvocation(
-      ast.SymbolIdentifier("stainless.lang.specialize"),
-      fi.tps,
-      Seq(fi)
-    )*/
-
     val body = FunctionInvocation(model.id, newParamTps, newParamVars)
     val indPattern = new s.FunDef(id, newParamTypes, newParams, returnType, body, flags)
 
+    val fi = FunctionInvocation(model.id, newParamTps, newParamVars)
+
     class Specializer(
       origFd: FunDef,
       newId: Identifier,

core/src/main/scala/stainless/frontend/BatchedCallBack.scala

@@ -109,8 +109,8 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
       }
       report = Report(reports)
       rerunPipeline = Trace.nextIteration(report)
-      if (rerunPipeline) report.emit(context)
-      else Trace.printEverything
+      if (!rerunPipeline) Trace.printEverything
+      //else report.emit(context)
     }
   }
 

frontends/benchmarks/verification/valid/Count.scala

@@ -17,7 +17,7 @@ object Count {
   }//ensuring(res => res == count1(p, l))
 
   @traceInduct("")
-  def count_check(p: BigInt => Boolean, l: List[BigInt]): Boolean = {
-    count1(p, l) == count2(p, l)
-  }.holds
-}
+  def count_check(p: BigInt => Boolean, l: List[BigInt]): Unit = {
+    ()
+  } ensuring (res => count1(p, l) == count2(p, l))
+}

frontends/benchmarks/verification/valid/Filter.scala

@@ -7,7 +7,7 @@ object Filter {
 
   def filter1(p: BigInt => Boolean, l: List[BigInt], n: BigInt): List[BigInt] = { 
     require(l.size <= n)
-    if(l.isEmpty) Nil()
+    if (l.isEmpty) List()
     else if(p(l.head)) l.head::filter1(p, l.tail, n)
     else filter1(p, l.tail, n)
   }
@@ -18,8 +18,9 @@ object Filter {
   }
 
   @traceInduct("")
-  def filter_check(p: BigInt => Boolean, l: List[BigInt], n: BigInt): Boolean = {
+  def filter_check(p: BigInt => Boolean, l: List[BigInt], n: BigInt): Unit = {
     require(l.size <= n)
-    filter1(p, l, n) == filter2(p, l, n)
-  }.holds
-}
+    ()
+  } ensuring(filter1(p, l, n) == filter2(p, l, n))
+  
+}

frontends/benchmarks/verification/valid/Insert.scala

@@ -13,8 +13,8 @@ object Monotonicity {
   }
 
   @traceInduct("")
-  def monotonicity(l: List[BigInt], set1: Set[BigInt], set2: Set[BigInt]): Boolean = {
-    (contains(l, set1, set2) && set1.subsetOf(set2)) ==> contains(l, set2, set1)
-  }.holds
+  def monotonicity(l: List[BigInt], set1: Set[BigInt], set2: Set[BigInt]): Unit = {
+    ()
+  } ensuring((contains(l, set1, set2) && set1.subsetOf(set2)) ==> contains(l, set2, set1))
 }
 

frontends/benchmarks/verification/valid/Monotonicity.scala

@@ -20,8 +20,8 @@ object Reverse {
   }
 
   @traceInduct("reverse0")
-  def revPreservesContent(l1: IList, l2: IList): Boolean = {
-    content(l1) ++ content(l2) == content(reverse0(l1, l2))
-  }.holds
+  def revPreservesContent(l1: IList, l2: IList): Unit = {
+    ()
+  } ensuring (content(l1) ++ content(l2) == content(reverse0(l1, l2)))
 }
 

frontends/benchmarks/verification/valid/Reverse.scala

@@ -13,8 +13,8 @@ object Size {
   }) //ensuring(res => res >= 0)
 
   @traceInduct("")
-  def nonNegSize(l: IList): Boolean = {
-    size(l) >= 0
-  }.holds
+  def nonNegSize(l: IList): Unit = {
+    ()
+  } ensuring (size(l) >= 0)
 }
 

frontends/benchmarks/verification/valid/Size.scala

@@ -22,8 +22,8 @@ object Sorted {
   }//ensuring(res => res == sorted1(l))
 
   @traceInduct("")
-  def sorted_check(l: List[BigInt]): Boolean = {
-    sorted1(l) == sorted2(l)
-  }.holds
+  def sorted_check(l: List[BigInt]): Unit = {
+    ()
+  } ensuring (sorted1(l) == sorted2(l))
 
 }

frontends/benchmarks/verification/valid/Sorted.scala

@@ -14,8 +14,8 @@ object Zero {
   }//ensuring(res => res == zero1(arg))
 
   @traceInduct("")
-  def zero_check(arg: BigInt): Boolean = {
-    zero1(arg) == zero2(arg)
-  }.holds
+  def zero_check(arg: BigInt): Unit = {
+    ()
+  } ensuring (zero1(arg) == zero2(arg))
 
 }