Propagate ghost annotation from class to methods

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

Propagate ghost annotation from class to methods #1476

Closed mario-bucev closed 9 months ago

mario-bucev commented 9 months ago

PR #1472 changed the way propagation of annotation works, but I did not propagate @ghost annotation from @ghost class to methods. This PR fixes that. Note that @ghost does not propagate to fields (see here where we explicitly ignore owners).

vkuncak commented 9 months ago

What do you know, we have ghost classes? Presumably those are classes all of whose instances must be ghost?

mario-bucev commented 9 months ago

Yes it seems so. The nightly failed due to sbt scripted failing for this test (I forgot to test sbt scripted locally...). I've pushed an invalid example to "document" this as well.