68 lines
1.8 KiB
Plaintext
68 lines
1.8 KiB
Plaintext
4.3
|
|
===
|
|
|
|
Floating-point arithmetic now takes the rounding mode into account,
|
|
which can be changed dynamically.
|
|
|
|
goto-gcc generates hybrid executables on Linux, containing both machine
|
|
code and the CFG.
|
|
|
|
Limited support for Spec#-style quantifiers added.
|
|
|
|
Pointer-checks no longer use a heavy-weight alias analysis.
|
|
|
|
Limited support for some x86 and ARM inline assembly constructs.
|
|
|
|
|
|
4.2
|
|
===
|
|
|
|
goto-cc now passes all command line options to the gcc preprocessor.
|
|
|
|
The MacOS binaries are now signed.
|
|
|
|
The C/C++ front-end has been tested and fixed for the Visual Studio 2012
|
|
header files.
|
|
|
|
The man-page has been elaborated.
|
|
|
|
Support for the C99 complex type and gcc's vector type has been added.
|
|
Various built-ins for x86 MMX and SSE instructions have been added.
|
|
|
|
Support for various C11 features has been added.
|
|
|
|
Support for various built-in primitives has been added, in particular for
|
|
the __sync_* commands.
|
|
|
|
New feature: --all-claims now reports the status of all claims; the
|
|
verification continues even if a counterexample is found. This feature uses
|
|
incremental SAT.
|
|
|
|
The counterexample beautification (--beautify) now uses incremental SAT.
|
|
|
|
Numerous improvements to SMT1 and SMT2 interfaces.
|
|
|
|
Support for further SAT solvers (PRECOSAT, PICOSAT, LINGELING)
|
|
|
|
|
|
4.1
|
|
===
|
|
|
|
The support for low-level accesses to dynamically allocated data structures
|
|
and "integer addressed memory" (usually memory-mapped I/O) has been further
|
|
improved.
|
|
|
|
Numerous improvements to the SMT back-ends. Specifically, support through
|
|
the SMT1 path for Boolector and Z3 has been improved; support for MathSAT
|
|
has been added. In combination with the very latest version of MathSAT,
|
|
CBMC now also supports an SMT2 flow (use --mathsat --smt2 to activate this).
|
|
|
|
|
|
4.0
|
|
===
|
|
|
|
Better support for low-level accesses to dynamically allocated data
|
|
structures.
|
|
|
|
Numerous front-end improvements.
|