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 #1177
• Add some simplify quantifiers examples by @sakehl in #1181
• Java system fix by @sakehl in #1185
• RASI Generator by @PBHTasche in #1171

New Contributors

• @Ellen-Wittingen made their first contribution in #1052
• @superaxander made their first contribution in #1149

Full Changelog: v2.0.0...v2.1.0