diff --git a/CHANGELOG b/CHANGELOG deleted file mode 100644 index 06fd741315a..00000000000 --- a/CHANGELOG +++ /dev/null @@ -1,225 +0,0 @@ -5.9 -=== -* GOTO-INSTRUMENT: --generate-function-body can be used to - generate bodies for functions that don't have a body - in the goto code. This supercedes the functionality - of --undefined-function-is-assume-false -* The --fixedbv command-line option has been removed - (it was marked deprecated in January 2017) -* GOTO-INSTRUMENT: New option --print-global-state-size - - -5.8 -=== - -* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice - down to a single property only. -* GOTO-INSTRUMENT: New option --list-calls-args -* GOTO-INSTRUMENT: New option --print-path-lenghts -* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions -* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false -* GOTO-INSTRUMENT: New option --remove-function-body -* GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to - --no-system-headers -* GOTO-INSTRUMENT: dump-c can output the generated environment via --harness - - -5.7 -=== - -* General: All tools now support the same set of --*-check options. -* General: Added --conversion-check to catch type casts that cause loss of - information. Previously --(un)signed-overflow-check would report these. -* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible - statement- and branch coverage report. -* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static, - --java-cp-include-files, --lazy-methods. -* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options - --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops, - --continue-as-loops, --log -* GOTO-INSTRUMENT: New option --slice-global-inits -* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline, - --no-caching -* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv, - --show-threaded -* GOTO-CC: Additional drop-in replacement support for bcc, as, as86 -* GOTO-CC: GCC-style error/warning messages -* GOTO-CC: New options --native-compiler and --native-linker to select the - compiler/linker to be used when building combined native/goto object files. -* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed - ambiguous --show-reachable-properties. -* CBMC: New option --no-built-in-assertions - - -5.6 -=== - -Bugfixes in the C, C++, Java front-ends. - - -5.5 -=== - -This is a major release, with significant changes. The option ---all-properties is now the default; to restore the previous behaviour, -use --stop-on-fail. The primary area of attention was again the Java -front-end. We have furthermore added test-suite generation for branch -coverage, location coverage, condition coverage, decision coverage and -MC/DC. - - -5.4 -=== - -This is a minor release, focused primarily on maintenance. The primary -area of attention was again the Java front-end. We have also updated to -Minisat 2.2.1. - - -5.3 -=== - -This is a minor release, focused primarily on maintenance. The primary -area of attention is the Java front-end. - - -5.2 -=== - -This is a minor release, focused primarily on maintenance. The primary -areas of attention are the full slicer, the Java frontend, test suite -generation and support for the Glucose solver. - - -5.1 -=== - -This is a minor release, focused primarily on maintenance. Support for solving -floating-point problems using for SMT-LIB2 solvers without support for the -floating-point theory has been added. - - -5.0 -=== - -This is a major release, focused primarily on performance improvements. -Furthermore, the support for the floating-point theory for SMT-LIB2 has been -improved substantially. This release breaks compatibility with the goto-binary -format used by earlier releases; i.e., you will need to rebuild your -goto-binaries. - - -4.9 -=== - -This release is primarily for maintenance purposes and does not add any major -new features. The support for SMT-LIB2 solvers has been improved substantially. - - -4.8 -=== - - -4.7 -=== - -Added support for Solaris 11. - -Bugfixes in partial-order encoding. - -Added --float-overflow-check - - -4.6 -=== - -Improved floating-point encoding. - -Improved AIG->CNF encoder. - - -4.5 -=== - -Optimizations to reduce memory consumption. - -Bugfixes in partial-order encoding. - - -4.4 -=== - -Now checks concurrent programs, with partial-order encoding. - -Support for SMT-LIB standard floating-point theory. - -goto-instrument knows k-induction and underapproximating loop accelleration. - - -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.