Newer
Older
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.
o* Kernel [2011-06-10] Fix dynamic access to function [is_default] of
parameters.
o! Kernel [2011-06-10] New way for handling abstract type in the type
-* Value [2011-06-09] Remove some uneeded warnings when comparing function
pointers with NULL. Fixes bug #!855.
-* Kernel [2011-06-09] Correct syntactic loop unrolling in presence of
switch. Fixes bug #861.
o! Kernel [2011-06-09] Remove function CilE.update_gotos.
o! Kernel [2011-06-09] new function Kernel_function.set_spec which
must be called whenever the spec of a kf is modified.
o! Kernel [2011-06-08] Remove Kernel_datatype (merge with Cil_datatatype).
o! Kernel [2011-06-07] Most types of module Property are now private.
Use smart constructors instead.
o Kernel [2011-06-07] New function Dynamic.is_plugin_present.
-* Cil [2011-06-07] Fixes bug #857 (problem with some C enum value and
Ocaml 32 bits 3.11.0).
-* Logic [2011-06-06] Normalization of assigns clause: \result and
\exit_status only appear if a \from is specified.
Fixes #!557, #!845
o! Kernel [2011-06-06] Structural_descr.pack is now a private type.
Use smart constructors instead.
- Value [2011-06-04] Emit \pointer_comparable alarm for unspecified.
equality test between literal strings such as "foo" == "foo".
- GUI [2011-06-03] Double-clicking on a warning now displays the
pretty-printed source location
o! Value [2011-06-03] Functions valid_* now take an argument ~for_writing
Pass true when the lvalue being considered is used for
writing in the program. Pass false when unsure.
- Value [2011-06-03] Literal strings are now read-only.
- Value [2011-06-03] More aggressive state reduction when emitting
pointer_comparable assertions. Use option
-undefined-pointer-comparison-propagate-all if you liked
the old behavior better.
o GUI [2011-06-02] Menu_manager now support check menus and toggle
- Value [2011-06-02] New option -no-val-show-progress
- Cil [2011-06-02] Pretty-printing lval and term_lval the same way
- Cil [2011-06-01] Normalization of lval: T+1 ==> &T[1] when T is in
fact an array (implies *(T+1) ==> T[1])
-* Logic [2011-05-31] can have a local binding for a predicate (even
a constant one) without spurious warnings from typechecker.
(fixes #!848)
+ Ptests [2011-05-31] Add -xunit option to support JUnit like output.
o Kernel [2011-05-31] Cil_datatype.LogicLabel implemented
o Kernel [2011-05-31] New function File.new_machdep in order to
register a new machdep dynamically.
- Dominators,Postdominators [2011-05-31] No feedback by default. Use
-dominators-verbose 2 or -postdominators-verbose 2 if you need it.
-* Project [2011-05-31] Fix sharing bug when copying project.
- Value [2011-05-31] Alarms may pretty print the abstract value culprit
for the potential violation. This is particularly informative for
certain alarms.
- Cil [2011-05-30] Support for &"constant_string" in parser.
-* Kernel [2011-05-29] Fixed macros in limit.h.
- GUI [2011-05-28] Support to display the state of the absolute memory.
o! Kernel [2011-05-26] Module Parameters is dead. Each module
corresponding to a parameters is moved to Kernel. Module
Parameters.Dynamic is now Dynamic.Parameter while
Parameters.get_selection_context is now
Plugin.get_selection_context. You can use the script
bin/carbon2nitrogen to perform the translation (almost)
automatically.
- Value [2011-05-24] Option -val-after-results to control the recording
of post-statement states. Active by default in the GUI.
-* Cil [2011-05-24] Fixes bug #832 (spurious warning for read/write
accesses in undefined order)
o! Logic [2011-05-24] Add possibility to cast integer to C integral
type when type-checking (Changes parameter of Logic_typing.Make)
o! Kernel [2011-05-24] Kernel_function.find_return may now raise
exception Kernel_function.No_Statement.
-* Cil [2011-05-17] Fixes bug #771 (spurious warning for read/write
accesses in undefined order).
-* Kernel [2011-05-13] Support GCC like typing of enums.
- GUI [2011-05-13] Add history for navigating source code.
o! GUI [2011-05-13] Signature change for Filetree#add_select_function,
Filetree#select_global and Menu_manager.entry. Deprecate
Design.apply_on_selected.
-* Kernel [2011-05-12] Fixed typing of bitfields whose size is equal to the
size of int (bugs #823, #817).
-* Value [2011-05-11] Fixed undocumented builtin is_base_aligned.
-* Value [2011-05-11] Fixed bug when bitfield receives the result of
a function call (bug #819).
- GUI [2011-05-10] Menu to configure what is displayed in the filetree.
-* Logic [2011-05-08] Fixed overloading resolution (fixes bug #655).
-* Logic [2011-05-06] Fixed issue with -pp-annot (fix bug #691 and #812).
o Kernel [2011-05-05] Kernel now accepts declarations as main entry point.
- Aorai [2011-05-04] Automaton is handled by contract of leaf functions.
o Cil [2011-05-04] Various smart constructors and ast helper functions.
-* Cil [2011-05-04] Fixes wrong precedence of not in predicate when
pretty-printing.
- GUI [2011-05-04] Automatically show the main function at launch.
- GUI [2011-05-04] Hide empty plugins columns in the filetree. Add
support for hiding globals entirely.
o! GUI [2011-05-04] Signature change for Filetree#append_pixbuf_column.
o! Kernel [2011-05-03] Remove Db_types module. All types are now in
Cil_types. Moved type Alarms.t to Cil_types.alarm.
-* Kernel [2011-05-02] Support for GCC packed and aligned attributes and
for GCC pack pragmas. Fixes #719.
-* Configure [2011-05-02] Fix bug #!262: --disable-plugin works for external
plugins compiled from within Frama-C kernel.
- Dataflow [2011-04-29] Improve precision of backwards dataflow algorithm
and of postdominators on 'if' with a missing branch
-* Pdg [2011-04-28] Better precision in the dependencies.
Fix bug #787, #789 and #802 : infinite loops creation in slicing.
o Value [2011-04-28] Changed representation of bases for literal strings
in preparation of related checks.
o Postdominators [2011-04-27] Add Db.PostdominatorsValue: postdominators
taking into account value analysis results
-* Value [2011-04-24] Fixed crash for high values of -subdivide-float-var
- Value [2011-04-24] Improved results for operation % by zero.
Removed message about binary operators raising exceptions.
o Value [2011-04-24] Defunctorized Lattice_Interval_Set.
-* Logic [2011-04-20] Fix bug #761: adding \old in ensures clause for
parameters does not capture terms in associated offset.
-* Logic [2011-04-20] Fix bug #!501: volatile clauses are
handled by the kernel.
-* Slicing [2011-04-20] Fix bug #799: missing label in sliced program.
-* Value [2011-04-17] Fix bug #798: calls to functions that
return a value with latent conversion.
-* Cil [2011-04-15] Fix bug #785: promotion between long long and an
unsigned same-sized type.
-* Cil [2011-04-14] Fix bugs #780 and #791: use ids unique
between projects for varinfos, statements and expressions.
o*! Cil [2011-04-14] Remove incorrect Cil_const.Build_Counter; use
State_builder.SharedCounter instead.
-! Value [2011-04-14] Use hash-consed sets of statements, making
many analyses faster and leaner for large functions or idioms
that make functions large at normalization
(e.g. large initialized local arrays).
-* Kernel [2011-04-14] Fix 'make clean' of plug-ins.
-* Kernel [2011-04-13] Fix bug #769: merging issue for declared struct.
o* Kernel [2011-04-13] Fix bug #790: AST integrity checker issue.
-* Pdg [2011-04-13] Fix bug #787 but leads to less precise dependencies.
-* Slicing [2011-04-02] Fix bug #786: missing label in sliced program.
-* Value [2011-04-12] Correctly emit \pointer_comparable(...) alarms.
-* From [2011-04-11] Fix #781: handling of function calls with an
implicit cast for the assignment of the result.
o Makefile [2011-04-08] Add target to launch the tests of a specific
dynamic internal plugin from Frama-C's main Makefile.
-* Aorai [2011-04-08] Existing assigns are augmented with the locations
corresponding to the instrumentation of the automaton.
- Value [2011-04-05] Each precondition can get a specific validity status.
-* Kernel [2011-04-01] Fixed bug #770 and #769, part 1. Fixed typo in
anonFieldName (was annonFieldName).
-* Kernel [2011-04-1] Fixed bug #775. Large octal and hexadecimal constants
are now correctly typed.
-* Occurrence [2011-04-01] Fixed bug when journalising.
-* Slicing [2011-04-01] Fixed bug #774: journalisation works again.
o Kernel [2011-03-30] Removed type Log.source. From now on all locations
have type Lexing.position.
- Kernel [2011-03-30] Some messages may be printed several time for
the same line if they refer to different columns.
-* Value [2011-03-30] Fixed bug #689. Each postcondition can get a
specific validity status.
-* Impact [2011-03-30] Bug fixed when plug-in `Security_slicing'
cannot be loaded or is incompatible with Impact.
-* Impact [2011-03-30] Bug fixed with '-impact-pragma f' on an unknown
function f.
-* Security_slicing [2011-03-30] Fixed bug #768 about exception raised when
analysing variadic functions. A warning is now emitted:
the function is ignored by the analyzer, thus the result is
potentially incorrect.
o! Kernel [2011-03-29] Alternative signature for dataflow initial state.
A few IntHash replaced by Stmt.Hashtbl.
- Users [2011-03-28] Calls to this plug-in are now written in the journal.
-* Value [2011-03-26] Some floating-point alarms could be printed several
times. Fixed.
o! Kernel [2011-03-25] get rid of bin/sed_inplace (use ISED from
share/Makefile.common where needed, which was the recommended
way from the beginning).
o* Kernel [2011-03-25] Makefile.plugin and .dynamic more robust wrt
external plugins (can make doc clean depend more easily;
fixes bug #754, improves bug #742).
-* Logic [2011-03-24] \at(t,L) when t is a C array is now a logic array
whose content is the one of t at L, not the address of the first
element of t (which stays the same between L and Here anyway).
partial fix of bug #761.
- Kernel [2011-03-24] \at(p,Old) is pretty-printed as \old(p).
o! Cil [2011-03-24] AST changed: removing Told and Pold constructs.
o! Kernel [2011-03-11] Following items are now deprecated:
function Kernel_function.pretty_name: use Kernel_function.pretty
module UseUnicode: use module Unicode.
o! Kernel [2011-03-11] Remove several kernel functions:
Ast_info.pretty_vname: use Cil_datatype.Varinfo.pretty_vname
Cil.print_utf8: use module Parameters.UseUnicode-
Clexer.keep_comment: use module Parameters.PrintComments
Cabshelper.continue_annot_error_set:
Cabshelper.continue_annot_error_set: use
Parameters.ContinueOnAnnotError.off
all Cil, Cilmsg and CilE functions for pretty printing: use Kernel
ones instead.
- From [2011-03-11] Display name of called function when displaying
results of option -calldeps.
o!* Logic [2011-03-11] Implementation of statement contracts for function
behaviors.
-* Value [2011-03-11] Fixed crash with ACSL assertions involving
floating-point variables (bug #752).
-* Logic [2011-03-10] Fixed bug #744 (comparison between arithmetic types
is done in the smallest possible type).
-* Kernel [2011-03-10] Bug fixed in File.create_project_from_visitor
potentially impacted programs transformation.
-* Kernel [2011-03-10] Bug fixed in pretty printer.
(incorrect precedences leading to missing parenthesis).
- Kernel [2011-03-09] Big integers can now be displayed using hexadecimal
notation.
- Value [2011-03-06] Improved option -subdivide-float-var when used
without -all-rounding-modes. Improvement marginal for
double computations and significant for float ones.
o! Cil [2011-03-04] AST changed: 'a before_after type is deleted. All
annotations are now attached before.
-* Value [2011-03-04] Fixed correctness bug when bitfield initializer
exceeds range (bug #721) (jrrt).
o! Value [2011-03-02] Minor interface changes in Value. Replace
some meaningless kinstr by stmt, and make the callbacks lazy.
o! From [2011-03-02] Minor interface changes in From. Replace
some meaningless kinstr by stmt, and make the callbacks lazy.
-! Cil [2011-03-02] Fixed #720 (incorrect simplification of switch).
- Kernel [2011-03-02] Better error message when plug-in crashes on
loading (bts #737).
o Kernel [2011-03-02] New function File.create_rebuilt_project_from_visitor
- Cil [2011-02-24] Implement precise dataflow on switch
constructs. As side effect, improve precision of value analysis.
o* Kernel [2011-02-24] Fixed bug #727 (visiting a GFun spec in frama-c
visitor was not done in the appropriate context).
o* Ptests [2011-02-24] Ptests adds filename of current test before the
options given to frama-c (see #736).
- Aorai [2011-02-24] Deterministic automata.
-* Aorai [2011-02-24] Fix issue in translation of guards + better error
messages.
o! Inout [2011-02-23] Db.InOutContext becomes Db.Operational_inputs.
- Inout [2011-02-23] Correctness in presence of recursive calls.
See issue #733.
- Value [2011-02-23] Improved informative messages about addresses
of locals escaping their scope.
o! Kernel [2011-02-22] Change semantics of ChangeDoChildrenPost for
vstmt_aux. See developer's manual for more precision.
- Value [2011-02-22] Take Flush-To-Zero possibility into account
for single-precision floats.
- Kernel [2011-02-22] Exit status on unknown error is now 125. 127 and
126 are reserved for the shell by POSIX.
o!* Kernel [2011-02-21] Extlib.temp_file_cleanup_at_exit and
Extlib.temp_dir_cleanup_at_exit may now raise exception
Temp_file_error. They may raise an unspecified exception before.
-* Value [2011-02-20] Fixed bug #732: Synthetic results were partial
when -slevel was set not high enough to unroll loops
completely.
- Inout [2011-02-20] Improved messages in presence of recursive calls
o! Kernel [2011-02-18] Bts #729: calling function Plugin.is_visible
(resp. Plugin.is_invisible) forces to display
(resp. prevents from displaying) the corresponding
parameters in an help message.
o! Kernel [2011-02-18] module Service_graph: function entry_point in
input and output of functor Make now returns an option type.
- Syntactic Callgraph [2011-02-18] Fixed issue #723: syntactic callgraph
does not require an entry point anymore. If no entry point,
services are less precise yet.
-* Cil [2011-02-17] Fixed bug #725 (type-checking && operator).
- Inout [2011-02-17] Improved precision of the computation of
operational inputs in presence of function calls.
-* Logic [2011-02-17] Fixed bug #714 about lexing ACSL characters and
o Cil/Logic [2011-02-16] New functions Clexer.is_c_keyword and
Logic_lexer.is_acsl_keyword.
-! Cil [2011-02-16] Enumerated constants are kept in the AST.
-* Aorai [2011-02-16] State names used as enum constant are checked to be
admissible fresh C identifiers.
-* Value [2011-02-15] Fixed bug when passing struct as argument to
function with a big-endian target architecture.
- Value [2011-02-15] Uniformized message displayed when no information
is available for a function.
- Logic [2011-02-14] Added support for bitwise operators --> and <--> into
ACSL formula.
-* Slicing [2011-04-02] Fixed bug #709: missing statements in sliced program.
-* Value [2011-02-14] Fixed bug when passing bitfield
as argument to function. (jrrt)
-* Value [2011-02-12] Fixed forgotten warning when passing completely
undefined lvalue as argument to function. (jrrt)
-* Value [2011-02-12] Fixed correctness bug involving nested structs
-* Value [2011-02-12] Fixed crash when passing invalid argument to
function, found by John Regehr using random testing (jrrt).
-* Value [2011-02-09] Fixed representation of unknown single-precision
floats in initial context (it used to be the same as for
an unknown double).
-* Value [2011-02-09] Changes related to 0., +0., -0., sort of thing.
Unwarranted loss of precision fixed.
#########################################
Open Source Release 6.2 (Carbon-20110201)
#########################################
- WP [2011-02-07] Plug-in WP removed from kernel-releases (now an
independent plug-in).
- Logic [2011-02-04] Mentioning a formal on the left-hand side of an
assigns clause is now an
error when type-checking logic annotations.
o! Logic [2011-02-04] Refactoring of assigns and from AST representation
and of Property.identified_property.
- Value [2011-02-04] Changes in Frama_C_memcpy built-in. Still not
- Value [2011-02-04] Is is now possible to call Frama_C_show_each
without ..._x.
- Value [2011-02-04] Generate independent assertions for signed
overflow and signed underflow. In many cases only one is
generated (win!).
o! Value [2011-02-02] Renamed copy to copy_offsmap in Offsetmaps.
The name "copy" clashed with Datatypes.
o Kernel [2011-02-01] New syntactic context for memory accesses with
user-supplied validity range.
+ WP [2011-01-31] Option -wp-warnings to display additional
informations for 'Stronger' and 'Degenerated' goals.
+ WP [2011-01-24] Option -wp-split-dim <n> to limit spliting
up to 2**n sub-goals (see -wp-split option).
-! Kernel [2011-01-27] Handle errors better when they occur when exiting
Frama-C. Slight semantic changes for exit code:
- old code 5 is now 127;
- code 5 is now: error raised when exiting Frama-C normally;
- code 6: error raised when exiting Frama-C abnormally.
- Kernel [2011-01-27] Improve performance on platform with dynami.c
loading. Mainly impact value analysis
(for developers: improve efficiency of Dynamic.get).
- Value [2011-01-25] Change in initial states generated by -lib-entry
Much smaller. Perhaps more representative.
+ WP [2011-01-24] When -rte-precond is not used,
wp generates a separate proof obligation for each call site.
-! Configure [2011-01-24] Frama-C does not require Apron anymore (Why
does for Jessie). Thus fix bug #647.
- Value [2011-01-22] More aggressive handling of if(x>e) where x has
type double.
o* Kernel [2011-01-20] Fix bug #677. As a side-effect, function
Plugin.add_alias is now deprecated and replaced by
Plugin.add_aliases.
o Kernel [2011-01-21] New function in API: