v0.4

Overview of Changes

• Added support for an experimental heap model that uses the theory of arrays. The heap model can be changed using the option -heapModel:native (default) and heapModel:array.

• Added an option to change solution reconstruction in Eldarica -solutionReconstruction:wp (default) and -solutionReconstruction:cegar. The CEGAR version leads to much smaller solutions in many cases, which is planned to be the default option in the future.

• Migrated the codebase to Scala v2.13.

Included PRs

• Upgrade project to Scala v2.13 by @zafer-esen in #48
• Switch to new heap interface methods by @zafer-esen in #50
• Add capabilities for nondeterministic array initialization. by @woosh in #44
• Change to default sbt directory structure by @zafer-esen in #45
• Adds support for statement expressions and assert.h assert macro by @zafer-esen in #46
• Add test case for -mathArray with struct array by @woosh in #49
• Update at expressions so that first argument is a string containing a label by @zafer-esen in #51
• v0.4 release by @zafer-esen in #54
• Changes to Symex LHS evaluation by @zafer-esen in #41

Full Changelog: v0.3.2...v0.4

v0.3.2

What's Changed

• Introduce result class by @woosh in #26
• ACSL stackpointer support by @woosh in #29
• Fix for shadowed global variables. by @woosh in #33
• Refactor CCReader by @zafer-esen in #38
• Update Eldarica version to v2.2 and changes to contract translation by @zafer-esen in #39
• Support for at expressions by @zafer-esen in #40

Full Changelog: v0.3.1...v0.3.2

TriCera version 0.3.1

What's Changed

• Theory of heaps translation contributed by @OskarSoderberg and @woosh in #13
• Fixed -logSimplified and -logSimplifiedSMT options, which weren't working at all.
• New -dumpSimplified option. Dumps clauses in SMT-LIB format after running Eldarica's preprocessors (similar to -dumpClauses which dumps them before any preprocessing).
• Reduced the amount of emitted warning messages for functions without bodies.

Full Changelog: v0.3...v0.3.1

TriCera version 0.3

• TriCera now supports symbolic execution using the option -sym. See CLI help for more related options.
• ACSL parser and translator improvements - details at #7.
• Better handling of properties - details at #10.
• Improved presentation of counterexamples and assertions that fail with exact line numbers and failed properties - counterexamples can also be visualized using the option -eogCEX.
• New -cpp option for calling the C preprocessor prior to TriCera (not to be confused with TriCera's own preprocessor triPP).
• Add support for interpreted predicates, with examples under regression-tests.

Full Changelog: v0.2...v0.3

TriCera 0.2

TriCera now uses the theory of heaps to encode heap operations. This version adds support for a larger subset of the C language, including partial support for C arrays and pointer arithmetic over pointers to arrays.

The accompanying pre-processor (tri-pp) greatly increases the range of supported programs, but currently only works on Linux. The script triNoPP can be used instead of tri to run the tool without the pre-processor on other systems.

Additional features:

• Preliminary support for parsing ACSL function contracts (credit to Pontus Ernstedt), see regression-tests/acsl-* for example programs.
• Automatic inference of some ACSL annotations when the program is safe. Function contracts are generated for functions annotated with /*@contract@*/, and loop invariants are generated for all program loops when the option -inv is passed. The generated annotations can be printed using the -acsl option.
• Support for specification of uninterpreted predicates, see examples under regression-tests/uninterpreted-predicates.
• Many new options are added (see program help), and some broken options should now work (notably -sol and -ssol for printing solutions).

TriCera 0.1

First release after separating the C front-end of ELDARICA as TriCera. This release features new support for stack pointers, basic heap support and C structs. C arrays and pointer arithmetic is not supported.