v0.3.0

What's Changed

• Coyote checks what is proved of the concurrent samples by @ashalkhakov in #32
• Entity Framework Core: queries as the database runs them, the change tracker and transactions checked by @ashalkhakov in #33
• A checked build, and Coyote liveness checking of every wait by @ashalkhakov in #34

Full Changelog: v0.2.0...v0.3.0

v0.2.0

What's Changed

• Release: pack and attach the packages to a release made by hand by @ashalkhakov in #10
• Phase 0: the corpus, the library report, stub conformance tests by @ashalkhakov in #11
• Phase 1: check profiles, graceful degradation, Nullable and patterns, null reasons by @ashalkhakov in #12
• Loop facts: infer invariants for loops without any by @ashalkhakov in #13
• Phase 2: null safety for apps by @ashalkhakov in #14
• Phase 5: spans as views of memory, span stubs by @ashalkhakov in #15
• Phase 3: disposables as linear resources by @ashalkhakov in #16
• Phase 4: strings by value, equality-aware contracts, HashSet/Stack/Queue by @ashalkhakov in #17
• List interfaces (reads, writes, foreach by dynamic type); Dictionary TryAdd, capacity, Remove(out) by @ashalkhakov in #18
• Phase 6: lambdas verified as units; eager and lazy LINQ with pure lambdas by @ashalkhakov in #22
• Test the verifier on random programs (after Testing Dafny) by @ashalkhakov in #23
• Merge raises at try handlers (state merging) by @ashalkhakov in #24
• Keep confined objects across await by @ashalkhakov in #25
• Linter benchmark: CsVerify against C# linters (#20) by @ashalkhakov in #26
• Model strings' characters; stop a solver that hangs by @ashalkhakov in #27
• Model shifts and bitwise operators; prove UTF-8 and Base64 by @ashalkhakov in #28
• Add InferSharp to the linter benchmark by @ashalkhakov in #29
• Locks, lock invariants and lock order; fix a soundness bug in specifications by @ashalkhakov in #30

Full Changelog: v0.1.0...v0.2.0

v0.1.0

What's Changed

• CsLemon: Lemon ported to C#, verified, with a validated LR(1) parser and C# output by @ashalkhakov in #1
• CI/CD, packages, verify → erase → Tarp, README split into docs/ by @ashalkhakov in #2
• Verifier: foreach, goto loops, rectangular arrays, ref cells and locals, mutable structs by @ashalkhakov in #3
• Library contracts, BCL contracts, async/await by @ashalkhakov in #8

New Contributors

• @ashalkhakov made their first contribution in #1

Full Changelog: https://github.com/ashalkhakov/CsVerify/commits/v0.1.0