Can ensure false as the post-condition of a function

[BenjaminFrei]

We are able to prove false in the function lenght below. This should not be possible.

adt List[T] {
  Nil()
  Cons(value : T, tail : List[T])
} 

function lenght(xs : List[Int]) : Int
  ensures lenght(xs) >= 0
  ensures xs.isNil ==> lenght(xs) == 0
  ensures (xs.isCons ==> lenght(xs) == lenght(xs.tail) + 2)
  ensures false
{
  (xs.isNil ? 0 : (1 + lenght(xs.tail)))
}

[marcoeilers]

Functions should not contain applications of themselves in their postcondition (since Viper's function encoding is unsound in that case, as you showed), but Viper currently does not check this (see issue #525).

For what it's worth, it's never necessary to use a function in its own postcondition, since unlike methods they are not treated modularly (i.e., the function definition is known by code that uses the function). You only need the first of your postconditions (since that describes an inductive property of the function), everything else follows directly from the definition.

[marcoeilers]

Forgot to add: Instead of writing lenght(xs) in the function postcondition, you should write result.