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

Missing dependencies when using bigSubstring #1542

Open LioTree opened 1 month ago

LioTree commented 1 month ago
import stainless.lang.*

def test1(): String = {
    val a = "hello"
    a.bigSubstring(1, 3)
}

def test2(): String = {
    val a = "hello"
    a.bigSubstring(1)
}
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing the symbols...                             
[ Error  ] substring.scala:3:5: test1 depends on missing dependencies:
           def test1(): String = {
               ^
[ Error  ] Method bigSubstring
[ Error  ] substring.scala:5:5: 
               a.bigSubstring(1, 3)
               ^^^^^^^^^^^^^^^^^^^^
[ Error  ] 
[ Error  ] substring.scala:8:5: test2 depends on missing dependencies:
           def test2(): String = {
               ^
[ Error  ] Method bigSubstring
[ Error  ] substring.scala:10:5: 
               a.bigSubstring(1)
               ^^^^^^^^^^^^^^^^^
[ Fatal  ] Cannot recover from missing dependencies
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

In https://github.com/epfl-lara/stainless/blob/1fcab3f013c803956698b2b7e1ffa36be8c00648/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala#L1271 and https://github.com/epfl-lara/stainless/blob/1fcab3f013c803956698b2b7e1ffa36be8c00648/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala#L1282

ExSelected could not match the corresponding method call, which causes bigSubstring to be treated as a regular method call. ExSymbol should be used.

LioTree commented 1 month ago

fix: https://github.com/epfl-lara/stainless/pull/1543