Deprecate 'new' and its semantics

[viper-admin]

Created by @alexanderjsummers on 2018-06-29 12:09 Last updated on 2019-03-02 22:27

We agreed at a recent Viper meeting to drop 'new' from the language, and possibly replace it with 'havoc'. I suggest that, in the meantime, we experiment with simply weakening the guarantees provided by 'new' to no-longer provide any freshness information. We could then judge how many tests fail, and whether there is a performance change. Migrating the tests to use e.g. a new 'havoc' feature would then be trivial, if we make that change to the Viper language.

[viper-admin]

@mschwerhoff commented on 2019-03-02 22:27

Directly related: https://github.com/viperproject/silicon/issues/29