Releases | Open Source Science

The semantics of permission amounts in functions has changed. When checking function preconditions, concrete permission amounts are ignored; instead, we only distinguish between zero and any positive amounts. Thus, the following assertions all have the same meaning in a function precondition: acc(x.f, write) or acc(x.f, wildcard) or acc(x.f, 1/2) or acc(x.f, b ? write : 1/2) or acc(x.f) && acc(x.f) or acc(x.f, 2/1) all just require checking that a caller has some positive permission amount to x.f. The same is true for predicate permissions. As a result, inside a function, one can no longer assume non-aliasing based on permission amounts. Additionally, when verifying well-definedness of a function, again all permission amounts are ignored (with the exception of distinguishing between zero and something positive as stated before), so one can for example unfold a whole predicate inside a function whose precondition only asks for half that predicate. Programs may still use concrete permission amounts in functions to preserve backward-compatibility, but such amounts will be meaningless and will result in a warning. The old permission semantics is still available and can be enabled using the new command line flag --respectFunctionPrePermAmounts. https://github.com/viperproject/silicon/pull/877
Added a new expression asserting (a) in e, which checks that a holds and subsequently evaluates to e. https://github.com/viperproject/silver/pull/814

API Changes

The permission amount in the AST nodes for field and predicate access predicates is now optional. If no permission amount is given, the amount defaults to wildcard in functions and write anywhere else.

Bug Fixes

Several bugfixes in trigger inference https://github.com/viperproject/silver/pull/827
Pretty printing:
- Termination measures are no longer pretty-printed as requires decreases, which was invalid Viper code https://github.com/viperproject/silver/pull/831
- Fixed pretty-printing conditional termination measures https://github.com/viperproject/silver/pull/847
- Unambiguous pretty-printing of integer division https://github.com/viperproject/silver/pull/818
Fixed crash in termination check for inhale-exhale-expressions https://github.com/viperproject/silver/pull/822
Fixed missing position information in predicate termination measures https://github.com/viperproject/silver/pull/836
Fixed case where program with annotations was incorrectly rejected by the parser https://github.com/viperproject/silver/pull/842

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

Soundness fixes:
- Fixed an unsoundness in package blocks that have no feasible paths https://github.com/viperproject/silicon/pull/899
- Fixed unsound definitions of snapshots inside quantifiers with exhaleMode 1 / moreCompleteExhale https://github.com/viperproject/silicon/pull/898
- Fixed unsound constraints for wildcard variables in function axioms with exhaleMode 1 / moreCompleteExhale https://github.com/viperproject/silicon/pull/895
- Fixed case where wildcard amount could be unsoundly constrained against itself https://github.com/viperproject/silicon/pull/893
- Fixed unsound snapshot definitions in function axioms resulting from state consolidation https://github.com/viperproject/silicon/pull/904
Performance improvements:
- Avoiding generating snapshot definitions that will not be used, reducing potential quantifier instantiations https://github.com/viperproject/silicon/pull/879
- State consolidation now also merged quantified chunks https://github.com/viperproject/silicon/pull/860
- Fixed potential matching loop in sequence axiomatization https://github.com/viperproject/silicon/pull/885
- Simplified and improved copying of macros and function declarations between solvers for parallel branch verification https://github.com/viperproject/silicon/pull/872
Debugger improvements:
- More informative names for debug labels, showing value expressions for non-quantified chunks https://github.com/viperproject/silicon/pull/884
- Improved pretty-printing of quantified chunks in debugger https://github.com/viperproject/silicon/pull/865
- Added option to print internal term representation instead of Viper-level expressions https://github.com/viperproject/silicon/pull/884
- Added missing old-labels around heap-dependent function applications https://github.com/viperproject/silicon/pull/900
- Fixed race condition in assumption ID generation https://github.com/viperproject/silicon/pull/887
Bug fixes:
- Fixed a rare crash related to wand packaging https://github.com/viperproject/silicon/pull/876

Verification Condition Generation Backend (Carbon)

Soundness fixes:
- Fixed incorrect injectivity check for quantified permissions with multiple quantified variables https://github.com/viperproject/carbon/pull/542
Completeness improvements:
- Improved framing of heap locations protected by predicates that have not been unfolded https://github.com/viperproject/carbon/pull/543
- Fixed incompleteness where condition of empty if-block could not trigger quantifiers https://github.com/viperproject/carbon/pull/544
Performance improvements:
- Fixed potential matching loop in sequence axiomatization https://github.com/viperproject/carbon/pull/536
- Improved framing axioms for quantified permissions https://github.com/viperproject/carbon/pull/524
Bug fixes:
- Fixed Boogie crash when using quantified predicates without parameters https://github.com/viperproject/carbon/pull/541

Based on - ViperServer release v.25.02-release - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-03-06-0931

Based on - ViperServer release 25.02-RC - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-03-04-1324

Based on - ViperServer release 25.02-RC - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-03-04-1317

Based on - ViperServer release 25.02-RC - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-03-04-1258

Based on - ViperServer release 25.02-RC - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-03-04-1242

Based on - ViperServer release 25.02-RC - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-02-28-1146

Based on - ViperServer release v-2025-02-03-0712 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] 12 months ago

viper-ide - Nightly Release v-2025-02-04-1042

Based on - ViperServer release v-2025-02-02-0718 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] about 1 year ago

viper-ide - Nightly Release v-2025-02-03-1055

Based on - ViperServer release v-2025-02-02-0718 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] about 1 year ago

viper-ide - Nightly Release v-2025-02-03-1039

Based on - ViperServer release v-2025-02-02-0718 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] about 1 year ago

viper-ide - Nightly Release v-2025-01-20-2148

Based on - ViperServer release v-2024-10-17-0712 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] about 1 year ago

viper-ide - Nightly Release v-2024-11-15-0837

Based on - ViperServer release v-2024-10-17-0712 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] over 1 year ago

viper-ide - Nightly Release v-2024-11-14-1701

Based on - ViperServer release v-2024-10-17-0712 - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] over 1 year ago

viper-ide - v4.4.2 (August 2024 release)

Release 2024.8

Date 31/08/24

Changes in Viper Language

Domain axioms can now refer to functions that have decreases clauses (but no preconditions) https://github.com/viperproject/silver/pull/802

API Changes and Internal Improvements

Improved Simplifier simplifies many additional expressions; new option determines whether simplification must preserve well-definedness https://github.com/viperproject/silver/pull/810
Chopper is now aware of opaque functions https://github.com/viperproject/silver/pull/779
Chopper has improved dependency analysis for axioms https://github.com/viperproject/silver/pull/776
Removed filtering of duplicate errors inside Viper (this is now left to frontends) https://github.com/viperproject/silver/pull/778

Bug Fixes

Fixed various issues with macro expansion:
- Fixed incorrect variable renaming during macro expansion https://github.com/viperproject/silver/pull/804
- Disallowing nested macro declarations https://github.com/viperproject/silver/pull/795
- Fixed incorrect renaming of label statements during macro expansion https://github.com/viperproject/silver/pull/793
Fixed incorrect Simplifier handling of division and modulo expressions https://github.com/viperproject/silver/pull/794
Fixed crash in proof obligation computation for expressions https://github.com/viperproject/silver/pull/783
Termination plugin: Improved encoding of checks for unfolding-expressions https://github.com/viperproject/silver/pull/773
ADT plugin: Fixed crash when plugin is used with other AST extensions https://github.com/viperproject/silver/pull/800

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

Added experimental support for (command line) verification debugging. With the new option --enableDebugging, users can see the state (store, heap, branch conditions and assumptions) in a format that that can be understood on the Viper level (avoiding internal Silicon concepts) at the point where a verification error occurs, locally assert or assume expressions to debug the error, and change SMT solver options. https://github.com/viperproject/silicon/pull/863
Soundness fixes:
- Fixed unsound rewrite for --conditionalizePermissions option https://github.com/viperproject/silicon/pull/853
- Fixed unsound handling of quantified permissions with unsatisfiable condition https://github.com/viperproject/silicon/pull/843
- Fixed unsound handling of quantified permissions with trivial condition https://github.com/viperproject/silicon/pull/834
- Improved encoding of magic wand snapshots that prevents unsoundness for applying-expressions https://github.com/viperproject/silicon/pull/836
- Fixed incorrect order of function precondition assumptions https://github.com/viperproject/silicon/pull/811
Completeness improvements:
- Recording missing constraints during function verification https://github.com/viperproject/silicon/pull/852 and https://github.com/viperproject/silicon/pull/825
- Fixed treatment of snapshot maps defined while evaluating quantifiers https://github.com/viperproject/silicon/pull/840
- Avoiding using a quantifier for wildcard constraints for quantified resources when possible https://github.com/viperproject/silicon/pull/817
Performance improvements:
- Improved snapshot map caching for quantified permissions (also improves completeness) https://github.com/viperproject/silicon/pull/846
- Avoiding creating new snapshot maps for quantified resources when unnecessary https://github.com/viperproject/silicon/pull/839
- Eagerly assuming non-aliasing for quantified field chunks https://github.com/viperproject/silicon/pull/835
- More efficient function axiomatization for functions with many branches https://github.com/viperproject/silicon/pull/808
- Flexible path joining options:
- With command line argument --moreJoins=1, Silicon joins only branches stemming from impure implications (immediately after branching). With --moreJoins=2 it joins all branches, including branches stemming from program control flow, at the earliest possible point. https://github.com/viperproject/silicon/pull/823
- The new annotation @moreJoins(n), with n bein 1 or 2 as just described, can be used to enable path joining on a per-method level https://github.com/viperproject/silicon/pull/823
- More flexible state consolidation:
- Added several new options for state consolidation behavior https://github.com/viperproject/silicon/pull/827
- The new annotation @stateConsolidationMode(n) allows configuring state consolidation on a per-method level https://github.com/viperproject/silicon/pull/827
Other improvements:
- Fixed crash resulting from double-declarations of macros with --parallelizeBranches https://github.com/viperproject/silicon/pull/813
- Fixed error reporting for method call arguments https://github.com/viperproject/silicon/pull/841
- Silicon now tries to find the Z3 executable in PATH if no path is explicitly provided https://github.com/viperproject/silicon/pull/818

Verification Condition Generation Backend (Carbon)

Bug fixes:
- Preventing Boogie crash when using annotations https://github.com/viperproject/carbon/pull/505

Based on - ViperServer release v.24.08-release - Z3 4.8.7 - Boogie release 7449a7a899c02c95

- TypeScript
Published by github-actions[bot] over 1 year ago

viper-ide - Nightly Release v-2024-03-29-0722

Based on - ViperServer release v-2024-03-29-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-27-0722

Based on - ViperServer release v-2024-03-27-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-26-0721

Based on - ViperServer release v-2024-03-26-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-24-0722

Based on - ViperServer release v-2024-03-24-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-23-0722

Based on - ViperServer release v-2024-03-23-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-18-0722

Based on - ViperServer release v-2024-03-18-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-17-0721

Based on - ViperServer release v-2024-03-17-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-15-0723

Based on - ViperServer release v-2024-03-15-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-10-0722

Based on - ViperServer release v-2024-03-10-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-03-01-0723

Based on - ViperServer release v-2024-03-01-0714 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 2 years ago

viper-ide - Nightly Release v-2024-02-20-0722

Based on - ViperServer release v-2024-02-20-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - v4.3.1 (January 2024 release)

Release 2024.1

Date 19/02/24

Changes in Viper Language

unfold, fold, and unfolding now require a strictly positive permission amount (i.e., none is no longer allowed) (Silicon#754) and (Carbon#469). This fixes an unsoundness (Silver#444). A new error reason NonPositivePermission is reported if this condition is not satisfied (Silver#744).
When generic functions are used inside axioms of their own domain and the type arguments are not constrained, Viper no longer uses Int as the type argument, but instead uses the domain's type parameter itself (i.e., it states that the axiom must hold for all type arguments). (Silver#758)
Functions can be annotated as @opaque(), which means that their definitions are not available by default. For opaque functions, any use of the function can be annotated with @reveal() to make the definition available for that specific function application. (Silicon#767) and (Carbon#474)

API changes:

The classes ErrorReason and VerificationError are now sealed. Code that extended them must now extend ExtensionAbstractVerificationError and ExtensionAbstractErrorReason, respectively. (Silver#749)
The ParseAST has been heavily reworked, which may require adaptations in plugins that work on the ParseAST level. Additionally, the order of constructor arguments of the PredicateInstance class in the predicate instance plugin has been switched. (Silver#764)

Changes in plugins:

Viper now includes a new smoke detection plugin that automatically checks if e.g. preconditions are unsatisfiable or branches are reachable by inserting refute false in various locations in the program. The plugin is not enabled by default. (Silver#762)
The ADT plugin now automatically generates well-foundedness axioms for each declared ADT type if the termination plugin is used, s.t. ADT values can be used as termination measures without the user having to declare them. (Silver#743)
Two bug fixes in the termination plugin:
- An incompleteness in the termination plugin affecting functions whose preconditions contain quantified permissions has been fixed (Silver#754)
- decreases clauses with predicate instances can now be written anywhere in function specifications (previously could not be after the postcondition) (Silver#738)
Fixed a bug in the refute plugin that prevented it from working inside loops in Carbon (Silver#736)

Other Viper-level improvements:

Substantially improved parsing and type checking errors (as well as parsing performance) (Silver#764)
Fixed a bug where domain axioms were not instantiated for all relevant cases (Silver#742)
Two improvements in trigger inference:
- Proper treatment of let-expressions when generating triggers (Silver#753)
- Trigger inference no longer incorrectly omits old (Silver#747)

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

Soundness fixes:
- Fixed a long-standing unsoundness and incompleteness related to packaging magic wands (Silicon#757)
- Fixed an incorrect well-definedness check of branch conditions inside goto-loops (Silicon#774)
- Fixed a missing check for map lookups (Silicon#770)
Completeness improvements:
- Silicon now uses Carbon's more complete axiomatization for sequences, sets and multisets. This usually comes with little or no performance cost, but we have observed individual examples where the new axioms caused non-termination or significantly worse verification time. We would be very grateful if users who observe additional examples where the new axiomatization leads to severe problems filed issues or sent us the problematic examples in some other way. Silicon's old axiomatization is still available and can be used via the command line option --useOldAxiomatization. (Silicon#642)
- Fixed an incompleteness when exhaling a quantified permission with a permission amount that depends on the quantified variable inside a package block (Silicon#797)
- Fixed an issue where a function definition was available too late (Silicon#744)
- Two completeness improvements of exhale mode 1 (aka moreCompleteExhale) (Silicon#760) and (Silicon#795)
Fixed crashes:
- when using Z3 via its API and interpreted functions (Silicon#752)
- when using predicate or wand triggers inside functions (Silicon#759)
Performance improvements
- More consistent caching for quantified permissions (Silicon#792)
- Better heuristics for quantified permissions (Silicon#789)
Other improvements
- Added a command line flag --disableNL to easily disable non-linear integer arithmetic reasoning in Z3 (Silicon#783)
- Added support for an experimental method annotation @proverArgs(key=value) that allows setting Z3 configuration parameters on a per-method basis (Silicon#784)
- Fixed incorrect branch conditions in symbolic execution log (Silicon#790)

Verification Condition Generation Backend (Carbon)

Soundness fixes:
- Exhaling quantified magic wands is now sound (Carbon#473)
Other improvements:
- Added support for several missing features: (Carbon#473)
- quantified magic wands
- magic wands as triggers
- perm for magic wands
- forperm with more than one quantified variable
- forperm for magic wands
- Added a command line option --timeout=n to set an overall verification timeout (in seconds) (Carbon#483)
- Several internal encoding improvements:
- Improved encoding of the old state (Carbon#482)
- Improved encoding of if statements (Carbon#478)
- Improved encoding of method calls (Carbon#477)

Based on - ViperServer release v.24.01-release - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - 4.2.1-RC

Based on - ViperServer release 23.07-RC2 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - 4.2.0-RC

Based on - ViperServer release 23.07-RC - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - 4.3.0-RC

Based on - ViperServer release 24.01-RC1 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-17-0723

Based on - ViperServer release v-2024-02-17-0714 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-16-0720

Based on - ViperServer release v-2024-02-16-0712 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-10-0723

Based on - ViperServer release v-2024-02-10-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-09-0722

Based on - ViperServer release v-2024-02-09-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-08-0721

Based on - ViperServer release v-2024-02-08-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2024-02-01-0836

Based on - ViperServer release v.23.07-release - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2023-12-16-1716

Based on - ViperServer release v-2023-12-16-0714 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2023-12-15-0759

Based on - ViperServer release v-2023-12-15-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2023-12-06-0725

Based on - ViperServer release v-2023-12-06-0713 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 2 years ago

viper-ide - Nightly Release v-2023-09-27-0729

Based on - ViperServer release v-2023-09-27-0716 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-08-26-2125

Based on - ViperServer release v-2023-08-26-0719 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - v4.2.2 (July 2023 release)

Release 2023.7

Date 31/07/23

Changes in Viper Language

Improved language flexibility (Silver#685): The syntax of declarations and assignments is now more permissive, allowing, for example, multiple declarations at once: field n: Ref, m: Ref // Declare multiple fields at once var a: Ref, b: Ref, c: Int // Declare multiple locals at once Additionally, method calls and new statements can now have fields or newly-declared local variables on their left hand side: var f: Ref := new(n) // Declare and initialise locals with `new` a, f.n := get_refs() // Assign to field from method call f.n := new(n) // Assign to field with `new` The Viper AST remains unchanged; the newly-supported syntax is desugared into equivalent code that uses the existing Viper AST.
Annotations (Silver#666): The Viper language now has support for annotations on statements, expressions, and top-level declarations. The syntax for an annotation is @key("value", "value2", ...), i.e., they have a key which is preceded by an @ sign and a sequence of values written as comma-separated string literals. A single expression/statement/declaration can have multiple annotations. If there are two annotations of the same key, their value sequences are concatenated. In the AST, annotations are represented in the info field of the annotated AST node using an AnnotationInfo object. Currently, there are two supported annotations: @weight("n") on quantifiers, where n is a positive integer, sets the weight of the quantifier in the SMT solver. The second annotation is exclusive to the Symbolic Execution backend (see below). Unknown annotations are ignored.
Domain axioms may now refer to non-domain functions that do not have any preconditions (Silver#698).
Support for chained comparisons (Silver#713): expressions like e1 < e2 <= e3 > e4 can now be parsed and will be desugared to (e1 < e2) && (e2 <= e3) && (e3 > e4). The AST nodes for comparison operations remain unchanged.
Two important changes in the termination plugin:
- The termination plugin now enforces that functions that refer to themselves (or to other functions that call the original function in a mutually-recursive way) in their own postconditions have a decreases clause (Silver#711). That is, for such functions, one must either prove termination using a decreases clause, or explicitly state that termination should be assumed by writing decreases *. This change addresses frequent issues where users wrote functions that are not well-defined using such postconditions and subsequently reported seemingly unsound behavior (e.g., (Silver#525) and (Silver#668)).
- The termination plugin now automatically imports the default definitions of well-founded orders if decreases-clauses are used but no such definitions are present in the program (Silver#710). That is, it is not longer necessary (but still possible) to write an import statement like import <decreases/int.vpr> when using a termination measure of type integer.
The Rational type, an alias for Perm, is deprecated. Viper issues a warning whenever the type is used.

Viper API Changes

Introduced a new API for frontends to interact with Viper (Silver#732). Frontends can create instances of ViperFrontendAPI and interact exclusively through those (instead of instances of Verifier or SilFrontend), which saves some boilerplate code and lets Viper manage plugins.

Other Viper-level Improvements

Improved error messages for parse errors (Silver#702) and type errors ((Silver#684), (Silver#724))
Fixed parsing and pretty-printing of scopes (Silver#704), which were previously ommitted under some circumstances by both the pretty-printer and the parser, which could make otherwise valid Viper code invalid.
Introduced caching to improve performance of common lookups on the AST ((Silver#659) and (Silver#719))
Viper now reports inferred quantifiers using a QuantifierInstantiationsMessage (Silver#653)
Introduced various new consistency checks for invalid code that used to crash the backends or lead to unexpected behavior:
- perm-expressions are no longer allowed in function postconditions (Silver#681)
- wildcard is no longer allowed as part of compound expressions (Silver#700)
- empty ADTs are rejected (Silver#696)
- predicate argument expressions must be pure (Silver#721)
Labelled old-expressions may now be used as triggers (Silver#695)
Various small fixes for crashes or other incorrect behavior.

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

The previously experimental mode --moreCompleteExhale is no longer experimental, but is now a supported mode that performs exhales and heap lookups in a way that is usually more complete (but possibly slower). However, Silicon's previous exhale mode remains the default. (Silicon#682)
- The new flag --exhaleMode=n, where n is 0, 1, or 2, can now be used to select the exhale mode. 0 is the default, 1 is the previous moreCompleteExhale mode.
- The new exhaleMode 2 uses the default exhale mode 0 throughout the program, until it encounters a verification error. When it does, it retries proving the failing assertion using the (more complete) mode 1. Since mode 0 is usually faster than mode 1, mode 2 often results in the best mix of performance and completeness.
- Additionally, one can now override the exhale mode selected via command line for individual methods using an annotation @exhaleMode("n") on the method (Silicon#724)
Via the option --prover=Z3-API, Silicon can now use Z3 as a library via its Java API ((Silicon#633) and (Silicon#692)). Note that this requires a native version of libz3java to be present on the path Java uses to look for native libraries (which can be set, e.g., via the environment variableLD_LIBRARY_PATH on Linux or DYLD_LIBRARY_PATH on MacOS). Depending on the OS and the Viper program, this option can lead to a significant speedup.
Silicon now emits warnings in cases where it cannot use the triggers specified by the user (Silicon#687)
old-expressions in triggers are now interpreted correctly (Silicon#710); previously, they were sometimes ignored.
Changed default options used for Z3; the new options have similar performance and completeness characteristics with the supported Z3 version 4.8.7, but perform better with newer versions (tested in particular with 4.12.1) (Silicon#694)
Silicon no longer creates a tmp directory containing .smt2 files that log its prover interactions by default (Silicon#709). The flag --disableTempDirectory no longer exists. Instead, one can use the new flag --enableTempDirectory or the flag --proverLogFile.
Improved heuristics for handling of quantified permissions, which improves performance in some cases (Silicon#704)
Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases (Silicon#705)
Added a new command line flag --reportReasonUnknown, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error) (Silicon#701). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.
Fixed five unsoundnesses:
- Incorrect handling of old-expressions in postconditions of methods called inside a package statement (Silicon#699)
- Incorrect handling of fold statements for predicates that are used inside a quantified permission in the current method (Silicon#696)
- Incorrect behavior for quantifiers whose bodies have unreachable branches (Silicon#690)
- Incorrectly terminating verification after using a refute (Silicon#741)
- Exhale mode 1 now correctly checks permission amounts in function preconditions (Silicon#682)
Fixed and generalized the experimental mode --conditionalizePermissions, which avoids branching on conditional permission assertions (e.g., b ==> acc(x.f)) by rewriting them to unconditional assertions with conditional permission amounts (e.g., acc(x.f, b ? write : none) whenever possible (Silicon#685). For programs with many branches, this option can improve performance.
Resource triggers on existentials now work correctly (Silicon#679)
More complete computation of function footprints (Silicon#684)
Various smaller bug fixes

Verification Condition Generation Backend (Carbon)

Improved encoding of well-definedness checks for field accesses and permission division (Carbon#451). As a result, Carbon now emits well-definedness errors in the expected order in some cases where this was previously not the case.
Improved encoding of definedness checks during exhale (Carbon#457). This fixed both possible unsoundness and incompleteness issues.
Using stdin instead of a temporary file to communicate with Boogie (Carbon#456)

Based on - ViperServer release v.23.07-release - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-08-05-1220

Based on - ViperServer release v-2023-08-05-0715 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-08-02-0730

Based on - ViperServer release v-2023-08-02-0718 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-07-18-0828

Based on - ViperServer release v-2023-07-17-1747 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-07-05-0730

Based on - ViperServer release v-2023-07-05-0717 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-06-15-0756

Based on - ViperServer release v-2023-06-15-0740 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 2 years ago

viper-ide - Nightly Release v-2023-05-17-0733

Based on - ViperServer release v-2023-05-17-0718 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-05-13-0727

Based on - ViperServer release v-2023-05-13-0715 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-05-05-0727

Based on - ViperServer release v-2023-05-05-0715 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-04-14-0820

Based on - ViperServer release v-2023-04-14-0806 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-04-08-0729

Based on - ViperServer release v-2023-04-08-0717 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-29-1448

Based on - ViperServer release v-2023-03-29-1414 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-28-2058

Based on - ViperServer release v-2023-03-28-2044 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-22-2238

Based on - ViperServer release v-2023-03-20-0717 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-17-0730

Based on - ViperServer release v-2023-03-17-0718 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-15-0748

Based on - ViperServer release v-2023-03-14-0716 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-10-1726

Based on - ViperServer release v-2023-03-10-1710 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-03-02-1938

Based on - ViperServer release v-2023-03-02-1655 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-02-26-2019

Based on - ViperServer release v-2023-02-24-1337 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-02-23-0933

Based on - ViperServer release v-2023-02-21-0716 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] almost 3 years ago

viper-ide - Nightly Release v-2023-02-18-0729

Based on - ViperServer release v-2023-02-18-0715 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-02-14-1040

Based on - ViperServer release v-2023-02-11-1555 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-02-09-0726

Based on - ViperServer release v-2023-02-09-0714 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-02-03-0729

Based on - ViperServer release v-2023-02-03-0715 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-02-02-1102

Based on - ViperServer release v-2023-02-02-1019 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - v4.1.1

This release is identical to the January 2023 release.

Based on - ViperServer release v.23.01-release - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - v4.1.0 (January 2023 release)

Release 2023.1

Date 25/01/23

Changes in Viper Language

Quasihavoc: New statements quasihavoc and quasihavocall allow explicitly losing information about a resource. E.g., quasihavoc c ==> P(x) havocs the snapshot of resource P(x) if c is true and some permission to P(x) is held, and does nothing otherwise. Semantically equivalent to (conditionally) exhaling the current permission amount to the given resource and inhaling it again, but implemented more efficiently. For more details, see this report (Silver#611). Currently, the Symbolic Execution backend (Silicon) fully supports quasihavoc and quasihavocall, while the Verification Condition Generation backend (Carbon) only supports quasihavoc for field and predicate resources and does not suport quasihavocall.
Syntax for backend types added in the form of domains with interpretations: Domains can be annotated with interpretations for different backends. E.g., domain myBV interpretation (SMTLIB: “(_ BitVec 32)”, Boogie: “bv32”) { ... } will be interpreted by Silicon as the SMTLIB type (_ BitVec 32) and by Carbon as the Boogie type bv32. Similarly, domain functions can be annotated with SMTLIB interpretations. (Silver#638)

Viper API Changes

Breaking change: The plugin API has been extended with a method to transform verification results for individual entities, in addition to the existing method to transform the verification result for the entire Viper program. Plugins should implement both methods; the former is used to transform verification results for individual members that are streamed via the Reporter interface (Silver#641). Additionally, the signature of the existing method has been changed in order to remove the need for plugins to maintain state.
Experimental quantifier weight support: Quantifiers can be given a weight to be used by the SMT solver by annotating them with special WeightedQuantifier info objects (Silver#633). Currently only available on the AST level (without syntax support), and only supported in the Symbolic Execution backend.
Breaking change: AST nodes for BackendFunctions have been changed to accommodate the new syntax for interpreted domains (see above): Among other small changes, BackendFunc objects no longer exist, and are replaced by DomainFuncs with interpretations. (Silver#638)

Other Viper-level Improvements

Improved pretty-printing of ASTs (Silver#616)
Improved parsing and better consistency checks for invalid triggers, invalid predicate accesses, and invalid domain types (Silver#601), (Silver#614), (Silver#626), (Silver#643)
Improved type checking performance for large methods (Silver#631)
Termination plugin generates simpler code (Silver#613) and supports more complex expressions (Silver#618)
Several bug fixes (Silver#607), (Silver#590), (Silver#636), (Silver#635)

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

Parallel branch verification: Use option --parallelizeBranches to verify different branches of a method in parallel. Generally speeds up verification but may lead to non-deterministic verification time. (Silicon#634)
Parallel Silicon instances: Multiple verifier instances can be used in parallel (Silicon#635), (Silver#600)
Soundness fixes for several long-standing soundness issues. As a result, standard Silicon currently has no known soundness issues outside of magic wands. Fixes include:
- Function encoding (Silicon#376), (Silicon#369)
- Quantified permission encoding for finite domains (Silicon#342), (Silicon#636)
- Quantifier encoding (Silicon#560), (Silicon#652)
Improved SymbExLogger is now thread safe and reports records via a SymbLogListener interface (Silicon#622).
Multiple performance improvements, mostly related to quantified permissions (Silicon#668), (Silicon#649), (Silicon#651), (Silver#604), (Silver#605)
Fixed crashes and other issues (Silicon#648), (Silicon#321), (Silicon#641), (Silicon#665)

Verification Condition Generation Backend (Carbon)

Boogie Version upgraded to 2.15.9 (Carbon#441)
Inconsistent interpretation of division and modulo fixed (Carbon#448)
Boogie and Z3 instances are now stopped if Carbon is interrupted (Carbon#426)

Based on - ViperServer release v.23.01-release - Z3 4.8.7 - Boogie release 2.15.9

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-01-31-0912

Based on - ViperServer release v-2023-01-30-1404 - Z3 4.8.7 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-01-27-0727

Based on - ViperServer release v-2023-01-27-0713 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - 4.1.0-RC

Based on - ViperServer release 23.01-RC - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-01-24-1437

Based on - ViperServer release v-2023-01-24-0718 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-01-06-1708

Based on - ViperServer release v-2023-01-06-1656 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2023-01-06-1101

Based on - ViperServer release v-2023-01-03-1402 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2022-12-12-0727

Based on - ViperServer release v-2022-12-12-0715 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2022-11-28-0726

Based on - ViperServer release v-2022-11-28-0714 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] about 3 years ago

viper-ide - Nightly Release v-2022-11-15-1354

Based on - ViperServer release v-2022-11-15-0715 - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 3 years ago

viper-ide - v4.0.1 (November 2022 release)

Viper's July 2022 release is used for the language and verification backends. For ViperServer, the November 2022 release is used that fixes several LSP related bugs in ViperServer.

Based on - ViperServer release v.22.11-release - Z3 4.8.6 - Boogie release latest

- TypeScript
Published by github-actions[bot] over 3 years ago