Releases: utwente-fmt/vercors
VerCors Nightly
Nightly Build
VerCors Wiki PDF
These are automatically generated versions of the tutorial on the VerCors wiki. There are two artefacts of interest: the Latex/PDF version, suitable for printing, and the HTML version, suitable for offline viewing.
VerCors 2.2.0
What's Changed
- Add challenge 3 from the verifyThis 2019 challenge by @sakehl in #1167
- Generics for PVL classes by @bobismijnnaam in #1154
- Watch input files by @pieter-bos in #1192
- Add challenge 1 and challenge 2 of verifythis 2024 by @superaxander in #1190
- Parser analysis by @pieter-bos in #1200
- Small fix by @sakehl in #1197
- Prepare formatting rules by @pieter-bos in #1205
- VeyMont: name refactoring, implementation generation, endpoint context, channel invariant partial support by @bobismijnnaam in #1188
- Small debug fixes 2 by @bobismijnnaam in #1048
- Vector support in C, OpenCL and CUDA + Vector ADT in PVL by @sakehl in #1156
- Rasi generator by @PBHTasche in #1208
- Add AutoValue by @superaxander in #1207
- VeyMont: channel invariant, stratified expression containers by @bobismijnnaam in #1209
- Fix build on JDK 21+, resolves #1146 by @superaxander in #1212
- Fix crash that can occur after vercors finishes executing by @superaxander in #1213
- Performance improvements by @pieter-bos in #1218
- Shared predicate node 2 by @pieter-bos in #1220
- Only rewrite with knowledge up to now by @sakehl in #1217
- Rasi generator by @PBHTasche in #1221
- Fix protobuf build on CMake 3.30 by @superaxander in #1223
- Middleware by @pieter-bos in #1224
- VeyMont: stratified permissions by @bobismijnnaam in #1210
- Integrate updates to LangCPPParser from the antlr/grammars-v4 repository by @superaxander in #1226
- Remove unused rewrite pass by @superaxander in #1228
- VeyMont: codegen by @bobismijnnaam in #1225
Full Changelog: v2.1.1...v2.2.0
VerCors 2.1.1
What's Changed
- Resolved a rare concurrency bug in the rendering of progress messages in aef15a4
- Restored SysCIR as a dependency in b13e385
Full Changelog: v2.1.0...v2.1.1
VerCors 2.1.0
What's Changed
- Generic parameters java by @Naum-Tomov in #983
- add forperm, polarity_dependent by @pieter-bos in #987
- VeSUV working for now by @PBHTasche in #985
- Framed proof heap values by @pieter-bos in #988
- add perf stats via jna for unix (linux/mac) by @pieter-bos in #978
- Veymont pre by @petravandenbos-utwente in #984
- [VCLLVM] LLVM to COL rewriter for LLVM specific nodes by @Drevanoorschot in #990
- Reorganize by @pieter-bos in #996
- add resourceusage fallback, used immediately in non-unix by @pieter-bos in #997
- [VCLLVM] Add llvm loop and llvm loop contract nodes by @Drevanoorschot in #994
- Nested foralls patch by @pieter-bos in #998
- Nested Quantifiers improvements by @sakehl in #991
- fix Issue 992 by @pieter-bos in #999
- [VCLLVM] Add proper label, goto, and branch support to LlvmFunctionDefinitions by @Drevanoorschot in #1002
- Implement scaling of instance predicates by @bobismijnnaam in #1003
- fix inline triggers with \unfolding by @Naum-Tomov in #1005
- Redo pretty-printing by @pieter-bos in #1006
- allow wand-chunk-not-found as falsity of assertions by @pieter-bos in #1008
- replace :: with +: by @pieter-bos in #1009
- print veymont nodes by @pieter-bos in #1010
- map viper prover types to vercors by @pieter-bos in #1016
- improve loop contract options in pvl by @pieter-bos in #1017
- Add DeserializeOrigin to LLVMOrigin rewriter by @Drevanoorschot in #1007
- Windows build stuff by @pieter-bos in #1020
- update boogie by @pieter-bos in #1024
- bump viper by @pieter-bos in #1027
- [VCLLVM] Deserialize origin "provider" by @Drevanoorschot in #1023
- Add context to VerificationError and print nodes in context by @Naum-Tomov in #1026
- fix #1025 and better inline binding origins by @pieter-bos in #1029
- Smtlib types by @pieter-bos in #1030
- update
realpath
command to be equivalent, osx compatiblereadlink -f
by @Naum-Tomov in #1032 - java version specified explicitly by @Naum-Tomov in #1033
- [VCLLVM] Add function call support for LLVM by @Drevanoorschot in #1036
- Fixes for examples by @ArmborstL in #1037
- Add flag to turn off smart heap inference by @bobismijnnaam in #1041
- Ranged for syntax in PVL by @bobismijnnaam in #1043
- Improve ranged for to not be annoying on use of heap locations by @bobismijnnaam in #1044
- add global heap variables by @pieter-bos in #1047
- [VCLLVM] Add partial contract support for LLVM by @Drevanoorschot in #1034
- Implemented basic C++ support by @Ellen-Wittingen in #1052
- [VCLLVM] Add support for pure functions by @Drevanoorschot in #1049
- Veymont gen par by @petravandenbos-utwente in #1053
- remove the implicit scope of AbstractMethod - should be covered by Scope by @pieter-bos in #1062
- Add the enum reference when an enum constant is resolved by @bobismijnnaam in #1066
- fix #463: consider whether the context is static by @pieter-bos in #1067
- fix #1061: propagate c_e to framedproof by @pieter-bos in #1071
- fix #1050: set git buildinfos for caching properly by @pieter-bos in #1072
- error when this makes no sense in a context by @pieter-bos in #1074
- do not emit permissions for final fields in pvl constructors by @pieter-bos in #1075
- Resolve javabip warnings by @bobismijnnaam in #1073
- fix #1000, fix #749: inline appropriate let bindings in patterns by @pieter-bos in #1076
- Refactor origin add req names by @Naum-Tomov in #1077
- Warnings by @pieter-bos in #1078
- VeyMont: Add communicate statement by @bobismijnnaam in #1079
- Support for SYCL's basic and nd-range kernels by @Ellen-Wittingen in #1070
- fix #1060, actually fix #789: stop all non-daemon threads and timers by @pieter-bos in #1084
- fix #742: yields variables are not referencable in requires/context/c_e by @pieter-bos in #1085
- Improve ci caching by @pieter-bos in #1086
- Refactor origin by @Naum-Tomov in #1089
- Resource values by @pieter-bos in #1087
- Make printing nodes in verificationerrors easier by @pieter-bos in #1091
- VeyMont: refactor SeqProgram into PVLSeqProgram & SeqProgram by @bobismijnnaam in #1090
- bump viper by @pieter-bos in #1093
- VeyMont: resolution improvements by @bobismijnnaam in #1092
- Refactor resolution error to have a more precise error code by @bobismijnnaam in #1098
- VeyMont:
seq_run
,:=
, structure checks and initial sequential program tranformation by @bobismijnnaam in #1095 - VeyMont: seq_prog initialization & permission generation by @bobismijnnaam in #1102
- Added support for SYCL's accessors and declarators. by @Ellen-Wittingen in #1100
- Fixed problems with the Viper (language) support by @OmerSakar in #1105
- Origin cleanup by @pieter-bos in #1104
- warnings by @pieter-bos in #1107
- VeyMont: loop & branch unanimity by @bobismijnnaam in #1106
- VeyMont: full permission generation & auxiliary methods by @bobismijnnaam in #1110
- Better c support by @sakehl in #1059
- Added support for SYCL's local accessors plus minor changes by @Ellen-Wittingen in #1121
- Redo helpers: make a proper meta-model of Node.scala by @pieter-bos in #1118
- add Nele's topological sort to examples directory by @ArmborstL in #1130
- Add ArrayList from Joost Sessink to test suite by @bobismijnnaam in #1131
- Move JavaBIP case study to publications folder by @bobismijnnaam in #1132
- Quantifier triggers are now also processed when they are location by @sakehl in #1124
- VeyMont: reinstate old tests & case studies by @bobismijnnaam in #1114
- More sycl examples and bugfixes by @Ellen-Wittingen in #1126
- perf: fix #1116 by @pieter-bos in #1135
- Fix for #1141 by @sakehl in #1142
- Vcllvm by @pieter-bos in #1144
- Fix bug which caused VCLLVM to get stuck by @superaxander in #1149
- run ci on pull request when forked by @pieter-bos in #1155
- Quick fixes by @sakehl in #1127
- Actually skip backend by @sakehl in #1157
- add syntax for indeterminate branch for pvl by @pieter-bos in #1174
- Fix VCLLVM compilation for the artifact by @superaxander in #1180
- Some fixes for GPUs shared memory by @sakehl in https://github.com/utw...
VerCors 1.4.1
NB: This is a release of backported changes to the v1
branch of VerCors. Please consider using a v2
version where possible. The VerCors executable is renamed to vercors1
to enable installing a v1
version alongside a v2
version.
What's Changed
- Print an error when the language is not specified by @bobismijnnaam in #723
- Add vim plugin (syntax and filetype detection) by @Jesse-Bakker in #737
- Veymont etaps extensions by @petravandenbos-utwente in #727
- Backport backend options flag by @bobismijnnaam in #784
- Add big integer support to PVL by @bobismijnnaam in #726
- Require constructor for lock invariant by @bobismijnnaam in #720
- Partially reinstate problem fail tests by @bobismijnnaam in #658
- Disable casting in parblockencoder by @bobismijnnaam in #660
- Veymont (v1) by @pieter-bos in #972
- Gpgpu optimizations by @pieter-bos in #976
New Contributors
- @Jesse-Bakker made their first contribution in #737
Full Changelog: v1.4.0...v1.4.1
What's Changed
- Print an error when the language is not specified by @bobismijnnaam in #723
- Add vim plugin (syntax and filetype detection) by @Jesse-Bakker in #737
- Veymont etaps extensions by @petravandenbos-utwente in #727
- Backport backend options flag by @bobismijnnaam in #784
- Add big integer support to PVL by @bobismijnnaam in #726
- Require constructor for lock invariant by @bobismijnnaam in #720
- Partially reinstate problem fail tests by @bobismijnnaam in #658
- Disable casting in parblockencoder by @bobismijnnaam in #660
- Veymont (v1) by @pieter-bos in #972
- Gpgpu optimizations by @pieter-bos in #976
New Contributors
- @Jesse-Bakker made their first contribution in #737
Full Changelog: v1.4.0...v1.4.1
VerCors 2.0.0
What's Changed
- The internal data structure for syntax trees was redesigned, making many things more stable and consistent
- Verification failures are translated to more specific errors
- The options were re-done, try
--help
- Various bits of syntax have changed, see also the wiki
- You can introspect the progress of the verification backend in more detail: a report is printed when it is stuck, and see e.g.
--silicon-print-quantifier-stats
New Contributors
- @Jesse-Bakker made their first contribution in #737
- @sakehl made their first contribution in #771
- @PBHTasche made their first contribution in #981
Full Changelog: v1.4.0...v2.0.0
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
VerCors Wiki PDF
This is an automatically generated LaTeX/PDF version of the tutorial on the VerCors wiki.
VerCors 1.3.0
Features
- The webpage code was moved to a different repository
- Added detection for contracts of which the requirements are unsatisfiable
- Added type checking to
jspec
rewriting rules - Refactored the test framework
- Warn users when using integer division in permission values
- Updated viper to release 20.07
- Improve the support for sequences, sets and options in PVL, and add support for Maps, Set comprehension (@OmerSakar)
- Fixed all warnings in the build, greatly improving build time
- Pointers may now be assigned by subscript
- Updated z3 to 4.8.6
- Added various simplifying rewrite rules
- Added support for exceptions and exceptional statements (
break
,continue
) (@bobismijnnaam) - Improved C and GPGPU support: pure methods and functions, ghost statements, CUDA kernel invocations, kernel invariants and atomics
- Improved syntax highlighting for PVL
--version
now outputs better diagnostic information, including the commit- Range syntax was changed from
[a..b)
to{a..b}
- Parsing frontend was redone: specifications are parsed in the first pass and attached in the tree; the parse tree is transformed by destructuring pattern match in Scala
- All expression classes are now case classes, and consequently have structural equality
- Add support for the ambiguous boolean/bitwise operators in Java:
^
,|
and&
- Contracts are attached correctly to labeled loops
- NameScanner was refactored (@bobismijnnaam)
- Pure function application is now allowed in invariants
- The user can be notified of completion of verification with
--notify
- Switched to GitHub Actions
- Added various new examples
Bugfixes
- Fixed a case where the origin of contracts was not preserved
- Fixed that vercors warned about simplification failures in simple quantified statements about arrays
- Fixed an infinite loop in the array encoding
- Map the
Head
operator to Viper again ==>
and-*
are now right-associative- Fixed a case where an expression was extracted to a variable in
flatten
without effect - Some examples that used old backends were refactored to use silicon (@Sophietje)
- Disallow writing to locals in parallel blocks (which caused unsoundness)
- Disallow using
\result
insignals
specifications - Warn that inner classes are not supported, instead of crashing