30-Nov-2016: Astraver Toolset 1.1 released

Astraver Toolset 1.1 comes with the following improvements:

C language support

• Initial support for pointer arithmetic involving nested structures e.g. `container_of' macro from the Linux kernel.
  In particular, the new implementation allows to prove the validity of the pointer to the outer structure obtained by subtracting the offset of the inner structure from the pointer to that structure.

New approach to support modulo arithmetic operations on values of integral C types in ACSL

• The pragma `JessieIntegerModel' for switching between different integer models (e.g. `math', `strict' and `modulo') is no more available. The new integer model integrates `strict' and `modulo' models with per-operation granularity.
• There are new logic operations introduced: +%, -%, *%, /%, and (integral_type %) (a cast).
  They represent the bitwise, i.e. overflowing or modulo arithmetic analogues of the corresponding operations without the %. These operations as well as all bitwise operations (&, |, ~, ^, >>, <<) are now encoded in the theory of fixed-sized bit-vectors.
• The new code annotation /*@%*/ can be used to mark some operation occurring in the C code to be treated as overflowing (performed in the modulo arithmetic) and encoded in the theory of bit-vectors.

Changes to Jessie2

• Split of the Jessie theory and the generated program theory and module. Now there is a separate theory for every axiomatic, every global lemma, each bounded integral type, and many Jessie definitions like pointer, pointer set, allocation table etc. The generated program module is now also separated into several ones, namely one per each code function. The dependencies between theories and modules are computed automatically so that only the theories and modules defining the needed symbols are imported. To import a theory with no used symbol (e.g. a useful lemma), a dummy identically true predicate can be defined and later used.
• Loop invariants are now separated with `&&', which influences behaviour of the split transformation so that previously proved invariants are added to premises when proving the remaining invariants.

Why3 IDE features

• Selected text search in task view.
• A new checkbox in View menu to hide empty theories (with no goals to prove)
  in goals view.

Other differences to the upstream tools see in the previous release announcement.

The current release can be installed either via OPAM or manually built from sources available in our public repositories. All the modifications are published under the licenses applicable to their corresponding original files (or in case of newly created files, the tools they were added to).