v25.09-overflowchecks-alpha

Alpha version of Gobra based on v25.09 with overflow checks enabled.

v25.09

What's Changed

• Update Submodules by @viper-admin in #887
• Fix type-checker crash when encountering an invalid ADT by @ArquintL in #897
• Update Submodules by @viper-admin in #896
• Fix bug 805 by @jcp19 in #900
• Fix error obtained when importing sync with flag --noassumeInjectivityOnInhale by @jcp19 in #854
• Update Submodules by @viper-admin in #908
• Fix issue 858 by @jcp19 in #868
• errors.New by @ArquintL in #909
• Fix issue 866 by @jcp19 in #918
• Update Submodules by @viper-admin in #917
• Update Submodules by @viper-admin in #920
• Add support for converting maps to dicts by @jcp19 in #923
• Package invariants by @jcp19 in #810
• Update Submodules by @viper-admin in #926
• Fix using for range over map without using visited by @ThomasMayerl in #933
• Generate cleaner output by @jcp19 in #927
• Fix 864 by @jcp19 in #925
• Update Submodules by @viper-admin in #941
• Hyper Gobra by @jcp19 in #802
• Error reporting by @bruggerl in #945
• Use elem to denote ghost collection containment by @ArquintL in #944
• Fix issue 943 by @jcp19 in #947
• Fix issue 883 by @jcp19 in #952
• Add support for indexing strings by @jcp19 in #961
• Bump actions/checkout from 4 to 5 in the all group by @dependabot[bot] in #967
• Remove deprecated initialization postconditions by @jcp19 in #971

New Contributors

• @ThomasMayerl made their first contribution in #933

Full Changelog: v25.02...v25.09

February 2025 release

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

v24.02

What's Changed

• Add --conditionalizePermissions by @jcp19 in #628 & #629
• Allow go calls of closures by @jcp19 in #615
• Fixes running the chopper together with other Viper plugins ( issue #625) by @ArquintL in #632
• Support outlines in closures by @jcp19 in #633
• Add support for more complete exhale on demand by @jcp19 in #636
• Add support for converting floats into ints by @jcp19 in #643
• Added section on debugging to README. by @rayman2000 in #617
• Update syntax for set cardinality in the tutorial by @jcp19 in #603
• Fix #651 by @jcp19 in #652
• Fix #655 by @Felalolf in #656
• Fix #659 by @ArquintL in #660
• Parallelizing Gobra by @ArquintL in #634
• Avoiding accidental printing of ASTs by @ArquintL in #665
• Fix #668 by @Felalolf in #669
• Add flag to use Z3 via API by @Dspil in #666
• Slice from array didn't have termination measure by @Dspil in #674
• Missing termination measures by @Dspil in #675
• Enable let expressions with weakly pure subexpressions by @jcp19 in #678
• Improvements in maps by @jcp19 in #676
• Add flag to require triggers in all quantifiers by @jcp19 in #679
• Several ADT improvements by @Felalolf in #687
• Treat values of type InternalSingleMulti(t, ms) as t for nested dictionaries by @jcp19 in #699
• Allow for recursive implementations of errors.Error() by @jcp19 in #700
• Do not use underlying type when inferring the type of some(...) by @jcp19 in #701
• Fixes #695 by @ArquintL in #696
• Re-do termination measures for methods in error by @jcp19 in #703
• Fix #705 by @ArquintL in #706
• Fixes Pretty Printer by @ArquintL in #711
• Flag for non-linear integer arithmetic by @Dspil in #709
• Add option to disable set axiomatization by @dnezam in #708
• Check by default that all pure and ghost functions have termination measures by @jcp19 in #718
• Fixes #697 by @ArquintL in #698
• Add opaque/reveal to Gobra by @dnezam in #715
• Improve Gobra Package Information by @ArquintL in #725
• Update ViperServer to Viper January 2024 release by @ArquintL in #729

New Contributors

• @rayman2000 made their first contribution in #617
• @dnezam made their first contribution in #708

Full Changelog: v23.02...v24.02

v23.02

What's Changed

• Fix lazy generation of the string domain by @jcp19 in #547
• Update Submodules by @viper-admin in #549
• Improving the Import of Termination Axioms by @ArquintL in #548
• Fixes Pure Function Calls whose Result is Unused by @ArquintL in #550
• Range by @Dspil in #551
• Update Submodules by @viper-admin in #552
• Skip Termination Checks for Imported (Pure) Functions & Methods by @ArquintL in #546
• Fix issue 553 by @jcp19 in #557
• Allow BaseConfig to skip verification by @ArquintL in #559
• Update Submodules by @viper-admin in #561
• Disable problematic tests by @jcp19 in #563
• Update Submodules by @viper-admin in #562
• Add distinction between shared and exclusive global variables by @jcp19 in #560
• Update Submodules by @viper-admin in #564
• Update Submodules by @viper-admin in #566
• Simplify encoding of NewSliceLit by @jcp19 in #567
• Made field names more specific by @Felalolf in #568
• Optimize map encoding by @jcp19 in #570
• Fix issue 573 by @jcp19 in #574
• reduce the exhale permissions from maps in range by @Dspil in #575
• Fix 576 by @jcp19 in #577
• Make receive executable by @jcp19 in #578
• Update Submodules by @viper-admin in #579
• Update Submodules by @viper-admin in #581
• Adts by @Felalolf in #580
• Remove sneaky heap-dependent triggers by @jcp19 in #582
• Fix comparability issues with builtin functions... by @jcp19 in #583
• Update Submodules by @viper-admin in #584
• Update Submodules by @viper-admin in #585
• Update Submodules by @viper-admin in #586
• Update Submodules by @viper-admin in #587
• Streaming errors by @Dspil in #590
• Update CI Dependencies by @ArquintL in #592
• Introduce len for ADTs to be used as a termination measure by @jcp19 in #591
• Fix --debug flag by @jcp19 in #593
• More precise triggers for smake by @jcp19 in #594
• Update Submodules by @viper-admin in #598
• QoL improvements by @jcp19 in #599
• print early errors that don't go through the streaming reporter by @Dspil in #597
• Allow non-side-effectful conversions in spec by @jcp19 in #600
• weaker error contract by @Dspil in #602
• Better error spec by @jcp19 in #604
• Update Submodules by @viper-admin in #605
• Update Submodules by @viper-admin in #608
• Encode slice make as a method call by @jcp19 in #607
• Update Submodules by @viper-admin in #611
• Use ghost equality in the generated invariants for range loops over slices by @jcp19 in #613
• add missing termination measures in box/unbox functions by @jcp19 in #614
• Undo #607 due to bug observable in SCION by @jcp19 in #616
• let expression support by @Dspil in #618
• Fix issue 621 by @jcp19 in #622

Full Changelog: v22.10...v23.02

v22.10

What's Changed

• Add termination measure to shStructDefault by @jcp19 in #495
• Introduce support for closures by @stefanomil in #479
• Add script to generate parser by @jcp19 in #498
• Make closure calls deferrable by @stefanomil in #501
• Add initial support for global variables by @jcp19 in #465
• Range by @Dspil in #496
• Remove unnecessary check by @jcp19 in #507
• Use ghostComparableTypes when type-checking PIn by @jcp19 in #508
• Use underlying type in type-checking range loops by @jcp19 in #509
• Allow constants of defined types, as long as there are constant values for their underlying type by @jcp19 in #510
• Introduce ghost equality (===) and inequality (!==) by @jcp19 in #514
• Update Gobra to the newest Viper version by @jcp19 in #499
• Update to latest version of silver with parallel branches by @jcp19 in #516
• Fixes #519 by @Felalolf in #520
• Remove redundant checks when comparing interfaces with the nil literal by @jcp19 in #522
• Remove unnecessary occurrences of the 'true' literal by @jcp19 in #524
• Add option to disable the behaviour of "moreCompleteExhale" by @jcp19 in #526
• Verify chopped parts in parallel by @jcp19 in #525
• Fix default value of option disableMoreCompleteExhale by @jcp19 in #527
• Changed Map and Slice Literals to Statements since they have side-effects by @Felalolf in #528
• updated viperserver version by @Felalolf in #530
• Remove node and strategy by @Felalolf in #529
• Use let expressions in encoding to reduce redundancy by @Felalolf in #535
• Fixes conversion to interfaces and interfaces in struct literals by @jcp19 in #537
• Auto-update ViperServer submodule by @ArquintL in #539
• Create gobrafied debug files by @ArquintL in #540
• Update Submodules by @viper-admin in #542
• CLI Option for Disabling Support for Global Variables by @ArquintL in #541
• Constant propagation by @jcp19 in #538
• Fix #544 by @jcp19 in #545

New Contributors

• @stefanomil made their first contribution in #479

Full Changelog: v22.07...v22.10

v22.07

What's Changed

• Example using Shared Variables by @ArquintL in #259
• Add support for short-hand for implementation proofs by @jcp19 in #463
• Add support for perm constants by @jcp19 in #462
• add variable to proofName to generate unique names by @Dspil in #464
• Outline statement by @Felalolf in #460
• Aliased type for any = interface{} by @gavinleroy in #467
• Encoding refactor by @Felalolf in #466
• Simple defer by @Felalolf in #469
• Make defer statement ghostifiable by @jcp19 in #470
• Improve trigger for acc(s) when s is a slice by @jcp19 in #471
• Fix duplicate type tags in the encoding by @jcp19 in #472
• fixed an incorrect type argument by @Felalolf in #476
• Add support for arrays of custom declared types by @jcp19 in #481
• Fix issue #151 by @jcp19 in #482
• Fix 475 by @jcp19 in #483
• Fix issue 486 (V2) by @Felalolf in #488
• Fix issue #489 by @jcp19 in #490
• Fix gobraDirectory and change severity of the warnings by @jcp19 in #493
• Embedded interfaces by @Dspil in #492

New Contributors

• @gavinleroy made their first contribution in #467

Full Changelog: v22.05...v22.07

v22.05.1

This release does not yet introduce the changes from PR #457. That will be done in the next release.