replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

updated CHANGELOG 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2009 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2013-01-13 12:31:14 +00:00
parent d53dcd89e1
commit a980599f7b
1 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
CHANGELOG
View File

@ -1,4 +1,21 @@
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.
@ -27,7 +44,9 @@ 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
@ -38,7 +57,9 @@ 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.