Skip to content

TriCera 0.2
Compare
Choose a tag to compare
@zafer-esen zafer-esen released this 30 Mar 13:42
· 141 commits to master since this release
v0.2
62af517

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).
Assets 3
Loading