search

viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

NullPointerException for file-name-only paths #781

Closed HSMF closed 1 month ago

HSMF commented 2 months ago

When running gobra with the -i command line flag, an argument of just the file name (-i main.go) raises a java.lang.NullPointerException. This behavior differs from any path containing a / (e.g. -i ./main.go).

$ java -Xss1g -Xmx4g -jar $GOBRA -i main.go
11:00:57.563 [main] ERROR viper.gobra.GobraRunner$ - An unknown Exception was thrown.
11:00:57.564 [main] ERROR viper.gobra.GobraRunner$ - null
java.lang.NullPointerException: null
        at java.base/sun.nio.fs.UnixPath.toUnixPath(UnixPath.java:196)
        at java.base/sun.nio.fs.UnixPath.relativize(UnixPath.java:423)
        at java.base/sun.nio.fs.UnixPath.relativize(UnixPath.java:43)
        at viper.gobra.frontend.Source$.uniquePath(Source.scala:88)
        at viper.gobra.frontend.Source$.getPackageInfo(Source.scala:68)
        at viper.gobra.frontend.FileModeConfig.config$lzycompute(Config.scala:370)
        at viper.gobra.frontend.FileModeConfig.config(Config.scala:362)
        at viper.gobra.frontend.ScallopGobraConfig.config$lzycompute(Config.scala:946)
        at viper.gobra.frontend.ScallopGobraConfig.config(Config.scala:946)
        at viper.gobra.GobraRunner$.main(Gobra.scala:350)
        at viper.gobra.GobraRunner.main(Gobra.scala)