Fix crash in Bloxorz example

[romac]

This file:

https://github.com/epfl-lara/bolts/blob/master/fp-design/bloxorz/Bloxorz.scala

crashes current stainless as far as I can test. Standard channel output:

http://lara.epfl.ch/~kuncak/crash.txt

error channel output:

Exception in thread "main" java.lang.NullPointerException
       at inox.Reporter.internalError(Reporter.scala:54)
       at inox.Reporter.internalError(Reporter.scala:100)
       at inox.Reporter.internalError(Reporter.scala:103)
       at stainless.MainHelpers.regularRunCycle$1(MainHelpers.scala:162)
       at stainless.MainHelpers.main(MainHelpers.scala:175)
       at stainless.MainHelpers.main$(MainHelpers.scala:122)
       at stainless.Main$.main(Main.scala:3)
       at stainless.Main.main(Main.scala)

Can you reproduce it? It also worked the same before the last few commits, so I think it's a longer-term issue.

— @vkuncak

[romac]

I can reproduce with latest version of Stainless via scalac, but extraction via dotty goes through, and the program verifies (modulo having to remove sealed on the StringParserTerrain trait which has no children, and thus a couple failing VCs). The benchmark should likely be refactored a bit for it to verify cleanly.

[vkuncak]

I was looking at bolts partly because I thought these would be a good set of tests for the sbt plugin; we could have each benchmark come with an sbt file. (I'd prefer if we did not have crazy deep directory structure for a single-file benchmark, though.)

[romac]

Agreed, that’s definitely something I would like to set up! Shouldn’t be too hard, now that the sbt plugin works again. I’ll look into it next week once I am done with a few more bug fixes.

On 27 Jun 2019, at 22:29, Viktor Kuncak notifications@github.com wrote:

I was looking at bolts partly because I thought these would be a good set of tests for the sbt plugin; we could have each benchmark come with an sbt file. (I'd prefer if we did not have crazy deep directory structure for a single-file benchmark, though.)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[Gorzen]

https://github.com/epfl-lara/bolts/pull/19 Fixes this issue, it isn't because of an infinite loop, but due to CodeExtraction's performance on recursive calls.

New issue: #695