Add measures in genc tailrec test cases, add empty statement after la…

…bel in C code

core/src/main/scala/stainless/genc/CPrinter.scala

@@ -244,7 +244,9 @@ class CPrinter(
       }
 
     case Labeled(name, block) =>
-      c"""|$name:
+      // In C, a label cannot be followed by a variable declaration
+      // So we add a semicolon to add an empty statement to work around this
+      c"""|$name: ;
           |    $block"""
 
     case Lit(lit) => c"$lit"

frontends/benchmarks/genc/valid/TailRecAliasedArgs.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecAliasedArgs {
   def aliased(n: Int, a: Int, b: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then a
     else aliased(n - 1, b, a + b)
 

frontends/benchmarks/genc/valid/TailRecComplexArgs.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecComplexArgs {
   def complexArgs(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n <= 0 then 1
     else complexArgs(n - 1 * 2 + 1) // Complex argument
 

frontends/benchmarks/genc/valid/TailRecCountDown.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecNoArguments {
   def countDown(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then 0
     else countDown(n - 1)
 

frontends/benchmarks/genc/valid/TailRecEarlyReturn.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecEarlyReturn {
   def earlyReturn(n: Int, acc: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then acc
     else if n == 3 then return acc * 2 // Early return
     else earlyReturn(n - 1, acc + 1)

frontends/benchmarks/genc/valid/TailRecFib.scala

@@ -5,6 +5,8 @@ import stainless.io._
 object TailRecFib {
 
   def fib(n: Int, i: Int = 0, j: Int = 1): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then i
     else fib(n-1, j, i+j)
 

frontends/benchmarks/genc/valid/TailRecFibAliased.scala

@@ -5,6 +5,8 @@ import stainless.io._
 object TailRecFibAliased {
 
   def fib(n: Int, i: Int = 0, j: Int = 1): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then i
     else
         val res = fib(n-1, j, i+j)

frontends/benchmarks/genc/valid/TailRecMultipleCalls.scala

@@ -4,7 +4,10 @@ import stainless.io._
 
 object TailRecMultipleCalls {
   def multipleCalls(n: Int, acc: Int): Int =
-    if n <= 0 then acc
+    require(n >= 0)
+    decreases(n)
+    if n == 0 then acc
+    else if n == 1 then acc + 2
     else if n % 2 == 0 then multipleCalls(n - 1, acc + 1)
     else multipleCalls(n - 2, acc + 2)
 

frontends/benchmarks/genc/valid/TailRecNested.scala

@@ -4,7 +4,10 @@ import stainless.io._
 
 object TailRecNested {
   def outer(n: Int): Int = 
+    require(n >= 0)
     def inner(x: Int): Int = 
+      require(x >= 0)
+      decreases(x)
       if x == 0 then 0
       else inner(x - 1)
     inner(n)

frontends/benchmarks/genc/valid/TailRecPatternMatching.check

@@ -1 +1 @@
-6
+5

frontends/benchmarks/genc/valid/TailRecPatternMatching.scala

@@ -3,14 +3,24 @@ import stainless.lang._
 import stainless.io._
 
 object TailRecPatternMatching {
-  def patternMatch(x: Option[Int], acc: Int): Int = x match
-    case None() => acc
-    case Some(0) => patternMatch(None(), acc + 1)
-    case Some(n) => patternMatch(Some(n - 1), acc + 1)
+  def patternMatch(x: Option[Int], acc: Int): Int = 
+    require(x match {
+      case None() => true
+      case Some(n) => n >= 1
+    })
+    val measure = x match {
+      case None() => 0
+      case Some(n) => n
+    }
+    decreases(measure)
+    x match
+      case None() => acc
+      case Some(n) if n == 1 => patternMatch(None(), acc + 1)
+      case Some(n) => patternMatch(Some(n - 1), acc + 1)
 
   @cCode.`export`
   def main(): Unit = {
     implicit val state = stainless.io.newState
-    StdOut.println(patternMatch(Some(5), 0)) // Expected: 6
+    StdOut.println(patternMatch(Some(5), 0)) // Expected: 5
   }
 }

frontends/benchmarks/genc/valid/TailRecStackOverflow.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecStackOverflow {
   def even(n: Int): Int =
+    require(n >= 0)
+    decreases(n)
     if n == 0 then 1
     else if n == 1 then 0
     else even(n - 2)

frontends/benchmarks/genc/valid/TailRecUnit.scala

@@ -4,6 +4,8 @@ import stainless.io._
 
 object TailRecUnit {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n == 0) return
     countDown(n - 1)
 

frontends/benchmarks/genc/valid/TailRecUnitIf.scala

@@ -2,8 +2,10 @@ import stainless.annotation._
 import stainless.lang._
 import stainless.io._
 
-object TailRecUnit {
+object TailRecUnitIf {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n == 0) return
     else countDown(n - 1)
 

frontends/benchmarks/genc/valid/TailRecUnitNoExplicitEnd.scala

@@ -2,8 +2,10 @@ import stainless.annotation._
 import stainless.lang._
 import stainless.io._
 
-object TailRecUnit {
+object TailRecUnitWithNoExplicitEnd {
   def countDown(n: Int): Unit =
+    require(n >= 0)
+    decreases(n)
     if (n > 0) countDown(n - 1)
 
   @cCode.`export`