File: CHANGELOG

package info (click to toggle)
cbmc 4.9-4
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 40,588 kB
  • ctags: 19,198
  • sloc: cpp: 185,860; ansic: 16,162; yacc: 5,343; lex: 4,518; makefile: 954; pascal: 506; sh: 318; perl: 213; java: 206
file content (103 lines) | stat: -rw-r--r-- 2,336 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
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.