May 23rd, 2016
SPARK lemma library for nonlinear int arithmetic
SPARK now comes with a library of lemmas separately proved in Coq, that can be called in user code to automatically prove nonlinear integer arithmetic properties, i.e. properties involving multiplication, division, modulo. The lemmas are ghost procedures, hence they are removed from the final executable when compiling without assertions. This library of lemmas is meant to be extended based on user needs. It is documented in the SPARK User's Guide, in section 4.10 about SPARK Libraries.
May 23rd, 2016
Improved support for arrays with static bounds
CodePeer now performs more accurate analysis of arrays with static bounds and has improved display of dynamically indexed array elements of such arrays.
May 20th, 2016
Elimination of more useless overflow checks at -O2
The compiler now eliminates more overflow checks that can never fail when the optimization level -O2 or above is specified.
QGen User Guide
This is the user documentation for QGen, a qualifiable and tunable code generation and model verification tool for a safe subset of Simulink® and Stateflow® models.
The GNU binary utilities
This is the documentation for GNU Binary Utilities.
The GNU linker
This is the documentation for GNU ld, the GNU linker, part of GNU Binutils.
This is the user manual for GAS, the GNU Assembler, part of GNU Binutils.
Debugging with GDB
This is the main documentation for GDB, the GNU source-level debugger.