Newer
Older
'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
prototype (fixes bug #!1349).
!* Kernel [2013-01-10] Add lv_kind field to trace origin of logic variables.
Cil_const.make_logic_var is deprecated in favor of specialized.
-* Kernel [2013-01-10] Fixed bug #!1347 about accessing to a consolidated
status of a property which depends on removed hypotheses.
o! Kernel [2013-01-10] Remove method is_annot_before from visitors
(it return only 'true').
-* Makefile [2013-01-08] Compile OcamlGraph less often: fixes issue #1343.
- Value [2013-01-08] More agressive analysis of statements with improperly
sequenced accesses when option -unspecified-access is used.
o Kernel [2013-01-04] New methods videntified_term and
videntified_predicate for the visitor.
-* Kernel [2013-01-04] Fixed discrepancy between compare_type and hash_type.
Added new datatype TypNoUnroll.
o Kernel [2013-01-03] Added pp_field and pp_model_field in Printer_api.
o Kernel [2013-01-03] Added type modules
Cil_datatype.Wide_string and Datatype.List_with_collections.
-* Logic [2013-01-03] Fixes various type-checking issues in presence of
polymorphism and implicit conversions (including #1146).
o! Kernel [2012-12-21] Module Cilutil has been removed. Previously used
list functions can now be found in Extlib (use script
oxygen2fluorine.sh for migration). Functions related to
configuration files are now Cilconfig.
o! Impact [2012-12-21] Function Db.Impact.compute_pragmas now returns
a list of statements.
-* From [2012-12-21] Fix absence of effect of option -calldeps after
a save/load cycle.
-* Inout [2012-12-21] Fix absence of effect option -inout-callwise after
a save/load cycle.
o! Kernel [2012-12-13] Reorganize AST's pretty-printers. You must now use
module Printer. Use the script oxygen2fluorine.sh to upgrade
your plug-in.
o! Kernel [2012-12-13] Remove Cilutil's pretty printing helpers. Use
Pretty_utils' ones instead.
- Inout [2012-12-12] Indirect reads (for example 'p' for '*p') are now
automatically added to inputs when evaluating assigns.
- Value [2012-12-12] Evaluation of assigns now include indirect reads
(ie 'assigns *p' depends on p) automatically.
- Value [2012-12-07] Improve handling of conditionals when option
-val-ilevel is used.
- Pdg [2012-11-28] InCtrl nodes are no longer displayed in Dot graphs.
o! Kernel [2012-11-24] Various types whose names started by t_ in
PDG/slicing related modules are now unprefixed.
o Rte [2012-11-23] Export function "exp_annotations" to get RTEs of a C
expression as annotations.
o*!Kernel [2012-11-23] Added TLogic_coerce constructor to mark
explicitly a conversion from a C type to a logical one
(in particular floating point -> real and integral -> integer).
Fixes issue #1309.
o! Kernel [2012-11-22] Remove unintuitive ?prj argument from Cil visitors,
and first argument of Visitor.generic_frama_c_visitor. Information
is now stored inside the type Cil.visitor_behavior.
-* Value [2012-11-20] Fix evaluation of logic constant characters
above 127.
-* Value [2012-11-20] Fix soundness bugs for comparisons with logic
constants that are not representable as 64 bits double.
o! Kernel [2012-11-20] Signature change for constructor LReal.
- Rte [2012-11-16] Generate Value-compatible alarms and annotations.
- Kernel [2012-11-16] Syntactic constant folding is done once by AST
(fixed bug #!1306).
- Value [2012-11-13] More precise line numbers for statuses of assertions
and loop invariants.
- Value [2012-11-09] New option -val-callstack-results to record and
display in GUI the results split by callstacks.
o Kernel [2012-11-08] New function Annotations.model_fields.
-! Rte [2012-11-06] Remove option -rte-print. Use -print instead.
-* Kernel [2012-11-06] Do not print help of negative options when the
positive one is invisible (fixed #1295).
o! Kernel [2012-11-05] Get rid of useless rooted_code_annotation datatype.
-* Aorai [2012-10-31] Adds locations modified by Aorai to existing
loop assigns (fixes issue #1290).
o Kernel [2012-10-31] Renamed Kernel_function.self to
Kernel_function.auxiliary_kf_stmt_state to avoid confusion.
o Kernel [2012-10-31] New function 'get' for projectified counters.
- Kernel [2012-10-29] Better frama-c.top (fixed issue #1287).
-* Kernel [2012-10-26] Do not attempt to merge unrelated anonymous enum
that have been given the same name by Cil (fixes #1283).
- Logic [2012-10-26] Extended syntax for naming terms and predicates
("string":pred and "string":term are now allowed).
o! Kernel [2012-10-18] New API for module Alarms.
- Kernel [2012-10-18] When printing the AST, display the emitter name
of generated annotations and also the origin of
annotations corresponding to an alarm.
o* Kernel [2012-10-18] Fixes incorrect visitor behavior with JustCopy
(issue #1282).
- Value [2012-10-16] Reduce more aggressively on accesses *p where p is
imprecise but contains only one valid value.
-* Value [2012-10-16] Correct potentially incorrect reduction on l-values
of the form *(p+off) or *(p-off).
-* Kernel [2012-10-16] Fixed bug with Type.pp_ml_name for pairs,
triples and quadruples which can lead to incorrect journal
generation (new occurrence of bts #1127).
o Kernel [2012-10-12] Optional argument 'reorder' to File.* functions
creating an AST in a new project from a visitor.
-* Value [2012-10-12] A bug causing the number of superposed states to be
slightly underestimated has been fixed. As a result, it may be
necessary to up the -slevel argument a little bit for existing
proof scripts.
- Kernel [2012-10-11] Option -enums for choosing representation of enums.
-* Scope [2012-10-10] Prevent crash in defs computation when a lvalue is
a formal.
o* Makefile [2012-10-01] Fix installation directory of API documentation
(fixed bts #1278).
- Kernel [2012-10-01] Assumptions and axioms now get consolidated status
"Considered valid" instead of "Valid".
-* Value [2012-10-01] Fix "Semantic level unrolling superposing up to"
messages. The number displayed was sometimes lower than
the actual number of superposed states.
-* Gui [2012-10-01] In some cases, after a crash of an analyzer,
the GUI was not fully restored, became inconsistent and could
crash.
o! Value [2012-09-30] Remove various instances of Top_Param, which were
all equal to Base.SetLattice.
o Pdg [2012-09-30] Fix display for control dependencies in PDG graphs.
o Kernel [2012-09-20] Provide Datatype.triple and Datatype.quadruple
(bts wish #1277).
o* Kernel [2012-09-20] Fixed consistency check of descriptor when
building polymorphic datatypes (fixed bts #1277).
###############################################################################
Open Source Release 8.0 (Oxygen-20120901)
###############################################################################
-! Kernel [2012-09-17] Remove useless negative options -no-help,
-no-version, -no-print-share-path, -no-print-lib-path and
-no-print-plugin-path.
- Kernel [2012-09-13] All globals with attribute FC_BUILTIN are preserved
even if unused.
- Value [2012-09-13] Print misaligned values in a simpler way. Fixes
wish #!1271.
o!* Cil [2012-09-12] Split constants of logic and C (fixes bts #745).
o! Cil [2012-09-12] Remove type Cil_type.typeSig. Use the functions in
Cil_datatype.Typ and Cil_datatype.Logic_typ to compare types.
-* Kernel [2012-09-07] Identical messages emitted in two different projects
will now be visible in both projects. Fix bug #1104.
o Kernel [2012-09-07] Improve signature of State_builder.Set_ref.
o* Kernel [2012-09-07] Correct hash function for Sets created by
Datatype.Make_with_collections or Datatype.With_collections.
o* Kernel [2012-09-06] Datatype with structural comparison
for exp and lval fixes bts #1263.
-* Kernel [2012-09-06] Fine tuning AST dependencies. See developer guide.
-* Kernel [2012-09-05] Fixed missing undefined behavior
for multiple write accesses (fixes bts #1059).
-* Metrics [2012-09-05] Fixes count of pointer accesses.
- Value [2012-09-05] Clarified message about completely indeterminate
-* Kernel [2012-09-03] Do not accept spurious '}'. Fixes bts #1273.
o! Kernel [2012-09-03] Remove obsolete constructors Cabs.TRANSFORMER and
Cabs.EXPRTRANSFORMER and related parsing rules.
- Value [2012-09-02] Warn when 'assigns *p' points to a completely
invalid location.
- Value [2012-09-01] Assertions such as \valid(p) now evaluate to Invalid
when p is not initialized or an escaping address.
-* Value [2012-08-30] Fix crash when evaluating *((int*)0+x)=v when the
NULL base is invalid.
-* Kernel [2012-08-29] Fixed #!1267 (adds explicit casts for default
argument promotions).
o! Value [2012-08-29] Signature change for function
Db.Value.register_builtin: builtins can now return multiple
states.
o! Value [2012-08-20] Rename Db.Value.assigns_to_zone_inputs_state to
Db.Value.assigns_inputs_to_zone. Add new functions
Db.Value.assigns_outputs_to_zone and
Db.Value.assigns_inputs_to_locations.
-* Kernel [2012-08-21] Fixed bug with save/load: loading a file <f>, then
quitting Frama-C can no longer modify <f> (bts #!1269).
+* Logic [2012-08-08] Fixed bts #!1262 about logic preprocessing
and string escapes.
- Value [2012-08-02] Statutes 'Invalid' are now positioned on 'for behav:'
assertions even when 'behav' is not the only active behavior.
o* Cil [2012-08-02] Fixed bts #1254: incorrect documentation of
Cil.d_plaininit.
-* Logic [2012-08-01] Fixed bts #!1253: IndexPI and PlusPI are equivalent.
o* Kernel [2012-08-01] Fixed bts #!1250: setting formals of visited
function is not delayed until fill_global_tables anymore.
+* Slicing [2012-07-31] Fixed bts #!1248 about empty slicing request.
-* Journal [2012-07-31] Fixed bts #932 about journalization of dynamic
plug-ins in some corner cases.
o!* Kernel [2012-07-31] Operations that silently mutate AST should now call
Ast.mark_as_changed to clear states depending on it
(fixes #!1244).
o Kernel [2012-07-30] API of dynamic plug-ins is now documented as
well as static plug-ins (fixed bts #!171).
- Slicing [2012-07-30] No more blank between -slicing-project-name and
-slicing-exported-project-postfix (from #!1249 entry).
- Gui [2012-07-27] Fixed bugs when the consolidation graph cannot
be displayed (fixed bts #1122).
- Kernel [2012-07-24] The annotation 'loop pragma UNROLL "completly", n;'
unroll 'n' times the annoted loop and then add it a clause
'loop invariant \false;'. The remaining loop should be death code.
o Kernel [2012-07-24] Changes in interface of StringHashtbl options.
-! Inout [2012-07-22] Option -inout-callwise restarts Value when it is
newly set
- Impact [2012-07-19] Complete rewrite. Improved precision and computation
time. Fixes wishes #!5 and #!6.
-* Logic [2012-07-18] Fixes sizeof("string_literal") in logic.
- Logic [2012-07-18] Better error messages when parsing logic.
- Kernel [2012-07-16] C constant expressions are now allowed as UNROLL
level into loop pragmas.
o! Cil [2012-07-16] Ast changed: Unrool_level renamed into Unroll_specs
and its argument becomes a list for next evolutions.
o! Kernel [2012-07-16] Add function [stmt_can_reach] to the arguments
of Dataflow.Backwards, which is used to speed up the analysis.
See dataflow.mli for good possible values.
- Kernel [2012-07-16] linker checks that the ghost status of two merged
declaration is the same, and raises an error otherwise.
o* Kernel [2012-07-16] -check verifies if vdefined flag is coherent with
status of variable in Globals tables and AST. Fixes one of the
issues of #!1241.
-! Rte [2012-07-16] Rename option -rte-const into
-rte-no-trivial-annotations (set by default).
-* Value [2012-07-15] Fix crash when an undeclared function returned
a pointer to a function that was later called.
-* Rte [2012-07-14] Prevent generation of incorrect alarms on statements
whose order of execution is not completely specified.
- Rte [2012-07-14] Generate simpler assertions for accesses to arrays,
and discard trivial ones; improve ordering of assertions.
Honor option -unsafe-arrays.
o Makefile [2012-07-13] Added variables PTESTS_OPTS and PLUGIN_PTESTS_OPTS
to pass options to ptests through make tests. See dev manual.
-! Value [2012-07-12] More thorough checks for calls through a function
pointer: warn when the function type and the pointer are
not compatible, and stop when they cannot be reconciled.
-! Kernel [2012-07-12] A negative value given to -ulevel option hides all
UNROLL_LOOP pragmas.
- Report [2012-07-10] Display unreachable properties in a special way;
identify unreachable statement more clearly.
- Gui [2012-07-10] Display all properties in 'Properties' panel,
including generated ones without location.
+! Kernel [2012-07-10] Change semantics of 'reachable' properties
for functions. Use intrinsic notion instead of accessibility
of first statement.
o Kernel [2012-07-04] Hook for handling for loop components in Cabs.
o Makefile [2012-07-04] plugin is distributed iff PLUGIN_DISTRIBUTED and
PLUGIN_ENABLE are not 'no' (instead of PLUGIN_DISTRIBUTED == yes).
-* Kernel [2012-07-03] Fixes bug #840 (inaccurate position in presence of
-pp-annot).
o+ Kernel [2012-06-29] New functions Annotations.remove_* and .fold_* for
each component of a contract and other small API changes.
Better compatibility between Visitor and Annotations.
- Kernel [2012-06-26] New option -keep-unused-specified-functions.
o! Kernel [2012-06-25] Correct (albeit slow) hash function for terms
and term lvalues.
-* Cil [2012-06-25] Better propagatation of volatile, const and restrict
type qualifiers through typedefs on arrays
-* Cil [2012-06-25] Preserve typedefs on global variables with an
initializer
-! Kernel [2012-06-22] improve 'reachable' properties.
o! Kernel [2012-06-19] Remove module Inthash. Use Datatype.Int.Hashtbl
instead, or directly carbon2nitrogen.sh migration script.
o! Value [2012-06-18] Made type Ival.tt private.
- Kernel [2012-06-16] Consolidation from call-site preconditions to
original precondition now handle calls through function pointers
- Value [2012-06-16] Position call-site statuses for function
preconditions, instead of the previous global status.
- Cil [2012-06-13] New option -warn-undeclared-callee for calls to
functions that have not been previously declared.
- From [2012-06-12] Better precision for code of the form
'if (c) stop(); else y = x+1;', where stop does not terminate
- Pdg [2012-06-12] Improve precision in presence of provably dead
code branches. Fixes issue #1194.
o Makefile [2012-06-12] Use ocamldoc.opt whenever possible.
- Rte [2012-06-11] Reuse behaviors names when -rte-precond is used
on fonctions with multiple behaviors.
o! Kernel [2012-06-11] New API for Annotations which merges old
Annotations, Globals.Annotations and operations of Kernel_function
over function contracts.
- Scope [2012-06-08] Improved computation of defs. Statements are
categorized between direct and indirect accesses.
-! Pdg [2012-06-08] Rename option -dot-pdg into -pdg-dot
- Logic [2012-06-07] Cleaner generated assertions in presence of multiple
pointer casts.
o! Kernel [2012-05-30] Kernel.Functions.get does not silently create
a kernel function if it does not already exist. This behavior
is kept for Cil builtins.
-* Kernel [2012-05-29] Fix graph of consolidation statuses when
several properties get the same name.
-* Value [2012-05-19] Calls (*p)() where p resolves to both valid functions
and invalid addresses are now properly handled.
- Value [2012-05-19] Add bzero builtin. A precise destination and size
are required (wish #915).
-* Value [2012-05-19] In lib-entry mode, honor 'const' attributes that
appear deep inside the type (bts #759).
-* Value [2012-05-19] Better time and space complexity for initialization
of big arrays in -lib-entry mode (bts #1026).
o* Kernel [2012-05-16] Fix implementation of Datatype.Triple and
Datatype.Quadruple (bts #!1133).
-* Value [2012-05-15] Re-emit alarms when Value options are changed and
an analysis is restarted.
- Value [2012-04-29] New option -val-ilevel, to change the frontier
between sets of integers and intervals.
- Kernel [2012-04-27] when printing help, display the name of the
opposite boolean option (bts #1085).
-* Kernel [2012-04-26] Fixed bug with Type.pp_ml_name for generic sets
which can lead to incorrect journal generation (bts #1127).
o! Kernel [2012-04-26] Plugin.set_optional_help is now deprecated.
-* Value [2012-04-26] Fix possible typing bugs when evaluating logic
expressions with non-integral types (bts #!1175).
- Kernel [2012-04-24] Use Zarith whenever possible (bts #!983).
- Value [2012-04-16] Allow comparison of invalid pointers in the logic.
- Value [2012-04-15] Old "Evaluate expression" menu in the GUI replaced
by "Evaluate ACSL term"; value of term lval is now displayed.
Evaluations that may fail are flagged.
- Value [2012-04-15] Errors during evaluation in the logic are now
reported.
*! Kernel [2012-04-14] Introduce more temporaries for a call [lv = f()] if
the return type of f and the type of lv do not match. Fix
issue #1024.
-* Value [2012-04-14] Fix incorrect initialization of volatile fields
or globals in presence of initializers (bts #!1112).
o* Makefile [2012-04-12] Fix bug #1145 about PLUGIN_LINK_GUI_OFLAGS.
-* Kernel [2012-04-12] Strict checking of type compatibility when merging
an already called prototype without arg list and a full prototype
(fixes issue #728, #!109).
- Kernel [2012-04-12] New option -<plugin>-share for plug-ins to
customize their specific share directories.
- Rte [2012-04-06] Emit \valid_read alarms instead of \valid for
read accesses.
- Inout [2012-04-05] Better precision for 'if' in which only a side
is reachable.
- Kernel [2012-04-05] Keep all prototypes with a spec,
even if not referenced.
- Inout [2012-04-04] Operational inputs are now more precise for
function with only an ACSL prototype.
-* Kernel [2012-04-04] Fixes issue in loop unrolling and annotations.
-* Kernel [2012-04-02] Fixed bug #1135 and bug #1139 about loop unrolling.
- Logic [2012-03-29] LoopEntry and LoopCurrent built-in labels.
- Value [2012-03-26] Support for \valid_read predicate; evaluation of
\at(p,Pre) and \initialized{Pre}(...).
o! Kernel [2012-03-26] Kernel.CppExtraArgs now gets type
Plugin.String_list and not Plugin.String_set (fixed bts #!1132).
- Value [2012-03-24] Improved handling of conditions involving the
conversion to int of a floating-point variable.
- Journal [2012-03-21] Better journalisation of command line options
setting a list of arguments (e.g. -slevel-function): avoid
quadratic complexity in the generated code (fixed bts #!1123).
- Gui [2012-03-20] Removing 'add assert before' from contextual menu.
Uses ACSL_Importer plugin for such a feature.
-* Value [2012-03-18] Handle 'assigns *p' where p has a typedef type
- Kernel [2012-03-18] Support for model fields
-* Kernel [2012-03-12] Initialization of locals is correct for all sizes;
uses bzero to 0 + contract (directly validated by Kernel)
-* Value [2012-03-12] Fixed bug where user assertions accessing
uninitialized variables got the wrong status.
- Value [2012-03-12] Improved handling of *(p+i) (or equivalently p[i])
when p is a known pointer and i is unknown.
-! Kernel [2012-02-29] Adding some more supports for built-in related to
memory blocks.
-! Cil [2012-02-24] Functions returning a value cannot let control flow
falling through the closing '}' Fixes #685.
- Inout [2012-02-24] Option -inout-callwise to compute callsite-wise
operational inputs. Improves precision of -inout, of the
"Modifies" clause in the gui, and of the slicing.
-! Kernel [2012-02-23] Sets generated assigns clauses into the default
behavior.
- Value [2012-02-22] New message for functions with only a specification.
Changed old message for functions with neither code nor
specification to "No code nor specification for function ...".
- Value [2012-02-21] Evaluation of \separated predicate
-* Value [2012-02-21] Fix bug in evaluation of pointers to start of array.
-* Cil [2012-02-20] Improve label positions in presence of loop
unrolling (bug #1100).
-* Value [2012-02-18] Fix crashes and/or missing alarms when evaluating
*p=(cast)f() with p invalid (bug #!1097).
-* Cil [2012-02-13] Correct sharing bug on widening pragmas.
Fixes #!1090.
o* Cil [2012-02-11] Fixed off-by-one error in
foldLeftCompound ~implicit:true.
o* Makefile [2012-02-09] 'make doc' did not work when GUI disabled
(bts #1014).
-! Kernel [2012-02-08] Adding supports for clause allocates and frees
and their version for loops.
- Slicing [2012-02-07] More precise slicing when -calldeps is used
(fixes wish #107).
-* Kernel [2012-02-07] Fixed bug about property statuses and setting
parameters after -load (statuses were not cleared when required).
-* Value [2012-02-07] Allocate a finite space for malloc builtins; fixes
some bugs when a pointer refers to a non-yet allocated space.
-* Journal [2012-02-07] Fixed bug #!1080: better generated journal
in case of missing internal data preventing it of being runable.
o* Makefile [2012-02-07] Fixed bug #1082 about wrong link in
generated code documentation.
- Scope [2012-02-04] Improve precision of Defs computation (wish #1079).
- Value [2012-02-02] Assertions of the form \valid(p+i) and \valid(&p->f)
are now used to reduce p whenever possible.
- Value [2012-01-30] Improve precision for code with pointer casts
(fixes bug #1074).
-* Syntactic_callgraph [2012-01-27] Fix bug #989 about difference of
display between GUI and dot output.
-* Syntactic_callgraph [2012-01-27] Fix tricky bug while computing
services when a cycle depends on another cycle (most part
of the fix is actually in OcamlGraph itself).
-* Value [2012-01-27] Evaluate ACSL && and || when they appear as terms
(fixes bug #1072).
- From [2012-01-25] More sharing between identical values when
printing results.
- Pdg [2012-01-25] Improve performance, typically on arrays of structs.
- Logic [2012-01-23] Better label inference in axiomatics (see bts #1068).
- Cil [2012-01-20] In debug mode, pretty-print numerical constants
instead of displaying the source file strings.
- GUI [2012-01-19] Add filters for properties' consolidated statuses.
- Value [2012-01-19] Aesthetic fix: do not display {{ &NULL }} and
{{ &"foo" + {2} }} but rather {{ NULL }} and {{ "foo" + {2} }}.
- Occurrence [2012-01-10] Results can be filtered to display only occurrences
in read or write positions.
- Value [2012-01-09] FRAMA_C_MALLOC_INDIVIDUAL modelization now
properly treats allocated blocks as uninitialized.
- Value [2012-01-07] Reduce more aggressively invalid pointers:
{ p->f1 = v1; p->f2 = v2 } will usually raise at most one alarm.
- Value [2012-01-03] During evaluation, reduce indexes that are detected
as out-of_bounds.
- Value [2012-01-03] In index out-of-bounds alarms, do not generate
'assert 0 <= i' part when 'i' is always greater than 0.
o Kernel [2011-12-19] Added Property.location function.
o* Value [2011-12-05] Fix option -absolute-valid-range being reset by
project copies.
-* Value [2011-12-05] Fix wrong hash function, which could cause
memory overuse and worse.
o Value [2011-12-02] Lmap.paste_offsetmap now handles imprecise
destinations.
o! Value [2011-12-02] Moved contents of memory_state/Abstract_value
into ai/Lattice_Interval_Set. Use bin/nitrogen2oxygen for
automatic migration.
- Project [2011-11-28] Accept to load inconsistent project by setting
to default the inconsistent states and their dependencies.
- Value [2011-11-26] Minor improvements related to single-precision
floating-point handling.
-* Pdg [2011-11-24] Option -pdg did nothing if -pdg-print was not set.
- Value [2011-11-22] After emitted an alarm \initialized(lv), the
value analysis tries to remember that lv is initialized.
This suppresses redundant alarms that were emitted further on.
-* Value [2011-11-22] Fixed soundness bugs involving lval = lval;
assignments targeting literal strings and automatically
created S_... memory zones.
- Value [2011-11-22] Suppressed confusing message "all target addresses
were invalid. This path is assumed to be dead.".
-* Value [2011-11-21] Prevent potentially incorrect assertions from being
emitted when the result a call must be cast. Fixes #997 and #1024.
o Kernel [2011-11-21] New File.init_from_project function.
- Value [2011-11-20] New builtin Frama_C_assert. Take advantage of
existing assertions with "#define assert Frama_C_assert".
-* Occurrence [2011-11-19] Fix bug where some occurrences were silently
ignored in big asts; improve performance.
-* Cil [2011-11-18] Go to new line more often when printing sequence
of statements. Fixes issues #1021.
- Value [2011-11-17] Better evaluation of \initialized predicate when
only some parts of the location are initialized.
- Value [2011-11-17] New option -no-val-left-shift-negative-alarms to
treat left shift of negative integers as defined.
-* Cil [2011-11-14] Fail when encountering a lvalue of type void (#1013).
- Value [2011-11-10] Evaluate more precisely statements of the form
if (*p == 1) {...} when *p is reused within the if block. This
also improves the handling of switches.
-* Kernel [2011-11-09] keep track of local variables even in presence of
annotation + do not silently lose statement contract.
Fixes issue #1009.
-*! Kernel [2011-11-07] empty list in complete/disjoint is expanded by
logic type-checker to the list of behavior name of current
contract. Fixes issue #1006. See bts comments for the
differences that can appear in the treatment of specs.
- Aorai [2011-11-07] Aorai gets a real Dataflow analysis for contract
generation + various logic simplifications.
- Gui [2011-11-04] Display global annotations in the filetree.
o! Cil [2011-11-04] Add method pFile in printers. Signature change for
Cil.d_file (but you should use !Ast_printer.d_file).
- Inout [2011-11-03] Major precision improvements when evaluating library
functions whose assigns contains ranges.
- From [2011-11-03] Major precision improvements when evaluating library
functions whose assigns contains ranges.
-* Logic [2011-10-30] Fixes issue #1005 (earlier detection of duplicated
axiom name avoids Kernel.fatal).
o Kernel [2011-10-27] Plugin.Register defines a new option
-plugin-debug-category that allows to enable debugging for
sub-categories of messages (See Log.set_debug_keys for more info).
-* Value [2011-10-27] Fixed #1001: do not warn for unsigned shifts,
do not end propagation on signed left shift of an address.
o Value [2011-10-27] shift_left and shift_right functions now take
an optional signedness boolean in addition to the optional size.
-* Value [2011-10-26] Generate correct assertions when using memcpy
builtin. Fix #1000.
- Value [2011-10-25] Improve interpretation of ACSL annotations in
presence of typedefs.
-* Value [2011-10-24] Improve warnings and evaluation in presence of
possibly infinite floats (fixes #997).
-* From [2011-10-21] The interpretation of explicit assigns clauses for
library function "assigns *p \from x;" was wrong: every possible
location was assumed to have been overwritten.
-* Kernel [2011-10-20] Link error aborts Frama-C (fixes #990).
-* Kernel [2011-10-20] Better linking behavior (fixes #672).
o! Kernel [2011-10-18] Logic_preprocess.file takes an additional parameter,
as gcc pre-processor treats differently .c and .cxx files,
and this must be reflected in annotation pre-processing.
- Value [2011-10-18] Improve evaluation of logic when option
-val-signed-overflow-alarms is active.
-* Value [2011-10-17] Fixed crash when a library function is called in
a state where the function's precondition cannot be true.
-* Value [2011-10-10] Fixed spurious alarm \valid(p) in *p = e; when e is
completely invalid. Soundness was not affected (the
alarm for whatever made e invalid was present).
###############################################################################
Open Source Release 7.0 (Nitrogen-20111001)
###############################################################################
- Rte [2011-10-07] No longer position 'Don't know' statuses
- Value [2011-10-07] New alarm for left shift of negative values.
Minor other changes related to shift operation alarms.
o*! Rte [2011-10-06] Correct plug-in name for dynamically registered
RTE functions.
-* Kernel [2011-10-06] Warn when the plug-in specified by -load-module
or -load-script is not found (used to remain silent)
-!* Kernel [2011-10-06] Do not normalize Pre in Old, especially where Old
is not allowed.
- Value [2011-10-01] Do not continue evaluating successive 'requires'
or 'ensures' clauses if one of them is false.
- Kernel [2011-10-01] New kind of command-line parameter, for commands
that do heavy output. Used for Value, Pdg and Metrics.
-* Cil [2011-09-30] Correctly handle casts in switch. Fixes #961.
-! Rte [2011-09-30] Option -rte-precond is not entailed by -rte-all
anymore (precontion annotations must now be required explicitly).
-* Aorai [2011-09-30] Generation of loop invariant for intermediate
counter + fixes various issues
-! Slicing [2011-09-30] Option -slice-print is now deprecated: use instead
<normal slicing command> -then-on 'Slicing export' -print
- From [2011-09-29] Display results function by function, instead of
as one big block (may lower memory consumption considerably).
- Value [2011-09-27] New option -remove-redundant-alarms for removing
redundant alarms. This was previously done by default. Use this
option if you are going to inspect alarms emitted by Value.
-* Kernel [2011-09-26] Treat long bitfields the same way as gcc and clang.
Fixes #!959.
-* Kernel [2011-09-26] New exception for Ast.UntypedFiles.get when no
untyped AST is available. Fixes #954.
- Value [2011-09-23] New alarm, for programs that do not respect
C99 6.5.16.1:3 (overlapping assignment from lvalue to lvalue).
Partially supported (not emitted in some cases).
-* Kernel [2011-09-23] Fixes various performance issues when parsing very
large functions. Fixes #!965.
- Value [2011-09-23] Improved precision of if (x!=c) when the value set
of x is an interval of 9 elements.
-* Slicing [2011-09-23] Use correct function during generation of
sliced project. Fixes #!950.
o* Kernel [2011-09-22] Copy visitor creates new kf before visiting a
function, allowing to use it for creating Property.t items in
the new project during visit (fixes #!942).
-* Value [2011-09-22] Much more clever when interpreting logic terms,
including those containing \old (eg. formals in postconditions)
- Value [2011-09-21] Raised cut-off limit between sets and intervals
from 7 to 8 elements.
- Value [2011-09-21] New informative message when not using.
-val-signed-overflow-alarms "2's complement assumed for overflow"
o! Value [2011-09-18] Changed the representation of Ival.t. If an
external plug-in matches "Ival.Set s", a simple fix is
to add "let s = Ival.set_of_array s in" as first line of
that case.
- Value [2011-09-16] Improved precision of &.
- Value [2011-09-16] Improved precision when using -all-rounding-modes.
o Kernel [2011-09-09] Map_common_interface to have a merge function for
Ocaml < 3.12.
o Kernel [2011-09-09] Quadruple datatype.
- Value [2011-09-09] Better message when interpretation stops
for a function argument.
- Pdg [2011-09-06] Pdg can now be saved on disk.
-* Logic [2011-04-20] Fix bug #!501: volatile clauses relative to
partially volatile lvalues are handled by the kernel.
- Pdg [2011-09-03] Improved time and space complexity on big functions.
- Cil [2011-09-02] Add support for GCC specific cast from field of
union to union
-* Cil [2011-09-02] Fix merging bug (#!948).
-* Slicing [2011-09-02] Fix incorrect simplification of single-statement
block in presence of label.
- Value [2011-09-02] Wide strings more supported.
- Kernel [2011-09-02] Improve space complexity of function stmt_can_reach.
- Semantic Constant Folding [2011-09-02] All options are prefixed by "scf".
Use -scf-help for the details. Fixed #!946.
Compatibility is preserved thanks to option aliases.
- Value [2011-08-30] Remove non-relevant variables from the 'Modifies'
clauses of the GUI.
o! Kernel [2011-08-30] Add parameter ~with_locals to Db.accept_base
(prior this, ~with_locals was implicitly false)
o! Value [2011-08-30] Signature change in CilE: plugins that want to
emit Value analysis alarms must define their own emitters.
o! Value [2011-08-30] Add some missing ~with_alarms arguments, notably
to offsetmaps copy and paste.
o! Kernel [2011-08-29] Export datatype Varinfo.Hptset. Signature change
in functor Abstract_interp.Make_Hashconsed_Lattice_Set.
- Metrics [2011-08-26] New command-line options to compute the functions
potentially called from a given function, and the percentage
of functions analyzed by the value analysis.
- Value [2011-08-25] Improve handling of assigns in library functions.
- Occurrence [2011-08-25] Better pretty-printing: do not display
internal ids anymore.
-! Value [2011-08-24] Improve behavior in presence of errors during
the computation of the initial state. Allow non ISO global
initializers using the value of constant globals defined earlier.
o! Kernel [2011-08-23] Getters of Dynamic.Parameter now get an extra
argument of type unit. May improve efficiency a lot.
-* Kernel [2011-08-23] Fixes visitor bug + properly refresh ids of
properties in code transformation (in particular loop unrolling).
-* Kernel [2011-08-15] Add parameter ~declarations to
Globals.FileIndex.get_functions. Prevent duplication bug
in properties navigator of the GUI.
- Inout [2011-08-12] Operational inputs and outputs are now more precise
for library functions: assigns clause are evaluated at each call.
o! Inout [2011-08-12] Interface change. Non_contextual renamed to
Cumulative_analysis.
-* Cil [2011-08-10] Fix conversion bug for f(i++) or f(++i) when i has
size less than int, and f expects an int (bug #911).
- Value [2011-08-10] Loop invariants are now used to improve analysis.
- Value [2011-08-09] Uses "complete behaviors" information.
- Scope [2011-08-09] "Show Defs" is now an interprocedural analysis.
o! Value [2011-08-09] Module Cvalue_type renamed to Cvalue.
Module Relations_type removed. Use Cvalue instead.
- Value [2011-08-04] Postconditions containing \old are now handled.
- Kernel [2011-08-04] Current pragmas no longer give rise to code
annotations (as they do not contain anything that can be proven).
-! Gui [2011-08-04] Improve labels under the icons of the toolbar. Smart
constructors in Menu_manager now require a label and a tooltip.
o Kernel [2011-08-04] Add Kernel.Unicode.without_unicode, which applies
a function without upsetting the Unicode option in the gui.
-* Impact [2011-08-04] Correct a journalisation bug in gui mode.
- Value [2011-08-01] More precise when an alarm is emitted in a loop.
o! Kernel [2011-08-01] Signature of Plugin renamed for consistency.
Use carbon2nitrogen for automatic translation.
o! Kernel [2011-08-01] Annotations.replace and
Globals.Annotations.replace_all are removed.
o! Kernel [2011-08-01] Add IPLemma, IPNotacsl and IPConjunction as new
constructors of Property.t; remove IPBehavior.
- Kernel [2011-08-01] Better pretty printing of lists of any elements
o! Kernel [2011-08-01] Properties_status is now called
Property_status. Fully new interface.
o! Cil [2011-08-01] Removing types about validity status from the AST.
Use module Property_status instead.
o Kernel [2011-07-25] Adding option ~dkey to Log.debug functions.
See Log.Messages for details.
o! Kernel [2011-07-22] Modification of Log.print_on_console. No more
based on Format.kfprintf to avoid deadlock when
error are raised by plugin pretty printers.
-* Logic [2011-07-22] Fixes bug #885 (wrong insertion of cast).
-* Logic [2011-07-21] Fixes bug #!887 (merging logic constants).
o* Kernel [2011-07-20] Ensures that a unique kf is generated per function
in each project, avoid using kf for project A in project B.
-! Kernel [2011-07-18] Better handling of comments with -keep-comments
and new API. See Cabshelper.Comments and Globals.get_comments_*
o! Aorai [2011-07-12] Redefinition of internal structures before
enabling Ya extensions for sequences
o! Value [2011-07-11] Add argument "exact" to Lmap.paste_offsetmap (which
was preciously supposed to be always true).
-* Cil [2011-07-06] Correct obscure Cil bug linked to the removal of
trivial unspecified sequences or blocks. Fixes bug #882.
- Value [2011-07-05] Option -val-builtin: experimental support for
builtins that can fail (by calling a fallback C function).
- Value [2011-07-04] New builtin Frama_C_dump_each_file, which dumps
the entire memory state into successive files.
o* Logic [2011-06-29] Fixes bug #751 (Cil.lconstant now returns terms of
type integer and not int).
- Metrics [2011-06-27] Improves efficiency of metrics computation.
o! Cil [2011-06-24] Improve performances of Cil_datatype.Typ.{compare,
equal, hash}.
- Cil [2011-06-22] Cache results of offsets computations.
-* Logic [2011-06-22] Fixed issue #!866 (merging specs included twice)
o Kernel [2011-06-16] Exporting Property_status.self state
o! Kernel [2011-06-16] Dynamic.load_module searches in plugin path as
advertised in its documentation
o*! Cil [2011-06-14] Support for large constants in programs. My_bigint
is now used instead of Int64.t in the AST. Fixes #!858.