Skip to content
Snippets Groups Projects
Commit bcdc2381 authored by Nicolas Voirol's avatar Nicolas Voirol
Browse files

Terminating test with nested functions

parent 3414e4f4
No related branches found
No related tags found
No related merge requests found
...@@ -78,8 +78,10 @@ trait StructuralSize { ...@@ -78,8 +78,10 @@ trait StructuralSize {
}).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus) }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
case IntegerType => case IntegerType =>
FunctionInvocation(typedAbsBigIntFun, Seq(expr)) FunctionInvocation(typedAbsBigIntFun, Seq(expr))
/*
case Int32Type => case Int32Type =>
FunctionInvocation(typedAbsIntFun, Seq(expr)) FunctionInvocation(typedAbsIntFun, Seq(expr))
*/
case _ => InfiniteIntegerLiteral(0) case _ => InfiniteIntegerLiteral(0)
} }
} }
......
/* Copyright 2009-2016 EPFL, Lausanne */
object Nested16 {
def foo(i: BigInt): BigInt = {
def rec1(j: BigInt): BigInt = {
require(j >= 0)
def rec2(k: BigInt): BigInt = {
require(j > 0 || j == k)
if(k == 0) 0 else rec1(j-1)
}
rec2(j)
}
rec1(3)
} ensuring(0 == _)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment