Newer
Older
statuses (e.g. True, then Unknown, then True) are now reported
in the console.
o! Kernel [2015-12-09] API change for function Alarms.register. See .mli
for details.
- Cil [2015-10-09] Add support for parsing digraphs.
o! Cil [2015-10-09] Buggy record Cil.miscState has been removed.
Customization must be done directly in Cil_printer.state.
- Value [2015-09-30] Better precision for calls through function pointers
when multiple functions are possible. The abstract state now
contains the information of which function was called.
o! Value [2015-09-20] Functions filter_le_ge_lt_gt_* have been renamed
into backward_comp_*. Evaluation and reduction functions
for comparisons now use and return dedicated types, in
Abstract_interp.Comp.
- Cil [2015-09-20] Double pointer casts on the NULL pointer are now
simplified.
-! Cil [2015-09-20] Typing within comparisons is now more strict,
or made more explicit through casts.
- Kernel [2015-09-20] The untyped AST is no longer removed by basic program
transformations such as loop unrolling.
o Ptests [2015-07-29] New EXEC: directive.
- Kernel [2015-07-01] New options -then-last and -then-replace.
- Kernel [2015-07-01] New option -remove-projects.
- Kernel [2015-06-30] New option -set-project-as-default.
#############################################
Open Source Release 12.0 (Magnesium-20151002)
#############################################
o! Kernel [2016-01-03] Modules Dataflow is deprecated, and will be removed
in Aluminium. Module Dataflow2 offers a very similar but simpler
API.
- Doc [2015-11-16] Fixed typo in the manual (Thx Mihaela Sighireanu).
-* Kernel [2015-10-12] Fix clearing of old statuses and hypotheses when a
new status is emitted or an annotation is removed.
-* Libc [2015-09-29] Removed obsolete file machine.h (along with other
similar files) from the Frama-C share folder. Fixes bug #2171
-! Kernel [2015-09-07] Removed support for OCaml 3.12.1
- Value [2015-09-03] Assertions containing \at(P, L), where L is a C
label, can now be evaluated. Evaluation is done once Value has
run; thus, it ignores option -slevel.
-* Value [2015-09-03] pointer_comparable alarms are now emitted with
arguments properly cast to void* or void (*)().
- Value [2015-08-10] The alarms raised when evaluating a global
initializer that leads to an undefined behavior are now marked
with an "Invalid" status.
- Report [2015-08-10] Reports in csv format now honor option
-report-specialized (previously, preconditions at a
callsite were always skipped).
-* Libc [2015-08-26] Fix bug in the specifications of readir, opendir,
closedir and fopen functions, that would cause incorrect analysis
in -lib-entry-mode.
- Gui [2015-08-14] When a call statement is selected, the statuses of
the preconditions of the called functions are displayed in the
'information' panel.
o! Gui [2015-08-14] Minor API changes regarding Design.reactive_buffer.
Some values that used to have an option type are now guaranteed
to be present.
- Gui [2015-08-12] Internal ids (for statements, code annotations, etc.)
are now hidden by default. Start the GUI in debug mode if you want
to see them.
-* Gui [2015-08-10] Filenames in the GUI file tree (top-left panel)
are now sorted correctly. Fixes bug #2173.
-! Value [2015-08-03] WIDEN_HINTS directive are now cumulative with
automatically inferred bounds. Fixes bug #876.
-* Cil [2015-08-03] Fix bug #1553, related to nested initialisations
of structures containing pointers.
-! Value [2015-08-03] All plugins that depend on Value, plus Value itself
are now dynamic. Custom plugins must specify in their Makefile the
plugins they depend on (e.g. PLUGIN_DEPENDENCIES:=Inout Value).
-* Cil [2015-07-29] Cil transformation can introduce assertion to ensure
that size expressions in an array declarations evaluated at
program execution time are positive and do not overflow.
o Ptests [2015-07-29] New LOG: directive.
- Value [2015-07-19] Garbled mix origins now include at most one source
location.
- Report [2015-07-19] New option -report-proven to control the display
of proven properties.
- Report [2015-07-19] New export format (.csv), through option -report-csv.
o! Callgraph [2015-07-16] Remove Cil.Callgraph, Db.Syntactic_callgraph and
Db.Semantic_callgraph which are all replaced by the single
plug-in Callgraph. See Changelog_detailled.md for further detail
about this change.
-! Callgraph [2015-07-16] New plug-in callgraph which merges the old
Syntactic_callgraph and Semantic_callgraph plug-ins (now
removed). Either this plug-in uses Value if already computed, or
computes the syntactic callgraph otherwise. This new plug-in
unifies the behavior of its two ancestors. In particular,
the edges of callgraph computed with the help of Value are
now directed in the same way as the syntactic callgraph (was
reversed before) and so the computed services are now
equivalent. Also, the uncalled functions are now displayed
by default. For plug-in developers, the callgraph is easily
accessible via an API (bts #755).
-! Value [2015-07-14] Float operations that are guaranteed to lead
to +/-infty (e.g. x = FLT_MAX*10.) now stop propagation.
Previous behavior was to continue with an imprecise value for x.
- Kernel [2015-07-09] New option -custom-char-annot for changing the
character introducing ACSL annotations (instead of '@').
- Value [2015-07-09] Do not emit pointer_comparable alarms on valid
pointer comparisons involving objects of size 0.
- Value [2015-07-07] The semantics of copying a lvalue has been changed
when a type mismatch occurs between the destination and the copied
value. A bitwise reinterpretation of the value to the destination
type is now performed during the copy.
o! Kernel [2015-07-01] Ival.Float_abstract renamed to Fval.
Fval.inject_r now may raise Fval.Non_finite instead of the old
Float_abstract.Bottom.
- Value [2015-06-29] Option -val-split-return-auto now always split
between NULL/non-NULL pointers.
-* Value [2015-06-26] Check the validity of the operands of the ACSL
operators /, %, << and >> when evaluating a predicate.
o! Value [2015-06-25] Remove duplicate values Ival.singleton_zero and
Ival.singleton_one. Use script sodium2magnesium.sh for automatic
migration.
-* Parsing [2015-06-22] Black-list gcc's builtin macros for logic
pre-processing to avoid warnings for duplication. Fixes bug #2161.
-* Logic [2015-06-15] Fix typing bug when converting into a term an
expression containing a pointer subtraction.
-* Value [2015-06-09] Pointer comparisons using relational operators (<,
>=, etc) between a pointer and NULL is now flagged as undefined.
o! Kernel [2015-06-09] Remove support of plug-ins without .mli.
Fixes bug #!1825.
-* Cil [2015-05-29] Better typing of '?' operator. Fixes bug #2117.
o! Kernel [2015-05-29] Remove long-obsoleted functions Cfg.computeCFGInfo
Cfg.printCfgFilename, and Cfg.printCfgChannel.
- Value [2015-05-28] Functions call using a function pointer are now
treated more leniently when too many arguments are supplied. An
alarm is emitted, but execution continues with the right number
of arguments.
- Value [2015-05-12] Improved reduction by predicate \initialized when
the left argument is a range of locations.
- Impact [2015-05-12] Removed function Db.Impact.slice, that was actually
unrelated to Impact. You can use the functions contained in
Db.Slicing.Select, in particular Db.Slicing.Select.select_stmt,
to obtain the same result.
- Makefile [2015-05-06] Dynamic plug-ins are now declared as Findlib
packages. Use variables PLUGIN_REQUIRES and PLUGIN_DEPENDENCIES.
Loading a plug-in automatically loads all necessary dependencies.
Plugin "MyPlugin" is register under "frama-c-myplugin" package.
-! Kernel [2015-05-06] Dynamic now rely on Findlib. Small changes in API.
Option -load-module can now load any Findlib package and its
dependencies as well.
- Kernel [2015-05-06] Reformulated help messages.
Option -help is more concise.
Option -version only prints version number.
Options -print-xxx uniformized.
New options -plugins, -print-config.
- Value [2015-05-29] Added built-ins for mathematical functions: atan2,
fmod, pow, expf, logf, log10f, powf, sqrtf, floor, floorf,
ceil, ceilf, round, roundf, trunc, truncf.
-* Value [2015-05-03] In -lib-entry mode, allow the generation of initial
states with 0-sized bitfields.
-* Metrics [2015-05-05] Fix computation of global cyclomatic complexity.
Fixes bug #!2089.
-* Libc [2015-04-29] Added ACSL specifications to some standard library
functions, including read, write and realloc. Fixes bug #1939.
- Scope [2015-04-22] Assertions previously removed by
-remove-redundant-alarms are now marked as proven, but remain in
the AST.
- Value [2015-04-22] New GUI panel 'Values', that displays nearly all the
information previously available under the 'Information' panel.
-* Logic [2015-04-14] Correct handling of string and char constant in
logic pre-processing. Fixes bug #2101.
-* Logic [2015-04-14] Better overloading resolution.
Fixes bug #2098.
o! Logic [2015-04-08] Functions Db.Properties.Interp.lval and
Db.Properties.Interp.expr have been renamed (into term_lval
and term, respectively), and have a new signature.
-* Cil [2015-04-19] Fix parsing of packing directives of the form
'#pragma pack(push, N)'.
-! Value [2015-04-13] In -lib-entry mode, functions pointers no longer
force the generation of dummy functions. Instead, they are
initialized to NULL. Fixes bug #!2104.
- Kernel [2015-04-01] New API for backward dataflow propagation in file
Dataflows.
- Metrics [2015-03-25] New category 'Extern global variables', that can
be used to check whether some files are missing.
- Metrics [2015-03-24] Functions from Frama-C standard library are now
hidden by default.
-* Cil [2015-03-26] Switch statements in which some cases are not
constant expressions are now completely disallowed, as per the
C standard.
-* Cil [2015-03-21] Disallow all incomplete types for struct fields
Fixes bug #!1672.
-! Cil [2015-03-21] Parsing no longer accepts structures containing
incomplete types. Fixes bug #!2091.
- Kernel [2015-03-24] Special functions CEA_ have been removed.
-! Libc [2015-03-19] Most .c and .h files under /share have been merged
into /share/libc. Inclusions of builtin.h should be replaced by
__fc_builtin.h.
- Kernel [2015-03-18] New ACSL predicate \valid_read_string in
share/libc/__fc_string_axiomatic.h.
-! Value [2015-03-12] Terms involving l-values that are bit-fields are now
correctly handled.
- Cil [2015-03-19] Fix incorrect simplifications of '!E' to 0 when
E is either an enum with value 0 (bug #2090), or an expression
whose value wraps.
-! Kernel [2015-03-17] Removed option -no-dynlink.
- Kernel [2015-03-10] macro __FRAMAC__ is defined when pre-processing
C files in Frama-C.
o! Kernel [2015-03-10] AST change: split GVarDecl into GVarDecl and GFunDecl
o! GUI [2015-04-04] Constructor Pretty_source.PTermLval now has an
additional argument, the property in which the term appears.
- Defs [2015-04-04] L-values for which defs are queried are now evaluated
only for the callstacks that are currently active, resulting
in possibly less locations.
-! Value [2015-03-08] Fix bug in -memexec-all option in presence of
instructions where evaluation was guaranteed to fail.
-! Inout [2015-03-08] The inputs of an instruction whose evaluation always
fail include the sub-expressions for which evaluation succeeds.
- Kernel [2015-02-26] Added -no-tty option to disable terminal capabilities
- Value [2015-02-23] Faster treatment of imprecise struct copying and
left shifts in the logic.
o! Kernel [2015-02-22] Function Integer.two_power now raises an exception
for overly big arguments.
- Kernel [2015-02-20] Add new suffix '.ci' for pre-processed files
containing ACSL annotations to be pre-processed.
-! Value [2015-02-18] In synthetic results, for local variables that are
not those of the current function, the approximated values
encompass only the callstacks for which the variables were
in scope in one of the callers.
- Value [2015-02-18] Local variables that are in scope but not yet
initialized are now present in the environment.
-! Value [2015-02-15] Option -subdivide-float-var has been renamed into
-val-subdivide-non-linear, and has now an effect on non-linear
integer expressions.
o! Value [2015-02-15] Removed function Cvalue.V.min_and_max_float. Use
Cvalue.V.project_ival and Ival.min_and_max_float.
- Cil [2015-02-11] Function Printer.change_printer now allows composing
printers, and is called Printer.update_printer.
- GUI [2015-02-11] Variables are now left- and right- clickable in
the 'information' panel.
- Value [2015-01-31] Improved reduction by assertions of the form
\initialized(&t[0..N]) when N is above -plevel.
o! Kernel [2015-30-01] Fixed bug #!2012 about combining
Ast.is_last_decl and Kernel_function.get_global.
- Value [2015-01-26] New option -val-initialization-padding-globals to
specify how padding bits should be initialized. Option
-initialized-padding-globals is deprecated.
-* Value [2015-01-26] Fix initial state in which some volatile qualifiers
for nested types were ignored.
-* Value [2015-01-26] Fix incorrect initialization of padding bits.
Option -initialized-padding was ignored in some cases.
-* Cil [2014-01-26] Fix iterators on C99 designated initializers.
- Value [2015-01-26] Improvements to option -subdivide-float-var, when
subdividing may avoid the emission of an alarm.
- Value [2015-01-21] Support for \subset predicate.
##########################################
Open Source Release 11.0 (Sodium-20150201)
##########################################
- Kernel [2015-02-01] Tests are added to the distrib (make tests).
-* Logic [2015-02-09] The ACSL parser accepts qualifiers in logic C types.
- Value [2015-01-07] Special functions CEA_ are deprecated. Use
Frama_C_show_each or Frama_C_dump_each instead.
- Kernel [2014-12-28] Improve pretty-printing of some loops.
-* Kernel [2014-12-16] -load-module M now works fine if M uses the API
of another plug-in (bts #!1824).
-! Cil [2014-12-09] Default preprocessing command now includes Frama-C's
standard library, and when possible sets option '-nostdinc'.
See options -frama-c-stdlib and -cpp-gnu-like.
*! Cil [2014-12-09] Variables __FC_MACHDEP_FOO_BAR are now automatically
positioned when setting a non-standard machdep and using Frama-C's
standard library.
- Cil [2014-12-09] Option -pp-annot should be much faster when parsing
files with many ACSL annotations.
- Logic [2014-11-28] The ACSL parser now ignores /*@{ and /*@} comments,
to avoid conflicting with Doxygen.
- Value [2014-11-10] Accesses to locations that contain garbled mix now
cause the garbled mix to be reduced to the set of valid locations.
- Value [2014-11-07] Accesses to '*(foo *)p' may now reduce p according
to the validity of the access, when useful.
- Value [2014-11-07] Removed message "assigning non-deterministic
value from the first time".
- Value [2014-10-28] Option -slevel-merge-after-loop renamed to
-val-slevel-merge-after-loop. Now takes a set of kernel functions
as an argument.
- Value [2014-10-24] Per-callstack results are now always computed.
Option -val-callstack-results is deprecated.
- From [2014-10-24] New option -from-verify-assigns to give assigns/from
clauses of function with bodies a validity status.
-! Value [2014-10-24] Logic ranges are now evaluated using a dedicated
lattice. Results are almost always more precise, and the analysis
faster.
-* Kernel [2014-10-23] allow dynamically loaded module to start with a
lower-case letter. Fixes #1276.
-* Value [2014-10-15] Improved precision for variables that are reduced
(but not written) during a call memorized by option -memexec-all
- Value [2014-10-15] Indeterminate bits copied when option
-val-warn-copy-indeterminate is active now cause a reduction in
the source location.
- Value [2014-10-15] Arguments of functions that give rise to an alarm
are now reduced when possible.
- Value [2014-09-26] Reduce arguments of a function according to the
possible values of the formal at the end of the call.
- Value [2014-09-26] Better precision when a scalar value is written
through a garbled mix.
o! Value [2014-09-26] Remove experimental support for periodic bases.
-* Value [2014-09-25] Fix bug when writing precise values at too many
locations in packed arrays.
-* Value [2014-09-19] When for missing '\from' clause for '\result' when
result is used in a postcondition. Fixes bug #1908.
o! Value [2014-08-29] Garbled mix (constructor Top in modules
Location_Bits/Bytes) now explicitly mention the NULL base.
- Kernel [2014-08-15] New option '-then-last', which behaves like
'-then-on' on the last project created by a program transformer.
-* Value [2014-07-27] Text-only alarms that used the '\defined' predicate
(to warn about dereferencing pointers to out-of-scope variables)
are now emitted with the '\dangling_contents predicate.
- Logic [2014-07-27] The ACSL predicate '\specified', which has been
renamed to '!\dangling_contents' is now supported.
o! Value [2014-07-22] Value 'empty' is no longer exported in module
Offsetmap. The API should prevent any accidental creation.
- Inout [2014-07-22] Remove undocumented option -access-path
o! Value [2014-07-22] Most iterators of module Lmap and Cvalue.Model
now accept only the non-bottom and non-top cases.
o! Value [2014-07-22] API of module Cvalue.V_Or_Uninitialized is now
type-safe. Replace all occurrences of 'get_flags v' by 'v'.
o! Value [2014-07-22] Improve and clarify the return conventions of modules
Offsetmap, Lmap, Cvalue.V_Offsetmap and Cvalue.Model, by returning
three cases: `Bottom, `Top and `Map. The latter case indicates
the operation succeeded precisely'.
o! Value [2014-07-22] Functions find_base and find_base_or_default in
modules Lmap and Cvalue.Model now return an optional type, to
account for invalid bases (that may not be present in the map).
o! Value [2014-07-22] Some functions of modules Offsetmap, Lmap,
Cvalue.V_Offsetmap and Cvalue.Model now require a separate
Locations.Location_Bits.t and (integer) size, instead of a
Locations.location. This avoids errors when the case was
Int_Base.Top.
o Value [2014-07-22] Argument ~conflate_bottom to Cvalue.Model.find is now
optional. The documentation has been updated to better explain its
meaning.
- Value [2014-07-22] Message 'extracting bits of a pointer' is no longer
emitted, as it was redundant with the warnings about garbled mix.
-* Value [2014-07-22] Fix evaluation of '/' in the logic, that silently
ignored the presence of the value 0 in the divisor.
- Value [2014-07-22] The arguments of an invalid shift operation are now
reduced so that they belong to the proper range.
o! Value [2014-07-22] Multiple low-level functions have been removed from
modules Cvalue.V and Cvalue.Model, and are no longer available.
o! Value [2014-07-22] Function Cvalue.Model.find does *not* signal its
result is indeterminate anymore. Use function
Cvalue.Model.find_unspecified instead.
o! Value [2014-07-22] Major API change in directories src/ai and
src/memory_state. Functions no longer take ~with_alarms arguments.
Instead, they return booleans, that indicate an alarm occurred.
- Value [2014-07-22] More systematic emission of message 'operation [...]
incurs a loss of precision', signaling an arithmetic operation
on a pointer address. This message is now emitted by Value itself.
-! Kernel [2014-07-09] New way to handle command line options which
accepts sets of values. Values may be prefixed by '+' or
'-' to add/remove them and categories of values prefixed by
'@' are available as well (for instance @all).
o! Kernel [2014-07-09] A new bunch of functors are available to
define command line collections.
o! Cil [2014-07-03] Field 'vgenerated' of type Cil_types.varinfo has
been replaced by the field 'vtemp' to emphasize the fact that
it should only be set to true for temp variables generated
during elaboration.
o Cil [2014-06-27] Variables are created with a field 'vgenerated' set
to 'false' by default. Only Cil should position this field to
'true'.
o! Cil [2014-06-27] The field 'vlogic' of type Cil_types.varinfo has
been replaced by the field 'vsource', to avoid confusion with
logic variables. The value of the new field is the negation of
the previous one.
-! Cil [2014-06-17] Frama-C's x86 default machdeps no longer assume that
the compiler is GCC. Some typing extensions and builtin are thus
deactivated. If you want a GCC-centric analysis, use the
gcc-prefixed machdeps.
o! Cil [2014-06-17] Modifications in some fields of type Cil_types.mach.
Function File.new_machdep has a simpler type.
- Value [2014-06-17] Option -val-split-return can now be used to split
between NULL / non-NULL pointers
- Kernel [2014-06-16] New option -const-readonly (set by default), that
asserts that 'const' variables must never be written.
- Logic [2014-06-16] New logic label "Init", that refers to the state
just after the initialization of globals.
- Cil [2014-06-16] Values extracted from initializers of const variables
are now accepted as arguments of directives pragma loop UNROLL.
- Logic [2014-06-16] New builtin functions \min and \max of type
Set(Integer) -> Int
- Semantic Constant Folding [2014-06-12] Reducing the number of introduced
casts; feature #!1787.
- Value [2014-06-07] Improve conversion of float values that have been
written as integers (through low-level memory accesses)
- Value [2014-06-06] Improved pretty-printing of variables containing
pointers.
-* Makefile [2014-06-05] Do not install ZArith with Frama-C anymore.
o* Makefile [2014-06-05] Fixed compilation bug for plug-ins with both a
GUI and a non-empty API (bug #!1798).
- Value [2014-06-01] Improved widening on variables that are used to
access an array
- Value [2014-05-27] The GUI now showns the value of logic l-values
inside function specifications. They are evaluated in the
pre-state of the function, before the evaluation of preconditions.
o Gui [2014-05-27] Logic l-values inside function specifications can
now be selected
* Slicing [2014-05-23] Fix issues about slicing calls to the main function
and journalization (bug #!1684).
- Kernel [2014-05-22] Nicer error message in case of code
incompatibility when loading a plug-in.
-* Kernel [2014-05-15] Fix bug #1765 (spelling errors).
-* Slicing [2014-05-14] Fix crashes about multiple slicing pragma inside a
function (bug #1768).
- Report [2014-04-07] New option -report-callsite-preconditions.
- Report [2014-04-07] More consistent behavior when option -report-untried
is not set.
- Report [2014-04-07] Better reporting of reachability statuses; do not
coalesce unproven reachability assertions with other alarms.
- Value [2014-04-05] When option -val-callstack-results is set, the GUI
now displays a callstacks-wide consolidation of the possibles
values for expressions and terms. Previously, the potentially
less precise summary state was used.
- From [2014-04-05] Major performance improvements on big analyses.
-! Value [2014-04-05] Complete rewrite of the modules Int_Intervals and
Offsetmap_bitwise; both are now implemented with the same
datastructure as Offsetmap. Many performance improvements.
Many changes in the API of module Offsetmap_bitwise. Few changes
in Int_Intervals, but the englobing module Lattice_Interval_Set
has been removed.
- Gui [2014-03-27] New option -gui-project to run the GUI in a
given project.
- Semantic Constant Folding [2014-03-25] Reducing the number of introduced
casts; feature issue #!1697.
- Semantic Constant Folding [2014-03-25] New option -scf-project-name.
o! Cil [2014-03-24] The ikind for Cil.kinteger64 is now optional.
- Value [2014-03-20] File-scope and formal const variables are read-only.
Any possibility of writing there is treated as alarm.
-! Gui [2014-03-14] C expressions can now be selected through the source
-* Cil [2014-03-13] Fix erroneous integral promotion of type 'char' on
architectures where 'char' is unsigned.
- Semantic Constant Folding [2014-03-13] Generate nicer constants for integers
and pointers
- Semantic Constant Folding [2014-03-13] Floating-point constants can now
be propagated.
-* Semantic Constant Folding [2014-03-13] Fix crashes and/or multiple declations
when a global was referenced in the constant-folded project
earlier than in the original one.
- Value [2014-03-12] Improve precision of &.
o Logic [2014-03-04] Annotations.{iter,fold}_all_code_annot are now
by default sorted. Use ~sorted:false in case of efficiency issues.
-* Value [2014-03-02] Dividing an integer value by a memory address
requires the address to be comparable to NULL.
- Value [2014-03-02] Alarms are now re-evaluated at the end of the
analysis. If their truth value is 'Valid' or 'Invalid', this more
precise status is used, instead of the previous 'Unknown' one.
- Value [2014-03-01] Preconditions of functions that are never called are
now also marked as dead at each call-site.
- Rte [2014-03-01] Very big floating-point constants that are converted
to an integer are now reported as overflowing in only one
direction
- Value [2014-03-01] Alarms when converting integers to floating-point
are now reported only for the range that overflows
- Value [2014-03-01] Instructions whose execution is guaranteed to fail
are now displayed in the GUI
- Value [2014-03-01] Option -val-after-results is now always active by
default, and can no longer be unset
-! Kernel [2014-05-12] require ocamlgraph version 1.8.5
- Kernel [2014-08-07] add instructions for downloading the manuals
-* Configure [2014-03-17] use the gcc from the configure for compiling c files
-* Configure [2014-03-10] fix for autoconf < 2.67 when checking ability
of default pre-processor to keep comments
########################################
Open Source Release 10.0 (Neon-20140301)
########################################
-* Value [2014-03-04] Fix bug when writing imprecisely in a struct
containing a 1-bit wide bitfield (bug #!1671)
-* Kernel [2014-02-18] Fix -machdep help in presence of other actions
(bts #1643).
+* Logic [2014-02-05] Better handling of sets. Use Tlogic_coerce to
explicitly mark conversion from singleton to set.
- Kernel [2014-02-04] Assigns clauses generated by the kernel for functions
with neither a specification nor a body receive an 'Unknown'
status.
- Value [2014-02-05] For functions for which only the specification is
available, non-invalid statuses are no longer reported when
evaluating a postcondition. Invalid statuses are reported, and
usually indicate a specification error.
-* Kernel [2014-02-05] Fix typing of variadic arguments.
- Configure [2014-02-05] New option --disable-local-ocamlgraph to
disable the use of the OcamlGraph version provided by
Frama-C.
-* Value [2014-02-04] Fix potential unsoundness in the operation testing
the inclusion of two memory states (never observed in practice)
o! Kernel [2014-02-03] The module Parameter_state now contains the
functions to select group of parameters (was in module Plugin).
o! Kernel [2014-02-03] The module Parameter_customize now contains the
functions to customize command line options (was in module
Plugin).
o! Kernel [2014-02-03] Parameter is now called Typed_parameter.
o! Kernel [2014-02-03] The module Parameter_sig now contains the
signatures of command line options (was in module Plugin).
- Kernel [2014-02-03] FRAMAC_PLUGIN may now specify a list of
comma-separated directories instead of a single one.
o* Logic [2014-01-30] Better specification and more checks on
Annotations.{add,remove}_* functions (fixes bug #!1635).
o! Kernel [2014-01-29] Changes to the signatures in lattice_type: top and
bottom are now optional, a join_and_is_included function is
required, and Upper_Semi_Lattice was renamed to Join_Semi_Lattice.
-* Value [2014-01-25] Remove support for ACSL \inter operator, which could
lead to unsoundness with predicates involving the empty set
(fixes bug #!1624)
- Value [2014-01-25] Fix spurious messages about integer overflow when an
arithmetic operation is guaranteed to result in an undefined
behavior.
o! Kernel [2014-01-21] Removed Db.Dominators. Use the Dominators kernel
module instead.
-* Value [2014-01-18] Fixed spurious warning about floating-point values
containing addresses.
-* Kernel [2014-01-18] Fixed parsing bug with decimal single-precision
floating-point literals representing numbers above MAX_FLOAT.
-! Value [2014-01-16] Replace mostly-inoperant option -memory-footprint
by an environment variable FRAMA_C_MEMORY_FOOTPRINT
o Ptests [2014-01-16] Use ptests.opt whenever possible.
o! Kernel [2014-01-14] For building a datatype, you now need to use
smart constructors provided in Structural_descr.
-* From [2014-01-11] Fix incorrect dependencies with code of the form
'f(); x = 1; f();' when f assigns a value with a right-hand side
that depends on x.
-* Value [2014-01-11] Fix missing read/written zones and dependencies when
accessing a completely imprecise pointer (garbled mix) and using
option -absolute-valid-range. Impacts the results of plugins
Inout, From, Pdg, Impact and Slicing.
o! Value [2014-01-08] Harmonisation and simplifications of functions
related to memory states in Cvalue.Model. Different functions
are now available for updating, refining and creating a state
-* Value [2014-01-07] Fix crash on analyses involving very imprecise
pointers and a partially valid absolute memory range
-* Cil [2014-01-06] Fixes issue #1589 (do not drop access to volatile
lvals in pure expressions).
- From [2014-01-01] Fix possibly invalid dependencies for functions
that return partially-written structs.
o Kernel [2013-12-23] Plug-ins may now have a non-empty .mli interface.
It deprecates the old way to register them through module Db
or Dynamic (this last one may remain useful for mutually
recursive plug-ins).
-* Value [2013-12-23] Fix possible unsoundness in presence of &.
(unsoundness never observed in practice)
- Value [2013-12-23] Improve precision of treatment of x = e1 & e2;
- Value [2013-12-23] Improve precision of treatment of:
if ((int)floatvar == intexpr)
- Value [2013-12-13] Ensure convergence in presence of some non-natural
-* Cil [2013-12-12] Do not pretty-print while(1) into while(c) when
the 'break' branch is not reduced to a single break, or contains
an annotation
-! Syntactic_callgraph [2013-12-10] Remove option -cg-services-only which
was unused since a while.
-* Value [2013-12-09] Fix rare crash during widening operation in
C union intensive code
-* Value [2013-12-03] Fix potentially invalid source line number in origin
of Merge garbled mix values.
- Value [2013-12-03] Display information about temporaries when emitting
- Kernel [2013-12-03] "-machdep help" now specifies the default
machdep (bts #!1558).
- Obfuscator [2013-12-03] New option -obfuscator-string-dictionary to generate
the dictionary of literal strings into a separated file.
- Obfuscator [2013-12-03] New option -obfuscator-dictionary to generate
the dictionary into a file.
-* Kernel [2013-12-03] Fix bug which may occur when pretty printing
range of terms.
- Obfuscator [2013-12-03] Warn about unobfuscated symbols.
- Obfuscator [2013-12-03] Handle literal strings in a separate dictionary
(bts #!1564).
-* Obfuscator [2013-12-03] Now properly handle option -ocode.
- Obfuscator [2013-12-02] Obfuscate (most of) logical constructs (bts #1563).
- Obfuscator [2013-12-02] Obfuscate labels (bts #1562).
- Obfuscator [2013-12-02] Print the category which each symbol belongs to
(bts #!1566).
-! Value [2013-12-01] Volatile pointers are now modeled as the base
addresses that are stored into the pointer, shifted by an
unspecified offset.
o! Value [2013-11-28] Functions previously required by some functors in
directories src/ai and src/memory_state are no longer needed.
Use script bin/fluorine2neon.sh for partially automatic migration.
- Scope [2013-11-27] Option -inout-callwise can be used to improve
the precision of computations, including the effects of option
-remove-redundant-alarms. Option -calldeps is no longer necessary
- Value [2013-11-27] Experimental option -slevel-merge-after-loop
- Value [2013-11-25] Improve precision of bitwise conversion from
floating-point value to integers
-* Value [2013-11-22] Ensures that sqrt(-0.) is -0., even with buggy
MSVC runtime. Fixes bug #!1396
- Kernel [2013-11-20] Support for binary literal constants in C and
in logic denoted by '0[bB][01]+' (common ISO/C extension).
- Value [2013-11-14] Copies of non-struct left-values that contain
indeterminate bits can now be reported using option
-val-warn-copy-indeterminate.
-! Value [2013-11-14] Passing a struct containing uninitialized fields
or padding bits to a function without a body no longer raises
an alarm.
- Value [2013-11-14] The option -val-left-shift-negative-alarms has been
renamed into -val-warn-left-shift-negative
-! Value [2013-11-14] Pointer subtraction now requires that the pointers
refer to the same allocated block, and returns the pointwise
difference between the corresponding offsets. Use
-no-val-warn-pointer-subtraction to obtain the previous behavior.
-! Value [2013-11-13] No alarms are emitted for overflowing unsigned
left shift operations.
-* Rte [2013-11-13] No assertions are generated for unsigned left-shift
that may overflow, regardless of whether -warn-unsigned-overflow
is set. Fixes issue #!1555.
-* Value [2013-11-13] Prevent GUI crashes when options -no-results or
-obviously-terminates are set and some functions have
ACSL preconditions
-* Value [2013-11-12] Fixed bug involving the conversion to
float of a double expression e s.t. 0 < fabs(e) <= 0x1.0p-150.
-* Kernel [2013-11-12] The parsed value could be wrong and the warning
for inexact decimal floating-point constants be wrongly omitted
for constants smaller than the smallest subnormal.
-* Logic [2013-11-08] Support for _Bool in ACSL formulas
-! From [2013-11-08] Separately compute data dependencies and indirect
(address, control) dependencies with option -show-indirect-deps
o Kernel [2013-11-08] parameters can be preserved across project creation
through copy visitor (do_not_reset_on_copy function). fixes
do_not_projectify and do_not_reset_on_copy status of
Kernel's options.
-* Logic [2013-11-06] do not cast an enum value toward its associated
integral type when comparing to an enum constant. Fixes #!1546
-* Kernel [2013-11-06] Fixes loop unrolling having in their body 'switch'
with 'continue' stmts.
- Report [2013-11-05] New option -report-untried
-*! Logic [2013-10-29] -check checks that C and associated logic variable
agree on their type. transfer completion of type up to
associated logic var and term when needed. Fixes #1538
-* Logic [2013-10-29] Do not remove labels out of scope of annotations
too quickly. Fixes #1536
-* Kernel [2013-10-29] Do not fail on nested ternary operators whose
value is dropped, as in #1503
-* Logic [2013-10-29] Accept struct with same name as typedef in specs.
Fixes #1518
-* Kernel [2013-10-29] Do not consider array variable as read lval in
unspecified sequence. It can't be written anyway. Fixes #!1519
o* Value [2013-10-27] Type Base.string_id is now concrete. No more need
for function Base.cstring_of_string_id
-* RTE [2013-10-28] Better normalization when using -rte-precond.
- Kernel [2013-10-27] Generate more aggressive assigns clauses for
unspecified library functions that arguments with type pointer
to void or char
-* Kernel [2013-10-26] Do not generate invalid assigns clauses when some
formals are pointers to arrays
- Kernel [2013-10-22] Support for static evaluation of the
__builtin_compatible_p GCC specific function.
- Kernel [2013-10-22] Add -aggressive-merging option to merge two
inline functions if they are equal modulo alpha conversion.
-* Kernel [2013-10-17] Correctly distinguish typenames and declared
identifiers in declarations. Fixes #1500
-* Kernel [2013-10-17] Statements with a label attached to them are
never erased during elaboration. Fixes #1502.
-* Slicing [2013-10-17] Slicing is now compatible with option -val-use-spec
- From [2013-10-15] Better precision when querying information about
a zone that has the same dependencies as its neighbors.
o! Value [2013-10-15] Function Map_Lattice.Make requires a new argument
- Value [2013-10-14] Evaluation of left-values such as t[i][j] or
p->arr[i] is now more precise when the total number of locations
to read or write is less than the value of -plevel option
- Value [2013-10-13] Syntactic loops (ie. 'for', 'while' and
'do ... while') are now always used to perform widening,
regardless of whether they are reducible
-! Impact [2013-10-11] More generic dynamic function impact_statement_gui.
The set of nodes impacted can now be filtered by a memory zone.
-! Journal [2013-10-09] By default, the journal is now generated into
the Frama-C session directory.
o*! Makefile [2013-10-03] Split Makefile.common in two parts in order to
include generic rules (new Makefile.generic file) at the end
of main Makefile, so specialized patterns will be considered
first in make < v3.82
-*! Logic [2013-10-02] Disallow cyclic logic type definitions
-! Gui [2013-10-01] the configuration file .frama-c-gui.config is
now put in the GUI config directory and named frama-c-gui.config.
o Kernel [2013-10-01] Plug-ins may now have their own configuration
directory in which they can generate configuration files
during a Frama-C session.
o Kernel [2013-09-30] Plug-ins may now have their own session
directory in which they can generate project-dependent files
during a Frama-C session.
o* Doc [2013-09-27] Fix ugly display of documentation of dynamic
plug-ins API (bts #!1394).
-* Value [2013-09-26] Fix crash when evaluating \valid(p->off) when
p is NULL or a valid pointer, and p->off is itself only partially
valid (bug #1486).
-* Kernel [2013-09-26] Reject identifiers in the same namespace and same
scope, according to C standard's rules. fixes bug #1330.
o! Kernel [2013-09-26] Alpha.{new,register}AlphaName: transform labelled
argument 'undolist' with option type into optional argument.
-* Kernel [2013-09-26] Fixes issue #1451 about -unicode which was not
taken into account by -load-script.
-* Kernel [2013-09-24] Fixes binding of formals when linking static
prototypes. Fixes issue #1475
o* Scope [2013-09-21] Functions registered in Db now return Stmt.Hptset
values instead of Stmt.Set
o* Value [2013-09-21] Minor signature change for widening functions
- Metrics [2013-09-19] More precise information about coverage
-o Value [2013-09-18] Fix bug in which two distinct memory states could be
erroneously made equal
-* Slicing [2013-09-12] Slicing on a composite statement containing dead
code now works properly
o* PDG [2013-09-12] Function Db.Pdg.find_stmt_and_blocks_nodes
returns a correct result on partially dead composite statements
- Slicing [2013-09-12] -slice-calls main only selects the calls to the
main function, nothing more.
o* Kernel [2013-09-11] Fixed buggy function Property.location.
- Logic [2013-09-10] Improve localisation of error messages during
logic typing.
- Value [2013-09-07] Degeneration points are now shown in the GUI
- Value [2013-09-07] Value analysis can now be aborted while keeping
intermediate results, by sending SIGUSR1 to Frama-C
- Value [2013-09-06] More aggressive evaluation of \initialized(p)
when p points to a memory zone containing both bottom and
non-bottom values
o! Value [2013-09-06] Function Cvalue.Model.find_unspecified now requires
one additional argument ~conflate_bottom
- Value [2013-09-06] Warn for missing '\from' or 'assigns \result \from'
clauses. Fixes wish #1448
-* Logic [2013-09-02] Conversion from C array to pointers do not lose
cast on pointed types. Fixes issue #1469
o* Cil [2013-08-30] Terms containing ACSL keywords are now properly
parsed by function Logic_lexer.lexpr
o* Cil [2013-08-26] Statements containing calls to va_start can now be
printed outside of a function
-* Pdg [2013-08-26] Fix possible non-termination during the computation
of the control dependencies (bug #1436)
- Metrics [2013-07-29] ACSL statistics
-! Value [2013-07-24] Fewer and better widening bounds for pointer
addresses: try the frontier of the block
-! Value [2013-07-24] Better widening bound for signed 32 bits integers
-* Kernel [2013-07-18] More clever merge of function contracts.
Fixes issue #1455
o Lib [2013-07-18] Filepath.normalize can replace paths by a symbolic
o Ptests [2013-07-16] add the possibility to define macros in
configurations. See developer documentation.
-* Kernel [2013-07-11] designated initializers are correctly pretty-printed.
Fixes issue #1457
-* Semantic Constant Folding [2013-07-10] Fixes error when folding fct pointer
resulting in two distinct kf for the same function.
o* Kernel [2013-07-08] Cil.mkEmptyStmt gets a valid_sid argument in
order to generate valid statements.
-* Kernel [2013-07-05] Tmp vars created during typecheck all have a
description. Fixes bug #!1387
-* Kernel [2013-07-04] more informative error message. Fixes bug #1352
-* Kernel [2013-07-04] implicit annotation status is not lost through
code transformations anymore. Fixes bug #!1442
o Kernel [2013-07-04] Added hooks when registering/removing a property
o Kernel [2013-07-03] Added StringList.append_{before,after} for
manipulating options (both static and dynamic API)
- Kernel [2013-06-27] An 'unknown' local status is set on assigns generated
from the C prototype of leaf functions
o Kernel [2013-06-25] Add hooks to register transformation to be performed
on a freshly computed AST. See src/kernel/file.mli
o Kernel [2013-06-25] Add hook builders for hooks that can have
dependencies. See src/lib/hook.mli
o Kernel [2013-06-21] adding a category do not set debugging level to 1.
Conversely debug ~dkey "..." (without ~level) will output "..."
if dkey is requested by the user, even if debugging level is 0.
-* From [2013-06-21] Position the 'and SELF' flag when an assigns clause
z1 and z2 overlap in an assigns clause z1 \from z2 .
- Value [2013-06-21] Better documentation of module Hptmap. Some
incompatible API changes.
- From [2013-06-20] Slowndowns in the analyses can be mitigated using
higher values for option -memory-footprint
- Value [2013-06-20] Option -memory-footprint now accepts much bigger
arguments. The size allocated to each cache is multiplied
by 2 between each increment.
-! Kernel [2013-06-20] Renamed argument ~cache of functions cached_fold
into ~cache_name. The previous integer is no longer used.
-* Kernel [2013-06-20] Fix consolidation algorithm of property statuses
which possibly occurs on cycles involving an unproved property
(bts #1443).
-* Kernel [2013-06-20] Fix incorrect dot output of consolidation graph
of property statuses.
-* Kernel [2013-06-19] Fix pretty-printing of comments in ghost code
(bts #1378 and #1404).
- RTE [2013-06-18] Remove limitation about alarms which do not fit
into 64 bits (bts #1391).
- Kernel [2013-06-18] Better strategy when -save is set and Frama-C
crashes (bts #1388).
-* Project [2013-06-17] Fix messages about projects.
-* Slicing [2013-06-17] Fix crash in presence of assertions involving
sizeof(t), where t is an array. Fixes similar bug with option
-remove-redudant-alarms
-! Inout [2013-06-13] Inputs of an instruction whose evaluation fails
now include the sub-expressions for which evaluation succeeds
-* Value [2013-06-12] Fix crash when the creation of the initial state
encounters a completely invalid compound initializer.
- Value [2013-06-11] The name of an evaluated property is now displayed
in the log message. Fixes wish #1415.
- Value [2013-06-11] Assertions on dead code now get a "true because
unreachable" status.
- Kernel [2013-06-23] The annotation 'loop pragma UNROLL "done", n;'
disables the unrolling of the annoted loop. Option -ulevel-force
has to to used for enabling the transformation of such a loop.
This pragma is introduced by the unrolling process in order to
prevent unrolling on source code obtained by a previous frama-C
run.
- Value [2013-06-05] Preliminary support on \forall and \exists
quantification when the introduced variables have a C type.
o! Value [2013-06-05] API change in module Base. Use script
bin/fluorine2neon.sh for automatic migration.
- Value [2013-05-26] Evaluation of \base_addr, \offset and \block_length
logic predicates.
o! Cil [2013-05-26] Rename function sizeOf_int into bytesSizeOf.
- Value [2013-05-26] Basic support for \inter logical predicate (treated
as an union).
- Value [2013-05-25] Distinguish unreachable state and invalid location
when printing the value of a l-value in the GUI
- Value [2013-05-25] Frama_C_show_foo functions now display struct
arguments in extenso.
-* Value [2013-05-24] Failure during a memory zone copy is now properly
notified. Alarms were emitted, but a non-bottom result was
simultaneously returned.
- Slicing [2013-05-24] Better slicing of complex logical assertions
(bug #690).
o! Value [2013-05-23] Do not crash when printing arrays or structs
containing abstract structs (bug #1416).
-! Kernel [2013-05-20] Support parsing and printing "asm goto" from gcc 4.6.
Added a component to Cil_types.Asm constructor.
- Pdg [2013-05-03] Shorter output when outputting results
o! Pdg [2013-05-03] Results of Pdg cannot be intercepted by
Log.add_listener anymore. Use Db.Pdg.get and Db.Pdg.pretty
instead.
o! From [2013-05-03] Results of From cannot be intercepted by
Log.add_listener anymore. Use Db.From.{pretty,display} to print
them.
o! Value [2013-05-03] Results of Value cannot be intercepted by
Log.add_listener anymore. Use Db.Value.display to print them
o! Value [2013-05-03] Remove functions Cvalue.Model.pretty_without_null and
Db.Value.display_globals. Function Db.Value.display is now a
reference to the real function. Removed last argument of
Cvalue.Model.pretty_filter.
###########################################
Open Source Release 9.2 (Fluorine-20130601)
###########################################
-* Value [2013-06-11] Add missing C library files.
###########################################
Open Source Release 9.1 (Fluorine-20130501)
###########################################
- Value [2013-05-22] Better precision for ^ (bitwise xor) operator
when applied on intervals of positive integers
-* RTE [2013-05-22] Fix off-by-one error in alarms on overflowing
unsigned unary minuses.
-* Value [2013-05-21] Catch evaluation errors when selecting a logic
l-value in the GUI.
o* Kernel [2013-05-06] Fixed Type.pp_ml_name for polymorphic types
with 3 and 4 type variables (bug #1127).
-* Makefile [2013-05-06] Fixed installation directory of the doc in
plug-in's Makefile (bug #1278).
###########################################
Open Source Release 9.0 (Fluorine-20130401)
###########################################
o! Cil [2013-04-11] Remove Cil pretty-printer. Use module Printer
instead. The script bin/oxygen2fluorine.sh may be used to
automatically convert your code.
- Cil [2013-04-09] Handles interpretation of linemarker ending by //
and cleanup file paths.
- Value [2013-03-26] Highlight non-terminating calls.
- Value [2013-03-26] The location in which the result of a call is stored
is now evaluated before the call. A warning is emitted if this
location has changed after the call.
- Logic [2013-03-26] Improved merge strategy for assigns, and report
the presence of different assigns clauses between two files.
- Value [2013-03-23] Better precision for postconditions in functions
with multiple return analyzed without slevel.
-* Value [2013-03-20] Fix incorrect interpretation of \valid{L}(P) when
L is not Here label.
-! Value [2013-03-20] The first element of a -lib-entry allocated array,
or of an array passed as an argument to main, is now valid
regardless of option -valid-context-pointers.
-* Slicing [2013-03-18] Fix incorrectness in presence of assertions involving
\initialized predicate. User predicates are no longer treated.
-* Value [2013-03-15] Fix incorrectness of option -remove-redundant-alarms
in presence of '\initialized(...)' alarms.
- Value [2013-03-15] Optionally warn against unsigned overflows according
to option -warn-unsigned-overflow.
- Cil [2013-03-14] The type of fields that are bit-fields now carry an
informative attribute FRAMA_C_BITFIELD_SIZE.
-* Value [2013-03-09] Fixed misleading "after statement" state on
statements followed by an assertion.
-* Value [2013-03-09] Option -memexec is now correct in presence of RTE
-! Value [2013-03-09] Consolidated states are now stored before 'assert'
clauses are evaluatued.
-* Slicing [2013-03-03] Fix options -slice-assert and -slice-threat
(-threat did nothing, -assert selected all alarms).
-! Sparecode [2013-03-03] Alarms are now ignored during the analysis.
-* Value [2013-03-03] Fix incorrect reduction in integers containing
pointers address when option -warn-signed-overflow is set.
-! Value [2013-03-03] Signed overflows now cause an alarm. Option
-no-warn-signed-overflow can be used to get 2's complement.
-! Kernel [2013-03-03] Signed overflow alarms are now emitted by default.
-! Kernel [2013-03-03] Signed downcast alarms are no longer emitted by
default. Use option -warn-signed-downcast to activate them.
- Kernel [2013-03-02] Print signed downcast alarms as 'signed_downcast'
-! Value [2013-03-02] Removed option -val-signed-overflow-alarms.
Use -warn-signed-overflow instead.
-! Rte [2013-03-02] Removed options -rte-signed, rte-unsigned-ov,
-rte-downcast and -rte-unsigned-downcast. They are replaced
by -warn-signed-overflow, -warn-unsigned-overflow,
-warn-signed-downcast and -warn-unsigned-downcast respectively.
-* Rte [2013-03-02] Added missing alarm for casts from overly large
floating-point numbers to integer. Fixes #!1318.
-* Value [2013-02-28] Initial state of Value does not depend on -main
option, but depends on -context-<...>.
- Value [2013-02-27] Emit proper alarms for completely imprecise
floating-point values, and for casts from float to int.
-* Impact [2013-02-23] Prevent crash when a caller or callee function has
been imprecisely analyzed.
- Pdg [2013-02-23] Ignore inline asm statements (previous behavior was
to generate Top Pdgs).
-* Value [2013-02-23] In -lib-entry mode, void* fields or pointers now
point to something potentially valid.
- Value [2013-02-22] Option -val-ignore-recursive-calls now uses the
assigns clauses of the recursive function to treat the call.
- Value [2013-02-17] Improved support for va_arg variadic macro.
-! Value [2013-02-17] Renamed options -initialized-padding-globals
and -no-no-results into -uninitialized-padding-globals and
-val-store-results respectively.
-* Value [2013-02-17] Improved again support for abstract structs.
o! Value [2013-02-15] Generic types of Value are now in Value_types
(previously Value_aux). Implies a signature change for
Db.Value.register_builtin. Value_aux.accept_base is now in
Db.Semantic_Callgraph.
- Value [2013-02-13] Offsets in misaligned values that repeat themselves
are now always printed relatively to the beginning of the binding.
- Value [2013-02-12] Suppress superfluous warning when passing as
argument a struct that contains pointers.
-* Metrics [2013-02-12] Global variables both declared and defined were
counted twice.
-* Metrics [2013-02-11] Option -value-metrics now report a correct location
for function referenced by an initializer. Fixes #!1361.
o! Value [2013-02-08] Renamed Locations.valid_enumerate_bits into
Locations.enumerate_valid_bits.
o*! Kernel [2013-02-08] Must register keywords introducing new clauses of
ACSL contracts. Fixes issue #!1358.
o! Kernel [2013-02-08] redesign of message categories.
See detailed changelog for more information.
o! Cil [2013-02-07] Clean up registering of new machdeps. Some machdep
options have been integrated into Cil_types.mach, or removed from
Cil.theMachine (as they were already in Cil_types.mach).
- Value [2013-02-06] Improve reduction by conditions that involve '&'
and '|' operators.
-* Value [2013-02-06] Fix validities of degenerate variables, which were
too big considering the size of the memory.
-* Impact [2013-02-06] Prevent crash when considering a function with an
unreachable first statement.
o! Logic [2013-02-04] Change Property_status.Consolidation_graph.dump
now takes a formatter instead of a file name.
- Value [2013-02-02] Improved support for abstract structs.
o! Value [2013-02-02] Removed Base.All validity. Use big validities
with unknown flag instead. Improved signature of Base.Unknown.
o! Cil [2013-02-02] Renamed function Cil.alignOf_int into bytesAlignOf.
o! Cil [2013-02-02] Remove unused 'alignof_char_array' machdep field.
-* Value [2013-02-01] Fix erroneous casting operating when interpreting
logic casts.
-* Kernel [2013-02-01] Ghost status is appropriately propagated in
statements (instead of only instructions) and pretty-printed
accordingly. Fixes issue #1328.
- Value [2013-02-01] Value more aggressive evaluation of construct
'//@ for b: assert p' when b is guaranteed to be active.
Harmonize behaviors-related messages.
- Kernel [2013-01-29] The level of verbose is at least the level of debug.
-* Value [2013-01-28] Ignore 'const' qualifier on extern globals in
lib-entry mode. Previously, those globals were initialized to 0.
- Obfuscator [2013-01-28] Hide variables that do not appear in the output
from the dictionary.
-* From [2013-01-28] Fix rare bug in presence of involved control-flow
graphs and non-terminating calls.
o! Slicing [2013-01-21] Remove no longer used ~ai argument.
-!*Value [2013-01-21] Various changes in the way undefined functions
returning pointers are handled.
- Value [2013-01-20] Alarms emitted by Value are no longer evaluated
during analysis (unlike user assertions).
- Value [2013-01-20] More aggressive reduction in presence of write
through partially invalid pointers. Warn if the pointer is
completely invalid.
-* Value [2013-01-20] Option -absolute-valid-range can now be changed
between two executions of Value.
-! Slicing [2013-01-19] Alarms are now removed in the generated project
(regardless of option -slicing-keep-annotations).
-! Sparecode [2013-01-19] RTE or Value-generated alarms are now removed
in the generated project.
o! Value [2013-01-17] Builtins must now warn if their results should not
be cached (signature change in Db.Value.builtin_result).
o* Kernel [2013-01-16] Visitor no longer crashes when a non-function global
is replaced by a list containing at least one function or