Retire resource havocking hack

[viper-admin]

Created by @mschwerhoff on 2019-12-28 17:22

Voila (and potentially other frontends) regularly needs to havoc all resources of a specific kind, e.g. all instances of a predicate P. This can be achieved as follows:

label here
exhale forall x1: T1, x2: T2, ... :: acc(P(x1, x2, ...), perm(P(x1, x2, ...)))
inhale forall x1: T1, x2: T2, ... :: acc(P(x1, x2, ...), old[here]()perm(P(x1, x2, ...))))

The above approach is quite general and can be used to havoc, e.g. only specific instances of P. However, the case where all instances of P are to be havocked can be supported by Silicon in a much more efficient way (w.r.t. Silicon’s symbolic execution).

Until Viper is extended by a suitable havoc feature, Silicon supports a command-line option --enableHavocHack that instructs Silicon to havoc all instances of a resource R whenever a method call havoc_all_R() is encountered.