search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

New reporter message for measure missing VC failing #1589

Closed samuelchassot closed 1 month ago

samuelchassot commented 1 month ago

the new message reports that the measure is missing instead of an empty counterexample. ex:

[Warning ]  - Result for 'measure missing' VC for leftPad @33:7:
[Warning ] false
[Warning ] LeftPad.scala:33:7:  => INVALID
             def leftPad[T](c: T, n: BigInt, s: List[T]): List[T] = {
                 ^
[Warning ] Measure is missing, cannot check termination