July 2022 release

Release 2022.7

Date 29/07/22

Changes in Viper Language

• ADT plugin added. It is enabled by default, and can be disabled with the --disableAdtPlugin command-line option. This plugin converts ADT (abstract datatype) declarations of the form adt (name) { Constructor1(args) ... } into domain types with constructors, destructors, discriminants, and corresponding axioms. More information can be found in the tutorial (Silver#574)
• Added support for a refute (expression) statement. This statement behaves like an assertion, except the expression is expected to be provably false. More information can be found in the tutorial (Silver#583)
• Division of two Perm-typed expressions is now allowed. (Silver#572)
• Typed function application syntax ((foo(...) : T)) now parses properly. (Silver#584)

Backend-specific upgrades/changes

Symbolic Execution Verifier (Silicon)

• Output sent to the backend solver is now SMT-LIB 2.6 conformant. Additionally, there is experimental support for the CVC5 solver using the --prover cvc5 command-line option. (Silicon#609)
• Improved counterexamples. Counterexamples are now generated for domain types as well, and are included in the output with the --counterexample mapped command-line option. (Silicon#631)

Verification Condition Generation Verifier (Carbon)

• Breaking change: wildcard acc expressions in exhale statements are no longer reordered. Behaviour is now consistent with Silicon and all permissions in an exhale statement are always exhaled left to right. (Silicon#30, Carbon#411)

Miscellaneous

• "Chopper" API is now available to front ends. This functionality allows a single Viper file to be split into multiple smaller files that can be verified separately. Dependencies between functions, methods, and predicates are correctly determined to minimise the size of the individual Viper files. (Silver#589)
• Upgraded projects to use sbt version 1.6.2. (Silicon#627, Silver#592)
• Viper IDE uses .vpr as its default file extension. (viper-ide#223)
• Viper IDE now requires at least Java version 11. (viper-ide#250)
• Cache improvements. (Silver#578)
• Various bug fixes. (Carbon#423, Carbon#425, viper-ide#248, Silver#496, Silver#587, Silver#590)

ViperServer: commit 22fe7b8
Silicon: commit 098881005e53a0784ed1862bea4c07408b9b6e2d
Carbon: commit 4df61d8e37d8952d0eeb69d4bb797d5934e1d2f0
Silver: commit 918bafa770a88e1b488d9a93ad5eb250be41e983