Smoke Detector

[viper-admin]

Created by @mueller55 on 2016-11-22 14:15 Last updated on 2017-06-28 15:24

We should provide a smoke detector to make it easier to detect if an encoding is unsound. Ideally, this can be implemented as a Viper-to-Viper translation that adds "assert false" in various places and provides an appropriate error message. However, that might not be easily possible, because one needs to invert the logic of the verifier. So after evaluating this idea, we might have to create feature requests for Silicon and Carbon instead.

[viper-admin]

@dohrau commented on 2017-06-28 15:24

Currently, there is no check whether an inhaled permission is non-negative (e.g. the example below verifies). Of course, a smoke detector as mentioned above would catch this, but a consistency check could probably provide a more precise error message.

#!scala

field f: Ref
method foo(a: Ref)
{
    inhale acc(a.f, -1 / 2)
    a.f := null
}