Skip to content

Releases: ftsrg/theta

v2.22.0

11 Aug 06:49
e10eede
Compare
Choose a tag to compare

This release introduces ArrayInitExprs (see release v2.21.0) in the XSTS formalism.

v2.21.0

07 Aug 20:52
e256056
Compare
Choose a tag to compare

This release fixed the ArrayLitExpr expression, and introduces a new ArrayInitExpr expression.

Until this release, arbitrary expressions could be passed to ArrayLitExpr, which only handled LitExpr correctly (e.g. the simplification assumed that only evaluatable expressions are present). This release forbids non-fully-evaluatable expressions in ArrayLitExprs, but introduces ArrayInitExpr which fills the gap by providing support for arbitrary expressions. The grammar does not change, but every initialization expression is compiled into an ArrayInitExpr, which when simplifiable, gets transformed into an ArrayLitExpr.

v2.20.0

07 Aug 20:40
0594693
Compare
Choose a tag to compare

This release brings BigFloat support for the Win64 platform, enabling the use of the floating point type in Theta.
Note the occasional instability of the windows version, detailed in the CFA readme.

v2.19.0

07 Aug 10:36
83b9d4b
Compare
Choose a tag to compare

Floating point types were introduced in v2.18.0, but the MPFR is only available on Linux (currently) so the Windows builds got broken. This release disables float tests on Windows to make the build possible, but of course floats will not be available. Some notes were added to readmes on this.

This release also adds array write syntactic sugar to the XSTS formalism: a[i] := v, which is equivalent to a := a[i <- v].

v2.18.0

04 Aug 19:31
fe8f9c8
Compare
Choose a tag to compare

This release adds support for IEEE-754-compliant floating point arithmetic. It is currently only available for the CFA formalism and only works on Linux due to the availability of the MPFR library.

v2.17.0

01 Aug 14:55
d12a0c4
Compare
Choose a tag to compare

This release adds checks to the CFA to ensure that all locations and variables have unique names. This is required because although in-memory CFAs are fine with having variables/locations with the same name (it can distinguish references), but if we serialize the CFA and try to parse it back, we're gonna have a bad time. This should not break any frontend, but if it does, then probably the frontend's code was relying on a fragile feature and it should be fixed.

v2.16.0

12 Jul 19:40
e82554e
Compare
Choose a tag to compare

This release adds automatic predicate-to-explicit switching strategies for product domains, and fixes havocs for enum variables.

v2.15.0

18 Jun 09:04
202f3c0
Compare
Choose a tag to compare

This release introduces the dedicated prod domain, EXPL_PRED_COMBINED.

v2.14.1

03 Jun 08:35
Compare
Choose a tag to compare

This release fixes a bug in XSTS parsing

v2.14.0

26 May 14:16
53bbe13
Compare
Choose a tag to compare

This release fixes the CI builds by changing the source of the Z3 dependency from bintray to a local jar.