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) viperproject/silver#802
API Changes and Internal Improvements
- Improved
Simplifier
simplifies many additional expressions; new option determines whether simplification must preserve well-definedness viperproject/silver#810 - Chopper is now aware of opaque functions viperproject/silver#779
- Chopper has improved dependency analysis for axioms viperproject/silver#776
- Removed filtering of duplicate errors inside Viper (this is now left to frontends) viperproject/silver#778
Bug Fixes
- Fixed various issues with macro expansion:
- Fixed incorrect variable renaming during macro expansion viperproject/silver#804
- Disallowing nested macro declarations viperproject/silver#795
- Fixed incorrect renaming of label statements during macro expansion viperproject/silver#793
- Fixed incorrect
Simplifier
handling of division and modulo expressions viperproject/silver#794 - Fixed crash in proof obligation computation for expressions viperproject/silver#783
- Termination plugin: Improved encoding of checks for
unfolding
-expressions viperproject/silver#773 - ADT plugin: Fixed crash when plugin is used with other AST extensions viperproject/silver#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. viperproject/silicon#863 - Soundness fixes:
- Fixed unsound rewrite for
--conditionalizePermissions
option viperproject/silicon#853 - Fixed unsound handling of quantified permissions with unsatisfiable condition viperproject/silicon#843
- Fixed unsound handling of quantified permissions with trivial condition viperproject/silicon#834
- Improved encoding of magic wand snapshots that prevents unsoundness for
applying
-expressions viperproject/silicon#836 - Fixed incorrect order of function precondition assumptions viperproject/silicon#811
- Fixed unsound rewrite for
- Completeness improvements:
- Recording missing constraints during function verification viperproject/silicon#852 and viperproject/silicon#825
- Fixed treatment of snapshot maps defined while evaluating quantifiers viperproject/silicon#840
- Avoiding using a quantifier for wildcard constraints for quantified resources when possible viperproject/silicon#817
- Performance improvements:
- Improved snapshot map caching for quantified permissions (also improves completeness) viperproject/silicon#846
- Avoiding creating new snapshot maps for quantified resources when unnecessary viperproject/silicon#839
- Eagerly assuming non-aliasing for quantified field chunks viperproject/silicon#835
- More efficient function axiomatization for functions with many branches viperproject/silicon#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. viperproject/silicon#823 - The new annotation
@moreJoins(n)
, withn
bein1
or2
as just described, can be used to enable path joining on a per-method level viperproject/silicon#823
- With command line argument
- More flexible state consolidation:
- Added several new options for state consolidation behavior viperproject/silicon#827
- The new annotation
@stateConsolidationMode(n)
allows configuring state consolidation on a per-method level viperproject/silicon#827
- Other improvements:
- Fixed crash resulting from double-declarations of macros with
--parallelizeBranches
viperproject/silicon#813 - Fixed error reporting for method call arguments viperproject/silicon#841
- Silicon now tries to find the Z3 executable in PATH if no path is explicitly provided viperproject/silicon#818
- Fixed crash resulting from double-declarations of macros with
Verification Condition Generation Backend (Carbon)
- Bug fixes:
- Preventing Boogie crash when using annotations viperproject/carbon#505
Based on
- ViperServer release
v.24.08-release
- Z3
4.8.7
- Boogie release
7449a7a899c02c95