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

Line number missing for verification condition about cast correctness #210

Closed jad-hamza closed 6 years ago

jad-hamza commented 6 years ago 
object O {
  case class A() 

  abstract class C {
    val startPos: A = A()
  }
}
[  Info  ]   ┌──────────────────────┐
[  Info  ] ╔═╡ verification summary ╞═══════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └──────────────────────┘                                                                   ║
[  Info  ] ║ startPos       cast correctness           valid from cache              ?:?:?     0,001    ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 1    valid: 1    (1 from cache) invalid: 0    unknown: 0    time:   0,001           ║
[  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════╝
samarion commented 6 years ago

I can't reproduce with the latest Stainless, so I'll hope it's fixed and close it :)

jad-hamza commented 6 years ago

Oh that's odd, I still have the ?:?:?

samarion commented 6 years ago

I don't even see the "cast correctness" VC. Maybe it's because I'm running against a later version of Inox. Anyway there seem to be many places where positions are not copied in TypeEncoding so I'm covering the main cases.