VerCors 1.4.0
Warning: this release has a path problem on windows. If you are a windows user, please use dev branch release: https://github.com/utwente-fmt/vercors/releases/tag/dev-prerelease
What's Changed
What's Changed
- Windows support by @ArmborstL in #582
- Reinstate carbon by @bobismijnnaam in #577
- Guide pass progression by AST properties (features) by @niomaster in #541
- rename DivAssign to FloorDivAssign by @Vescatur in #590
- permission values should be rationals; some formatting fixes by @niomaster in #575
- Fix grammar warnings by @bobismijnnaam in #587
- support given/yields for kernels, support multiple upper bounds in quantified relational expressions by @niomaster in #591
- fixed NullPointerException in CreateReturnParameter.java by @ArmborstL in #606
- use Path objects instead of plain Strings to track file origins. Fixes #601 by @Jankoekenpan in #602
- Standardize "resource functions" to predicates by @niomaster in #607
- Upgrade to viper 21.01 by @bobismijnnaam in #580
- changes to PVL and JavaPrinter and PVLSyntax by @petravandenbos-utwente in #616
- Update options of VerCors by @Sophietje in #586
- Issue 614 by @ArmborstL in #617
- order of annotations is now preserved almost by @petravandenbos-utwente in #618
- run sbt for classpath from repo root by @niomaster in #611
- Issue #621: improved support for set comprehension by @ArmborstL in #622
- Remove unused rewrite passes by @Sophietje in #615
- disabled fail-fast strategy #issue-626 by @Vescatur in #627
- Issue 628 shared run configurations and list of failing tests by @Vescatur in #630
- Fix ArrayNullValuesSpec: make sequence as primitive type (not old style) by @niomaster in #638
- Issue 633 by @Vescatur in #634
- Predicate refactor 2 by @bobismijnnaam in #639
- VeyMont merge into VerCors by @Sophietje in #641
- reduce veymont code smells by @petravandenbos-utwente in #645
- Upgrade SBT to 1.5.1 by @bobismijnnaam in #632
- Add exception patterns case study & re-enable elect.pvl by @bobismijnnaam in #635
- Issue 449 - sonarcloud by @Vescatur in #647
- Issue 449 remove commented code by @Vescatur in #648
- Fork examples by @petravandenbos-utwente in #652
- Add coverage by @bobismijnnaam in #487
- Testsuite verdict strict by @bobismijnnaam in #599
- Final fix for coverage by @bobismijnnaam in #656
- Skip backend & skip transformations flags by @bobismijnnaam in #657
- Proper error when unfolding abstract predicate by @bobismijnnaam in #659
- Issue 509 slow tests by @Vescatur in #649
- Fix simple-ltid.cu by @bobismijnnaam in #661
- Reinstate History.pvl by @bobismijnnaam in #662
- Reinstate monotonicBool & monotonicBoolBroken by @bobismijnnaam in #667
- Issue 663 2 by @Vescatur in #669
- fix sonar test by @Vescatur in #670
- Veymont fix bugs and test cases by @bobismijnnaam in #672
- Run VeyMont in CI by @bobismijnnaam in #673
- Add a trait which makes the main method explicit by @Vescatur in #677
- Issue 664 - removing unused code by @Vescatur in #671
- added examples from verifyThis competitions by @ArmborstL in #697
- Make formatting of printed information consistent and print verification start time. by @bobismijnnaam in #698
- Change vsum axioms to only return null upon an empty range, and not an invalid range by @bobismijnnaam in #699
- Viper 21.07 by @bobismijnnaam in #700
- Ensure vercors package works in the presence of long paths by @bobismijnnaam in #702
- Fix trigger generation for
\values
by @bobismijnnaam in #706 - Enhance exists by @bobismijnnaam in #705
- Add more detailed version info to
--version
by @bobismijnnaam in #707 - Generate triggers more conservatively by @bobismijnnaam in #708
- Replace old in syntax with slash syntax by @bobismijnnaam in #709
- More explicitly print the context if a name cannot be resolved by @bobismijnnaam in #710
- Also print trigger candidates if body is not eq, ne, etc. by @bobismijnnaam in #711
- Add Wiki to PDF/HTML workflow by @bobismijnnaam in #712
- Add injectivity/equality axiom to Option by @bobismijnnaam in #713
- Enable GPGPU examples for testing by @bobismijnnaam in #715
- Test wiki snippets in CI by @bobismijnnaam in #714
- Move old rewrite rules to file in util/ by @bobismijnnaam in #716
- Take
synchronized
into account when computing features by @bobismijnnaam in #717 - Fix that a return parameter assignment is not created on function calls by @bobismijnnaam in #719
New Contributors
- @ArmborstL made their first contribution in #582
- @Jankoekenpan made their first contribution in #602
Full Changelog: v1.3.0...v1.4.0