viperproject/gobra v26.09

on GitHub

What's Changed

• Fix error position when output parameters are used in the postcondition of pure functions and methods by @jcp19 in #1006
• add initial AGENTS.md by @jcp19 in #1009
• Configure Gobra via JSON by @ArquintL in #895
• Reject occurrences of output parameters in preconditions by @jcp19 in #1018
• Disallow conditional termination measures in ghost and pure members by @jcp19 in #1019
• Add support for existential elimination with assign such that by @jcp19 in #1021 & #1026
• Represent array type lengths as BigInt by @ArquintL in #1022
• Encoding changes for zero-sized data by @ArquintL in #1023
• Add missing position information in termination measures by @jcp19 in #1032
• Adds Unbounded Integer Type by @ArquintL in #1033
• Adjust preserves desugaring order by @ArquintL with @Copilot in #1035
• Lift asserting expressions from Viper by @jcp19 in #1036
• Allow outer function outputs in outline preconditions (Fix issue #1029) by @jcp19 in #1031
• Add position information to nodes related to closures that don't have it by @jcp19 in #1038
• Replace !<...!> predicate-constructor delimiters with {...} by @jcp19 in #1024
• Fix position of result assignments by @AndreaKe in #1046
• Fix issue #1045 by @jcp19 in #1047
• Fixes parsing of magic wands by @ArquintL in #1044
• Fixes bound checking for slice expressions and treats string literals as byte arrays by @ArquintL in #1055
• Fix #1057 by @ArquintL in #1058
• Variadic type identity by @ArquintL in #1065
• Fixes an incompleteness of append and copy by @ArquintL in #1064
• atomic methods and invariants by @jcp19 in #983
• Makes AdtT and AdtClauseT contextual types by @ArquintL in #1073
• Optimize openInvariants set usage in loops and methods by @jcp19 in #1074
• Reports the Gobra commit in the CLI version output and bumps the copyright year to 2026 by @ArquintL in #1076
• Resolve embedded interfaces through their owning type context's cached by @ArquintL in #1054
• Delegates interface method-set computation to the interface's owning type-checking context by @ArquintL in #1071
• Handle Throwable errors in main exception handler by @jcp19 in #1084
• Fix all compiler warnings and introduce a check that prevents new errors from being added by @jcp19 in #1086
• Fix crashes on comma-ok lookups and on comparing map lookups to nil (#893) by @jcp19 in #1087
• Add support for converting slices to sequences by @jcp19 in #1088
• Desugar map keys to the key type of the map by @jcp19 in #1085
• Add assert timeout configuration option for Silicon backend by @jcp19 in #1013
• Adds an API to cancel a running verification by @ArquintL in #1089
• Fix nil intf receiver for mpred by @ArquintL in #1094
• Improve Stats Writing in the Presence of Crashes by @ArquintL in #1099
• Upgrades z3 to 4.16.0 by @jcp19 in #1104
• Update to Viper's August 2026 release by @viper-admin in #1101
• Update sbt and its plugins by @jcp19 in #1107

New Contributors

• @Copilot made their first contribution in #1035
• @AndreaKe made their first contribution in #1046

Full Changelog: v26.02...v26.09