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

February 2022 release

ViperServer: commit b62f762
Silicon: commit cd20cf02b31ccd82a2cfdca7003947fd4380fe7b
Carbon: commit ef14316accc1add1effd3c2c2b1969f16891ba91
Silver: commit aeaebeaef7bf977c037e6390839aeb2f5c8b384b

22.02-RC

ViperServer: commit d2115c6
Silicon: commit cd20cf02b31ccd82a2cfdca7003947fd4380fe7b
Carbon: commit ef14316accc1add1effd3c2c2b1969f16891ba91
Silver: commit aeaebeaef7bf977c037e6390839aeb2f5c8b384b

v.21.07-release

ViperServer: commit 3e7d117
Silicon: commit 4dbb81fc9c3470ba9608eda5f08932962aee5479
Carbon: commit 4cdea1baeefbfd741ee2d0157e7c43337d84fe44
Silver: commit 3ea54220f1d2bc4adcc3151fa2080c198dbbd641

21.07-RC

ViperServer: commit dd1fe3f
Silicon: commit 8a017406684c5f5301c99a06873d0416388e89f2
Carbon: commit 4cdea1baeefbfd741ee2d0157e7c43337d84fe44
Silver: commit 44129b9d3870d2ca26c6f567405aa8abc51b9365

v.21.07-alpha2

ViperServer: commit a9ec059
Silicon: commit 3a31f3917f47b7734044d4ccfd1aa46b250dca34
Carbon: commit d6008c5da7d5b506c34d06b98b15811af77d9504
Silver: commit 47705f930fef963d58fb42ac9cd713d48af048d3

v.21.07-alpha1

First non-pre-release to test dependent projects against these artifacts.

ViperServer: commit 16cfc08
Silicon: commit 403055436199625955a1193d7482240aead252b5
Carbon: commit 2b9ac113e58b2091a818f8cae9cce2826d2a106d
Silver: commit 9aa917a808d00e2efc6d00c085b21a25d8dbe980