Skip to content

Commit

Permalink
Release 0.10
Browse files Browse the repository at this point in the history
New features:
- array abstract domain (--arrays)
- new loop unwinding for heap-manipulating programs (allows k-induction)
- rebase to CBMC 5.61
- removed necessity of the symbolic paths domain for heap analysis
- various bug fixes
  • Loading branch information
viktormalik committed Jan 25, 2023
1 parent 758ce83 commit 384c20f
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 1 deletion.
5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ Releases

Download using `git clone http://github.com/diffblue/2ls; cd 2ls; git checkout 2ls-x.y`

* [2LS 0.10](http://github.com/diffblue/2ls/releases/tag/2ls-0.10) (01/2023)
* [2LS 0.9](http://github.com/diffblue/2ls/releases/tag/2ls-0.9) (03/2020)
* [2LS 0.8](http://github.com/diffblue/2ls/releases/tag/2ls-0.8) (11/2019)
* [2LS 0.7](http://github.com/diffblue/2ls/releases/tag/2ls-0.7) (08/2018)
Expand Down Expand Up @@ -101,6 +102,10 @@ Since release 0.7:
* Heap abstract domain with intervals or zones: --heap-[intervals|zones]
* Heap abstract domain with intervals or zones and loop paths: --heap-[intervals|zones] --sympath

Since release 0.10:

* Array abstract domain: --arrays

Interprocedural Termination Analysis
====================================

Expand Down
2 changes: 1 addition & 1 deletion src/2ls/version.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,6 @@ Author: Peter Schrammel
#ifndef CPROVER_2LS_2LS_VERSION_H
#define CPROVER_2LS_2LS_VERSION_H

#define TWOLS_VERSION "0.9.6"
#define TWOLS_VERSION "0.10.0"

#endif

0 comments on commit 384c20f

Please sign in to comment.