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) 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
• 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), with n bein 1 or 2 as just described, can be used to enable path joining on a per-method level viperproject/silicon#823
  • 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

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