viperproject/gobra v25.02

February 2025 release

on GitHub

Based on Viper v.25.02 release

What's Changed

• Fix #713 by @Felalolf in #732
• Add a flag to enable silicon's unsafe wildcard multiplication by @jcp19 in #739
• Fix #511 by @jcp19 in #740
• Add --moreJoins flag from silicon by @jcp19 in #742
• Fix #734 by @Felalolf in #735
• Improves Error Messages for Assignments by @Felalolf in #746
• Add support for backend annotations on functions and methods by @jcp19 in #749
• Update to new chopper version by @Felalolf in #744
• Add missing termination measures in the sequence and array encodings by @jcp19 in #758
• more flexible joins from silicon by @jcp19 in #761
• Fix incompletness with conversions to and from strings by @jcp19 in #763
• Fix purity classification of composite literals by @jcp19 in #768
• Support for Ghost Pointers by @ArquintL in #747
• Disallows impure non-ghost calls in ghost code by @ArquintL in #755
• Support for Ghost Fields by @ArquintL in #766
• Ghost Pointer & Ghost Fields by @ArquintL in #771
• Gobra CLI Input Documentation by @ArquintL in #610
• Add purity checks to the ternary expression by @jcp19 in #778
• Add refute statement by @bruggerl in #776
• Impure assume by @bruggerl in #779
• Fix issue #781 by @ArquintL in #785
• Revert "Add refute statement" by @jcp19 in #787
• docs: correct function name in tutorial by @aaronbojarski in #789
• Fix bounds of singed integers for overflow checking by @jcp19 in #795
• Fix #796 by @jcp19 in #800
• Change computation of unsigned type bounds to prevent overflows by @jcp19 in #801
• Use option --respectFunctionPrePermAmounts in the backends by @jcp19 in #813
• Reinstate the usage of the SilFrontend API and support for the refute statement by @jcp19 in #818
• Add support for new interpretation of fractional perms in pure function preconditions by @jcp19 in #822
• Fix #823 by @ArquintL in #825
• More robust config creation by @ArquintL in #824
• Relative Paths in Generated Parser by @ArquintL in #827
• Fix #828 by @ArquintL in #833
• Fix #836 by @jcp19 in #837
• Change the default interpretation of access predicates in function preconditions according to the new semantics of Viper by @jcp19 in #843
• Expands tutorial by total correctness by @ArquintL in #847
• Generate parser by @ArquintL in #848
• Fix parser generation for dependers by @ArquintL in #851
• Optimize parser generation by @ArquintL in #852
• Fix nit in tutorial. by @jhoyla in #853
• Avoids type-checking if imports contain errors by @ArquintL in #855
• Support for Ghost Types by @ArquintL in #773
• Fix #620 by @ArquintL in #863
• Fix #861 by @ArquintL in #862
• Slice cap operation didn't check underlyingTypes by @Dspil in #867
• Fix Link by @felixlinker in #870
• Fix reserved parser keyword error reporting by @ArquintL in #869
• Domains under interface by @ArquintL in #860
• Fix exception when checking whether an imported domain is identity preserving by @ArquintL in #875

New Contributors

• @bruggerl made their first contribution in #776
• @aaronbojarski made their first contribution in #789
• @jhoyla made their first contribution in #853
• @felixlinker made their first contribution in #870

Full Changelog: v24.02...v25.02