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 compatible readlink -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 in signals specifications
• Warn that inner classes are not supported, instead of crashing