search

epfl-lara / stainless

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

Fix positions for inlined functions #1477

Closed mario-bucev closed 9 months ago

mario-bucev commented 9 months ago

In some cases, VCs positions could be incorrect when using inline functions. This is particularly the case for synthetic copy methods which are always inlined. For instance, in the following snippet, the VC generated for mc.copy(x = y) would incorrectly point at the definition of MyClass. This PR fixes this issue and the correct position is now reported.

case class MyClass(x: BigInt, y: BigInt)

def buildClass(mc: MyClass, x: BigInt): MyClass = {
  mc.copy(x = y)
}.ensuring(_.x >= 0)
vkuncak commented 9 months ago

Are you saying that the position for a function f that is called from g and inlined will also be reported in g? Does this apply to user-defined functions as well?

mario-bucev commented 9 months ago

If I'm understanding correctly, yes, the inlined body of f will have its position set to the call site. Note that inlined bodies are annotated as @DropVCs (except for synthetic inlined functions since these are removed and as such cannot be checked independently).