Newer
Older
###############################################################################
# Preliminary notes: #
# ------------------ #
# Mark "-": change with an impact for users (and possibly developers). #
# Mark "o": change with an impact for developers only. #
# Mark "+": change for Frama-C-commits audience (not in html version). #
# Mark "*": bug fixed. #
# Mark "!": change that can break compatibility with existing development. #
# '##nnn' : Public Gitlab (pub/frama-c) issue
# '#@nnn' : Gitlab frama-c/frama-c issue #
# For compatibility with old change log formats: #
# '#nnn' : BTS entry #nnn (OBSOLETE) #
# '#!nnn' : BTS private entry #nnn (OBSOLETE) #
# '#?nnn' : OLD-BTS entry #nnn #
###############################################################################
###############################################################################
Open Source Release <next-release>
###############################################################################
o! Kernel [2025-01-31] Use a record to represent `Cil_types.typ` with two
fields `tnode` and `tattr` for its `typ_node` and `attributes`.
- Ivette [2025-01-23] New sidebar listing functions and global variables
for each source file.
- Eva [2025-01-23] Rename warning key `invalid-assigns` to
`assigns:invalid-location`
- Eva [2025-01-23] All warnings about missing assigns or \from clauses
are now emitted as errors by default, with the new warning key
`assigns:missing`.
- Kernel [2025-01-17] New option -memory-footprint to configure the memory
usage of analyses.
o! Kernel [2024-12-20] Remove Cabs.SEQUENCE statement
###############################################################################
Open Source Release 30.0 (Zinc)
###############################################################################
-! Kernel [2024-11-04] Add partial parsing support for statement/label
attributes
- Eva [2024-10-25] Never emit alarms on pointer conversions to intptr_t
or uintptr_t.
- Kernel [2024-10-15] Warn when encountering an unknown attribute
o! Kernel [2024-10-08] introduce logic type Lboolean and constants
- Kernel [2024-10-08] Asm contracts can now have \initialized ensures.
See option -asm-contracts-ensure-init
- Kernel [2024-10-08] Option for converting stmt contracts into
ACSL assert for plug-ins with incomplete stmt contract support
See option -inline-stmt-contracts
- Ivette [2024-10-07] Complete rewriting of the callgraph, improving its
readability and usability and adding new features: filtering
and selecting functions, showing alarms by function, and more.
- Ivette [2024-10-04] Show the "Source Code" view at first launch.
-* RTE [2024-10-04] Fixed missing assertion on modulo signed overflow.
-* Eva [2024-10-04] Fixed missing signed overflow alarm on modulo.
- Eva [2024-10-04] Fewer false alarms of signed overflow on divisions.
o! Kernel [2024-09-30] ACSL extensions are now associated to a plug-in,
allowing the registration of several extensions with the same name
from different plug-ins
- Eva [2024-09-26] Removes approximation messages "more than N elements
to enumerate".
- Kernel [2024-09-23] Support for ACSL modules.
- Kernel [2024-09-23] Extension for importing external modules in ACSL
o Kernel [2024-09-23] API to register ACSL extern modules import functions
o! Kernel [2024-09-23] Move functions for finding logic types, functions,
predicates and constructors from Logic_typing to Logic_env.
- Kernel [2024-09-20] New warning category typing:implicit-int, allowing
to omit type specifiers in declarations (default is error).
o! Kernel [2024-09-13] Pragma nodes in the AST have been removed
- Slicing [2024-09-13] -slice-pragma is now -slice-annot
- Slicing [2024-09-13] `slice pragma <elem>` is now `slice_preserve_<elem>`
- Impact [2024-09-13] -impact-pragma is now -impact-annot
- Impact [2024-09-13] `impact pragma stmt` is now `impact_stmt`
- Kernel [2024-09-03] Place noreturn attribute on types instead of vars
- Alias [2024-08-22] no longer classify virtually all casts as unsafe
o! Kernel [2024-08-08] New Machine module to manage theMachine and machdeps.
Cil functions related to theMachine are deprecated.
-! Kernel [2024-08-08] New minimal OCaml version: 4.14
o! Kernel [2024-08-08] Plug-ins Dominators and Postdominators have been
removed and replaced by the Dominators module in the kernel.
- Eva [2024-08-06] Support for 'calls' ACSL extension
o Kernel [2024-08-05] Added new modules `Cache_dir` and `State_dir`
and additional facilities to build sub-directories in these
-! Kernel [2024-08-05] Changed `Config_dir` module signature, and
behavior on macOS and Windows
o! Kernel [2024-08-05] Changed `Share` module signature
o Kernel [2024-07-30] mapNoCopy moved to Extlib and deprecated in Cil
o Eva [2024-07-31] Export profiling information about the analysis
performance via the new module Eva_perf in Eva.mli.
- Ivette [2024-07-26] New flamegraph component to visualize Eva analysis
time by C functions, in the "Eva Summary" view by default.
- Ivette [2024-07-19] New left sidebar to configure and run Eva analyses.
-* Eva [2024-07-18] Fixes number of sure alarms by function shown in
Ivette.
-* Eva [2024-06-21] Fixes possible unsoundness when writing 0 on a set of
contiguous and non-overlapping locations containing a value with a
different size or alignment than the write.
- Ivette [2024-06-12] Include global initializations in the list of writes
of a global variable.
- Ivette [2024-06-04] In the sidebar, global variables and types are sorted
by name.
- Kernel [2024-05-20] New ACSL extension loop unfold (replaces loop pragma UNROLL)
-! Kernel [2024-05-20] Removed loop pragma UNROLL annotations
o! Kernel [2024-05-20] Renamed module Unroll_loop into Unfold_loop
- Ivette [2024-05-17] Improved colored status bullets in AST view.
###############################################################################
Open Source Release 29.0 (Copper)
###############################################################################
- Ivette [2024-05-03] Fix performance issues on large codebases.
- Kernel [2024-04-30] new warning category too-large-array, allowing to
use array > SIZE_MAX by changing its status (default is error).
- Eva [2024-04-26] Improve builtins memcpy, memmove and memset when
arguments are imprecise.
o Dev [2024-04-22] Remove frama-c-build-scripts.sh; add a section in
the user manual about how to manually replace it.
-! Kernel [2024-04-19] Change format of custom_defs field in machdep schema
and allow #undefining builtin macros in the command-line.
- Eva [2024-04-18] Remove support for deprecated WIDEN_HINTS loop pragma.
Use ACSL extension "widen_hints" instead.
o Kernel [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix
- Alias [2024-04-16] Fix analysis results in the presence of structures.
Complete rework of the API. Improved documentation. Fix stack
overflow in case of a cyclic graph.
- Eva [2024-04-10] Reduce pointer values according to ACSL predicate
\base_addr.
-* Eva [2024-04-10] Fix a crash when running successive analyses using
the -eva-domains-function parameter.
- Ivette [2024-04-09] New notifications at the bottom-right of the main
window. Some components are highlighted in the bottom bar when
they are updated but are not currently visible.
- Kernel [2024-04-04] Avoid ambiguous pretty-printing when C labels match
the name of an ACSL built-in label (fix #@1359)
-! Kernel [2024-04-02] Systematically abort when a function is redeclared
with an incompatible type, instead of trying to finish
type-checking, preventing misleading error msgs after the first
report. IncompatibleDeclHook has thus been removed from the API.
o Kernel [2024-04-02] Annotations.{fold,iter}_behaviors now pass full
behaviors to the iterated function. To iter on fragments split by
behavior and emitter, use {fold,iter}_behaviors_by_emitter.
- Eva [2024-03-29] Reduce pointer values according to ACSL predicate
valid_string and valid_read_string.
o! Kernel [2024-03-29] Refactor current location handling mechanism
o Ivette [2024-03-29] Upgrade to node 20 and electron 28. Use vite instead
of webpack. Upgrade many dependencies.
- Ivette [2024-03-28] In the Eva values table, show values before/after
statements with annotation, as values can be reduced after them.
- Ivette [2024-03-26] Add feedback when the user requests the evaluation
of a custom term.
- Kernel [2024-03-26] Introduce \plugin:: prefix for ACSL extensions,
unknown extensions can be safely ignored when the plug-in that
handles them is not available
- Ivette [2024-03-20] Add shortcut to select next/previous tab.
- Ivette [2024-03-14] Complete redesign of the main view. Components and
views can be selected in the left sidebar (the right sidebar has
been removed). The top bar contains tabs of the currently selected
views. Components can be docked in the bottom bar, to be shown or
hidden on a simple click.
-* Variadic [2024-03-07] Make sure that generated functions have fresh names
o! Kernel [2024-03-07] More coherent naming of functions determining if a
symbol is a Frama-C built-in.
- Eva [2024-03-04] Better reporting of imprecise "garbled mix" values
(resulting from imprecise or unsupported operations on addresses)
through more relevant messages and a compact summary at the end of
the analysis, enabled by default.
-* Kernel [2024-03-04] Accept conditional expr whose 2d and 3d operands
have type void, as per C11 6.5.15§3
-* Kernel [2024-02-22] When an array is declared with a fixed length l,
raise an error if l * sizeof(elem) > SIZE_MAX
o! Kernel [2024-02-22] Merged AST nodes TCastE and TLogic_coerce
o! Kernel [2024-01-29] Db is now mostly empty, the only remaining value is
Db.Main.extend which is deprecated and replaced by
Boot.Main.extend. Features related to asynchronous interactions
are now handled in module Async
- Ivette [2023-11-24] Global variables and types are listed in the sidebar.
Global variables can be filtered according to some criteria.
###############################################################################
Open Source Release 28.1 (Nickel)
###############################################################################
-* Kernel [2024-01-18] Fix Cil.isConstant on lvalues with offset.
-* Ivette [2024-01-11] Fix Ivette shell wrapper on macOS.
###############################################################################
Open Source Release 28.0 (Nickel)
###############################################################################
- Eva [2023-10-11] Optimization of the multidim domain.
-! Kernel [2023-10-09] Remove options -no-type and -no-obj and related
functions.
o! Kernel [2023-10-03] New mechanism for generating default specifications
- Kernel [2023-10-03] New options -generated-spec-mode and
-generated-spec-custom for configuring how default specifications
are generated
- Eva [2023-09-26] Support evaluation of simple \let bindings in
ACSL terms and predicates.
o! Kernel [2023-09-25] Remove Dynamic.Unloadable exception, useless since
the move from dynamic to static API for plug-ins.
- Alias [2023-09-07] New alias plugin that implements a points-to
analysis and an alias analysis based on Steensgaard's algorithm.
For these purposes it presents a more efficient (albeit less
precise) alternative to Eva. See src/plugins/alias/README.md.
- Kernel [2023-09-04] Fix #@846 (printing ACSL attribute in ghost code)
- Eva [2023-08-31] Adds warning key "garbled-mix" to all log messages
related to garbled mix (degenerated imprecise values).
o Eva [2023-08-05] Remove deprecated API Db.Value.
- Eva [2023-08-01] Print less messages unless -eva-show-progress is set.
o Kernel [2023-07-24] Expose Cil functions for type compatibility
-* Eva [2023-07-17] Fix unsound behavior on goto or switch statements
skipping local variable declarations: initialization alarms about
such variables are now properly emitted.
-* Eva [2023-06-21] Fix convergence issue on dynamic memory allocation
in some loops.
###############################################################################
Open Source Release 27.1 (Cobalt)
###############################################################################
- Kernel [2023-07-17] New frama-c-script wrapper for make_machdep.py
-* Ivette [2023-07-06] Fixes crash with multiple instances
-* GUI [2023-07-05] Fixes freeze when a plugin aborts during splash screen
-* GUI [2023-07-05] Fixes crash related to tags and undefined types
###############################################################################
Open Source Release 27.0 (Cobalt)
###############################################################################
-! Kernel [2023-05-15] New machdep mechanism, based on YAML files. A new
make_machdep.py script allows automatic machdep creation from a
C11-compatible (cross-)compiler.
- Eva [2023-05-04] The octagon domain can now infer relations between
any lvalues of integer or pointer types.
-* Ivette [2023-05-02] Ends properly frama-c process when Ivette is closed.
-* Ivette [2023-05-02] Custom views are correctly saved and reloaded.
-* Eva [2023-05-02] Fixes interpretation of Eva annotations at the end of
a block, and of multiple split annotations after a function call.
- Eva [2023-04-24] When possible, Eva shows the name of enumeration tags
instead of their integer values, in the log and the GUI.
- Aorai [2023-04-24] Allows comments in .ya automata files.
- Aorai [2023-04-24] Supports specification about floating-point variables.
- Ivette [2023-04-24] New callgraph component.
- Ivette [2023-04-07] The values table shows the status of uninitialized
and escaping variables.
- Eva [2023-04-05] Better display of large integer sets for high values
of the -eva-ilevel parameter.
- Ivette [2023-03-31] The values table shows values of function parameters.
- Ivette [2023-03-31] The values table can show the logical status of ACSL
predicates, and the values of C lvalues in these predicates.
o! GUI [2023-03-27] Remove GTK2 bindings. Only support GTK3 as of now.
- Ivette [2023-03-23] Improves function filtering in the left sidebar.
- Ivette [2023-03-23] Better display of dead and non-terminating statements.
-* Eva [2023-03-13] Fixes a soundness bug of the equality domain when
the same equality holds in two programs paths, but involving a
pointer pointing to different variables in the two paths.
- Kernel [2023-03-03] Deprecate option -c11 (now enabled by default).
- Ivette [2023-02-15] Shows information about C types in the Inspector.
- Eva [2023-02-06] Fixes performance issues on programs with too many
function calls (more than 20000 callsites).
-! Kernel [2023-01-25] Add support for C11's _Generic. Modifies Cabs AST.
-* Eva [2023-01-16] Fixes unsoundness of the bitwise domain on shifts
and casts on big-endian architectures.
- Eva [2023-01-12] Better partitioning splits on ACSL predicates.
###############################################################################
Open Source Release 26.1 (Iron)
###############################################################################
- Logic [2023-01-16] Accept \ghost attribute in logic annotations (##2638)
- Logic [2023-01-10] Fix issue in pretty-printing ranges (##2639)
###############################################################################
Open Source Release 26.0 (Iron)
###############################################################################
- Ivette [2022-10-26] After an Eva analysis with taint, the taint status of
lvalues is shown in the Inspector component and in Dive graphs.
- Eva [2022-10-25] The octagon domain can infer relations on the integer
conversion of floating-point variables.
- Ivette [2022-10-20] The installation of Frama-C provides an installation
script for Ivette: run 'ivette' once to finalize its installation.
- Kernel [2022-10-14] 'calls' ACSL extension is now registered in the
kernel and not WP
o! From [2022-10-13] Removed Db.From API: use the From API instead.
- Ivette [2022-10-13] Fixes some issues in the data dependency graphs
generated by the Dive plugin in the 'Dive Dataflow' component.
-* Eva [2022-10-10] Fixes a crash on recursive functions with an ACSL
specification without assigns clause.
-! Aorai [2022-10-11] Remove support for LTL and Promela input formats
- Kernel [2022-10-05] Support for ghost VLA and calls to builtins with
ghost arguments.
- Kernel [2022-10-03] -version prints a newline, -print-version does not.
o! Eva [2022-09-07] Deprecate Db.Value API: use the new Eva API instead.
- Kernel [2022-09-07] Improve error message for invalid options -D/-I/-U.
o! Configure [2022-07-28] Removed autoconf and configure
o! Makefile [2022-07-11] Removed Makefile, Frama-C is now built using Dune 3.x
o! Pdg [2022-07-01] Removed from Db. Use proper Pdg API instead.
- Ivette [2022-06-30] New component 'Eva States' that prints the internal
Eva domain states at a given statement for the selected marker.
- Ivette [2022-06-20] In the AST component, the user can fold/unfold ACSL
specifications, and preconditions are now shown at call sites.
- Eva [2022-06-17] Improved precision: arguments of calls interpreted by
an Eva builtin or with an ACSL specification can now be reduced in
the caller. This is especially useful on C asserts.
-* Eva [2022-06-06] Fixes a possible crash when -eva-subdivide-non-linear
and relational domains are enabled.
-! Kernel [2022-06-06] Remove journalisation.
- Eva [2022-05-11] Avoid false alarms of partially overlapping lvalue
assignments when writing a struct array from itself.
###############################################################################
Open Source Release 25.0 (Manganese)
###############################################################################
o Kernel [2022-05-03] Prototype of AST comparison between two versions
of the same program, via the new option -ast-diff.
- Eva [2022-05-02] Fixes stack overflow errors on very large C functions.
- Eva [2022-04-25] Improve the multidim abstract domain: it is now
more precise and more robust, it is able to infer simple array
invariants on some loops without unrolling, and has a new option
-eva-multidim-disjunctive-invariants to infer structures
disjunctive invariants.
o Kernel [2022-03-07] Known compiler builtins are no longer hardcoded in
OCaml, but defined via JSON files (in share/compliance).
o Kernel [2022-02-23] New visitor functions visitFramacFileFunctions
and visitCilFileFunctions to visit only function definitions,
for better performance.
o! Kernel [2022-02-23] Remove State_selection.Static (deprecated since
10 years, use directly State_selection instead)
-* Kernel [2022-02-22] Fix list of potential types for decimal
integer literal constants
* Kernel [2022-02-17] Reject programs using unsupported
vector_size attribute (fixes ##2573)
o Eva [2022-02-15] New API to run the analysis and access its results,
intended to replace the old API in Db.Value. It is more precise
as it uses all available domains to evaluate values and locations.
See file Eva.mli for more details.
* Kernel [2022-02-08] Reject array whose size is too big with a proper
error message instead of a crash (fixes ##2590)
o! Kernel [2022-02-19] Removed obsolete AST nodes IndexPI and Info
* Kernel [2022-02-08] Reject array whose size is too big with a proper
error message instead of a crash (fixes ##2590)
o! Kernel [2021-12-03] Remove unused AST node Dcustom_annot and field
fpadding_in_bits. Do not cache size of types in the AST but in
a dedicated table.
-* Logic [2021-11-30] Fix type of expressions whose value are functions
o! Kernel [2021-11-29] Integer.pretty does not have the optional argument
hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you
want to print integers in hexadecimal format.
###############################################################################
Open Source Release 24.0 (Chromium)
###############################################################################
-* Eva [2022-01-19] Always emits alarms about initialization, escaping
pointers and special floating-point values for the arguments of
calls to functions without body (or whose body is not analyzed),
even when -eva-warn-copy-indeterminate is unset.
- ACSL [2021-10-28] better type checks for volatile clauses
- Variadic [2021-10-26] translates printf/scanf calls even if formatting
string is not constant, warning that it will assume arguments
match the format.
- Kernel [2021-10-26] Support for C11's _Static_assert
- Libc [2021-10-26] Frama-C's libc #define _STDC_NO_COMPLEX as mandated by
ISO C11 for libraries without support for complex numbers
- Eva [2021-10-19] New options to allow states partitioning to survive
function returns: -eva-interprocedural-split for disjunctions
from split annotations, and -eva-interprocedural-history for
disjunctions from the -eva-partition-history option.
- Eva [2021-10-14] Supports the evaluation of ACSL set comprehension.
- Eva [2021-10-14] On a SIGINT signal (Ctrl-C), the analysis is stopped
but partial results are saved if option -save is set.
-* Eva [2021-10-12] Always checks the arguments of builtin calls for
alarms about initialization, escaping pointers and special
floating-point values, unless -eva-warn-copy-indeterminate is set.
-* Kernel [2021-10-11] Fixes crashes on C integer constants overflowing
ocaml integers.
- Eva [2021-10-06] Improves the precision of the octagon domain on
unsigned variables.
-* Eva [2021-10-06] Fixes a soundness bug in the octagon domain on
- Eva [2021-09-10] Improves the symbolic-locations domain precision.
- Kernel [2021-09-02] 0-sized flexible array members only available in
gcc_* machdeps, that now also support FAM in nested struct.
- Eva [2021-07-26] Removes the maximum limit of option -eva-ilevel.
- Eva [2021-07-26] New \tainted predicate to evaluate if the value of an
expression is tainted according to the taint domain.
-o Eva [2021-07-25] Changes the Domain_builder.Complete functor to
automatically build more abstract domain functions.
-* Eva [2021-06-24] Fixes a soundness bug of the bitwise domain with the
memexec cache.
-* Variadic [2021-06-23] Create a fallback specialisation if there is an error
while translating a variadic call so that no variadic call are
left in the AST after Variadic.
- Eva [2021-06-22] Reduction of "garbled mix" values by \valid and
\valid_read ACSL predicates.
- Eva [2021-06-15] New experimental multidim domain to improve analysis
precision on arrays of structures and multidimensional arrays.
-* Eva [2021-06-10] Fixes a crash in the octagon domain.
o Kernel [2021-06-10] New module Cil_builder, simplifies C and ACSL code
generation.
o Ptests [2021-06-03] Add new PLUGIN directive and new predefined macros.
- Eva [2021-06-01] Annotations split and dynamic_split can be applied
to logic predicates (in addition to terms).
- Eva [2021-06-01] New annotation dynamic_split, similar to split, but
separates the analysis w.r.t. the current value of an expression
instead of the value it had at the annotation point: the partition
can be changed at an assignment to ensure that the expression
always evaluates to a singleton in each analysis state.
- Eva [2021-05-20] New taint analysis via an experimental taint domain.
New annotations //@ taint … (for statements) and //@ taints … (in
function contracts) to initiate taint on lvalues.
Tainted properties can then be seen in the future GUI Ivette.
- Eva [2021-05-11] Support for ACSL predicate \is_infinite.
###############################################################################
###############################################################################
###############################################################################
Open Source Release 23.0 (Vanadium)
###############################################################################
-* Kernel [2021-04-26] Do not crash on _Alignof(void): accept or properly
reject, depending on machdep. Fixes pub/frama-c#2551
- Eva [2021-04-21] Partial support for recursion:
new option -eva-unroll-recursive-calls to precisely analyze the n
first recursive calls, before using the function specification
to interpret the remaining calls.
The unsound option -eva-ignore-recursive-calls has been removed.
-! RTE [2021-04-16] -rte-initialized takes a set of functions as
parameter (defaults to none)
- RTE [2021-04-16] No more initialization warnings for full structures
and unions reads. Initialization warnings for other
types *without* trap representation. Refer to the
documentation for more details.
-* Kernel [2021-04-16] Pretty prints array formals in their original form.
Fixes pub/frama-c#392
o! Kernel [2021-04-13] Removed deprecated function Filepath.pretty
o! Kernel [2021-04-13] Filepath directories functions now return
Filepath.Normalized.t, Frama-C configuration and plugin
configuration getters updated accordingly
o! Kernel [2021-04-09] Change the type of the measure from string to
logic_info in the variant AST node.
o Ptests [2021-04-08] FILTER directive reads the standard input and can be
chained.
- Eva [2021-04-02] Improved automatic loop unroll (-eva-auto-loop-unroll
option) of loops with goto or continue statements, or assigning
constant values to loop variants.
- Libc [2021-03-31] In math.h specifications, new behaviors for cases
creating NaN or infinite values. These behaviors are allowed or
forbidden according to the -warn-special-float option.
-* Kernel [2021-03-26] Raise an error if trying to merge a tentative
definition with a proper definition during linking
o Ptests [2021-03-25] Modify MODULE directive.
o Ptests [2021-03-24] Add new EXIT directive.
- Eva [2021-03-15] Slightly more precise evaluation of ACSL quantifiers.
o! Eva [2021-03-01] New signature for builtins, that are now registered
via Eva.mli instead of Db.Value.
- Eva [2021-02-18] New "audit mode" to track file checksums, correctness
options and enabled warnings, via options -audit-prepare and
-audit-check.
- Aorai [2021-02-09] New option for tracking last N states of the
automaton. Easier analysis of instrumented code with Eva.
o! Kernel [2021-02-08] Avoid triggering warning 16 (unerasable optional
argument). Implies changing some labeled functions' signatures.
- ACSL [2021-02-04] New admit annotations to express hypotheses to be
admitted but not verified by Frama-C.
- Eva [2021-01-28] Improved automatic widening thresholds (widen hints):
use constant modulo as threshold, and infer thresholds globally
for global variables.
- Eva [2021-01-21] Better interpretation of logical operators && and ||
(useful when option -keep-logical-operators is enabled).
o! Kernel [2021-01-15] Make cfields list optional. None means undefined,
empty struct allowed only in specific machdeps.
removed cdefined field
-* RTE [2021-01-13] Remove spurious assert when comparing function
- Kernel [2021-01-12] Set default machdep to x86_64 (was x86_32);
allow setting machdep via environment variable FRAMAC_MACHDEP.
- Kernel [2021-01-08] Allow -add-symbolic-path to survive saves/loads and
-* Eva [2020-12-05] Fixes a crash when subdividing the evaluation of
pointer expressions (via option -eva-subdivide-non-linear).
- Libc [2020-12-02] Remove obsolete attribute FRAMA_C_MODEL in the libc.
-* Logic [2020-11-30] The assigns clause can't mention const locations
o Kernel [2020-11-27] Extract builtin-related functions from module Cil
to module Cil_builtins. Code can be updated using
`bin/migration_scripts/titanium2vanadium.sh`.
- Eva [2020-11-26] Allow using Eva directives Frama_C_show_each and
Frama_C_dump_each in ghost code.
- Metrics [2020-10-27] Add json output in addition to text and html.
###############################################################################
Open Source Release 22.0 (Titanium)
###############################################################################
- MdR [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
- Dev [2020-10-20] Support for OCamlGraph 2.0.0
- ACSL [2020-10-16] Allows for axiomatic blocks-like extensions
- Variadic [2020-10-14] Don't print generated function name but print
original name and a comment with the generated name so that the
printed code is compilable.
- Aorai [2020-10-13] Ya automata can set auxiliary variables during a
transition, and use such variables in subsequent guards.
- Kernel [2020-10-09] Add option -print-config-json, to output Frama-C
configuration data in JSON format.
- Logic [2020-10-14] '\from' now accepts '&v' expressions
- Metrics [2020-10-01] Distinguish between undefined but specified functions
and functions with neither definition nor specification.
-* Eva [2020-09-28] Improved string builtins on wide strings: crash fixed,
better performance, misaligned pointers now considered invalid.
- Kernel [2020-09-22] New option -autocomplete p1, ..., pn that list the
options of plug-ins p1, ..., pn in a format suitable for
autocompletion scripts.
- Kernel [2020-09-21] Option -permissive now allows non-existent option
names.
- Logic [2020-09-11] Introduce check-only annotations for
requires, ensures, loop invariant and lemmas
- Kernel [2020-09-08] Add option -print-cpp-commands, to print the
preprocessing commands used by Frama-C.
- Eva [2020-09-07] Deprecates legacy options aliases -val-* in favor
of option names -eva-*.
-* Slicing [2020-09-07] Better handling of invalid command line options.
- Eva [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using
equality operators, temporary variables introduced by the Frama-C
normalization or goto statements.
-! Kernel [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
- Eva [2020-05-29] New builtins for trigonometric functions acos, asin
and atan (and their single-precision version acosf, asinf, atanf).
- Kernel [2020-05-28] Support for C11's _Thread_local storage specifier
- Kernel [2020-05-26] New option -explain, which provides help messages
for options used on the command line.
- Eva [2020-05-25] New annotation eva_allocate to configure the behavior
of an allocation builtin for a call, overriding the global option.
- Eva [2020-05-25] New option -eva-alloc-builtin to configure uniformly
the behavior of allocation builtins, instead of providing several
builtins with different behaviors for malloc/calloc/realloc.
- Eva [2020-05-20] Supports the ACSL mathematical operator \abs
- Kernel [2020-05-18] Support for C11's _Noreturn function specifier
###############################################################################
###############################################################################
###############################################################################
Open Source Release 21.0 (Scandium)
###############################################################################
-* Doc [2020-05-07] Fixes internal refs in generated pdfs (fixes #2505)
-* Kernel [2020-05-04] Accept UCN-encoded unicode char in ACSL (fixes #@849)
o Kernel [2020-04-27] Plug-ins specific dirs now use Filepath instead of
- Eva [2020-04-10] Fixes the Memexec cache on functions with logical
annotations about variables unused in the C body of the function.
- Eva [2020-04-06] New option -eva-domains-function to enable domains
only on given functions. Argument <d:f> enables the domain [d]
on function [f], while <d:f+> also enables it on all functions
called from [f]. <d:f-> disables [d] from function [f].
- Eva [2020-04-03] New experimental builtins for dynamic allocation
Frama_C_*alloc_imprecise: faster convergence, but very imprecise.
- Kernel [2020-04-01] Report user errors when keys are not bound to a
value for command-line options that require pairs of key:value
as arguments. Such keys were silently ignored.
*! Kernel [2020-03-30] Reject labels at end of blocks.
- RTE [2020-03-30] Emits alarm on invalid pointers when option is on
- Eva [2020-03-30] Emits alarm on invalid pointers when option is on
- Kernel [2020-03-30] New option -warn-invalid-pointer (disabled by
default) to warn on invalid pointer arithmetics resulting in a
pointer that does not point to an object or one past an object.
- RTE [2020-03-27] Emits alarm on pointer downcast when option is on
- Eva [2020-03-27] Emits alarm on pointer downcast when option is on
- Kernel [2020-03-27] New option -warn-pointer-downcast (activated by
default), to warn when a conversion between pointer and integer
might provoke a loss of precision.
- Kernel [2020-03-20] Add option -cpp-extra-args-per-file
-* Kernel [2020-03-18] Fixes #@823 (-load-module/-load-script now accept
-* Kernel [2020-03-18] Fixes #@818 (term generated for downcast alarms)
- Eva [2020-03-17] Supports the ACSL extended quantifiers \min and \max.
- Eva [2020-03-17] deprecate options -eva-*-domain in favor of
- ACSL [2020-03-04] Make conversion from C ptr to logic array explicit
- Eva [2020-03-03] Evaluates the logic predicate memchr_off, used in
- Eva [2020-03-03] Slightly better heuristics for the subdivision of
- Instantiate [2020-03-02] New plug-in Instantiate, to create function
specializations for specific plug-ins and functions (e.g. malloc,
memcpy, memset), to overcome limitations due to their
specifications.
- Kernel [2020-02-25] support for ghost else blocks
- Kernel [2020-02-18] checks that ghost code does not modify the normal
-* Kernel [2020-02-17] fixes issue that could prevent loading plug-ins on
- Kernel [2020-02-14] -constfold now takes into account value
o ACSL [2020-02-13] Add possibility for ACSL extensions to alter the
sequence of untyped terms they receive from the parser. Make also
possible to customize the short pretty printer of extensions.
o Kernel [2020-02-13] Deprecated:
- Logic_typing.register_*_extension
- Cil_printer.register_*_extension
- Cil.register_behavior_extension
Use Acsl_extension.register_* instead
- Eva [2020-02-12] New option "-eva-domains <d1>,<d2>,..." to enable
several domains at once. The list of available domains is given
in the help message of the option.
o! Eva [2020-02-12] Simplifies abstract domain signature by removing the
-* Eva [2020-02-12] Fixes the evaluation of logic predicates involving
- Eva [2020-02-07] Supports the logic evaluation of quantifiers
introducing mathematical variables (integer or real).
o! Kernel [2020-02-04] Removed FCBuffer, FCMap and FCSet. Use directly
OCaml stdlib modules Buffer, Map and Set instead.
- Eva [2020-02-04] Renamed option -eva-malloc-functions into
-eva-alloc-functions. Also contains calloc and realloc by default.
-* GUI [2020-01-24] Fix order of globals in the source panel.
- Eva [2020-01-23] Adds consistency checks on return and parameters
types between a builtin and the replaced C function.
- Eva [2020-01-23] Subdivisions can now be enabled locally:
- through the new option -eva-subdivide-non-linear-function that
overrides the global option for the given functions;
- via /*@ subdivide N; */ annotations on specific statements.
###############################################################################
###############################################################################
- Eva [2019-11-25] In the summary, fixes the number of alarms by
category when the RTE plugin is used, and do not count logical
properties in dead code as proven.
-! Kernel [2019-10-31] More stringent verifications on the use of ghost
- MdR [2019-10-31] New plug-in Markdown-Report (MdR) for markdown and
- Eva [2019-10-23] In the summary, fixes the total number of functions
- Eva [2019-10-23] New option -eva-auto-loop-unroll N to unroll all
loops whose number of iterations can be easily bounded by <N>.
- Eva [2019-10-21] New octagon domain inferring relations of the form
l ≤ ±X±Y ≤ e between pairs of integer variables X and Y. Enabled
with option -eva-octagon-domain. Only infers relations between
pairs of scalar variables occuring in a same instruction.
Intra-procedural by default; octagons can be propagated through
function calls with option -eva-octagon-through-calls.
- ACSL [2019-10-04] Support for ghost parameters
- Eva [2019-10-04] Evaluates ACSL predicates \is_plus_infinity and
\is_minus_infinity.
- Kernel [2019-10-04] Supports macro INFINITY and NAN.
o Config [2019-09-27] ocp-indent 1.7.0 is now used for indentation
o Eva [2019-09-16] Dynamic registration of abstract values and domains:
developers of new domains no longer need to modify Eva's engine.
-* Kernel [2019-09-13] Fixes Hptmap on keys with id greater than 2^28.
-* Makefile [2019-09-12] Fixes #2378 - bytecode only compilation (patch
contributed by madroach) and use -thread where needed.
-* Eva [2019-08-21] Fixes the reduction by the negation of \initialized
and \dangling predicates on imprecise lvalues.
-* Kernel [2019-08-20] Fixes a rare but critical bug which occured when
Frama-C internally switched the current project in presence of >2
projects and destroyed the old current project at about the same
time: the Frama-C internal state became inconsistent and lead to
unsound computations and crashes. It may be revealed to the
end-user when using a long sequence of -then-replace (at least 3
of them).
-* Kernel [2019-08-20] Fixed sequence of -removed-projects and -then
o Ptests [2019-08-05] Add new MODULE directive for compiling and loading
an auxiliary OCaml module for a test
- Kernel [2019-08-05] Add -keep-unused-types normalization option
- Libc [2019-08-05] Remove obsolete (and forcing cpp error) builtins.h
o! Kernel [2019-08-02] Functions over visitor's behaviors have been moved
from Cil into a new module Visitor_behavior. Apply the migration
script potassium2calcium.sh to update your plug-ins automatically.
o! Sparecode [2019-07-26] Removed from Db. Use proper Sparecode API instead.
-! Kernel [2019-07-24] OCaml version greater than or equal to 4.05.0 required.
- Kernel [2019-07-24] Improve placeholders handling in -cpp-command
o! Kernel [2019-07-23] Types in Properties are now records and not tuples
- Eva [2019-07-09] Supports ACSL floating-point comparison operators
eq_float, le_float, eq_double, le_double, etc.
o! Kernel [2019-06-28] removes AST constructors TCoerce, TCoerceE,
-* Kernel [2019-06-20] fixes dangling ref when removing unused static local
###############################################################################
###############################################################################
-* RTE [2019-05-24] fixes a crash when visiting variable declarations
- Eva [2019-04-19] The new annotation /*@ split exp; */ enumerates the
possible values of an expression and continues the analysis
for each of these value separately, until a /*@ merge exp; */
is encountered. It is also possible to maintain this partitioning
at all times with the option -eva-partition-value exp.
- Eva [2019-04-19] New option -eva-partition-history N to delay the join
of abstract states for up to N merging points, thus keeping these
states separate longer. Useful when a reasoning depends on the
path taken to reach a control point, but can increase the analysis
time exponentially in N.
- Eva [2019-04-19] Loop unroll annotations now accept non-constant but
bounded expressions as the maximum number of unrollings to perform.
-* Kernel [2019-04-09] Avoid crashing on one-letter attributes. Fixes #2432
-* Obfuscator [2019-04-09] Also obfuscate formals in function pointer types.
- Eva [2019-04-05] Prints an analysis summary at the end, outlining the
analysis coverage and the number of errors, warnings and emitted
alarms. It can be disabled with the option -eva-msg-key=-summary
- Eva [2019-04-03] New option -eva-precision to globally configure the
analysis from 0 (fast but imprecise) to 11 (accurate but slow).
A precision of 5 is often a reasonable trade-off. This meta-option
automatically sets up other options that can also be overriden.
- Inout [2019-04-01] Fix performance issue when initializing large arrays.
- ACSL [2019-03-08] Add check annotation, similar to assert except that
it does not introduce additional hypotheses on the program state
-* Makefile [2019-03-07] Do not attempt to install .cmx on bytecode-only
architectures. Patch by M. Dogguy backported from Debian package
- Libc [2019-03-05] Better specs and removal of half-implemented ifdef
that tried to take various POSIX versions into account
-* Kernel [2019-03-05] Better detection of invalid goto in presence of VLA
- GUI [2019-03-04] Compatibility with lablgtk3 and improved handling of
- ACSL [2019-03-01] Clarifies which C variables are in scope under a
- Libc [2019-02-26] Ask clang not to warn about unknown FRAMA_C_MODEL
attribute when pre-processing frama-c's libc
-* Obfuscator [2019-02-26] Obfuscate logic types and logic constructors.
-* Inout [2019-02-21] Fixes operational input on const local initialization
o RTE [2019-02-21] RTE has a static API
o Kernel [2019-02-18] When registering extended ACSL annotations, one
must now indicate whether they should have a status.
o Kernel [2019-02-05] Integer API moving closer to Zarith
- Eva [2019-01-19] New warning category for detecting loops without
- Eva [2019-01-31] Ignore annotations with "no_eva" tag
-* ACSL [2019-01-19] Accept C identifiers that happen to be ACSL keywords
- Eva [2019-01-10] Improved precision on nested loops (by postponing
the widening on inner loops according to -eva-widening-period).
-* Aorai [2019-01-04] Fixes #@586: avoid removing the initial state
- Kernel [2019-01-03] Add attributes for loop statements to allow
-! Kernel [2019-01-03] Add statement attributes (sattr) to the AST. They
are not printed by default, use -kernel-msg-key printer:attrs
-! Kernel [2019-01-03] Improved precision of integer abstract bitwise
-* Eva [2018-12-17] Fixes -eva-split-return on uninitialized or escaping
function returns when -eva-warn-copy-indeterminate is disabled.
o Kernel [2018-12-11] New functions for retrieving major and minor version
-* Kernel [2018-12-04] Fixes AST integrity check wrt volatile accesses
-* Kernel [2018-11-21] Fixes #@553 - pretty-printing of basic asm template
###############################################################################
Open Source Release 18.0 (Argon)
###############################################################################
-! Kernel [2018-10-24] Log.error and Log.failure will eventually make
Frama-C exit with a non-zero status. Fixes #@552
- Kernel [2018-10-24] More ergonomic command-line options for governing
warning categories statuses.
- Eva [2018-10-24] Enable the memexec cache by default. It can be
disabled by option -eva-no-memexec.
- Eva [2018-10-22] Improved performances when the symbolic locations
domain and the memexec cache are enabled.
- Eva [2018-10-22] The memexec cache is now fully compatible with all
abstract domains provided by Eva. However, the binding to the
Apron domains disable memexec.
- Eva [2018-10-18] New experimental domain "numerors" inferring absolute
and relative errors of floating-point computations. Enabled by the
option -eva-numerors-domain. Does not handle loops for now.
-* Kernel [2018-10-18] Fixes parsing of compound initializers with anonymous
fields. Fixes #2384
-* Kernel [2018-10-16] Consider that asm can change content of pointers
used as inputs when generating assigns clauses. Fixes #@458
- Eva [2018-10-12] Remove option -obviously-terminates.
- Kernel [2018-10-05] New option -warn-invalid-bool, to warn when reading
trap representations of type _Bool.
- Eva [2018-10-04] ACSL predicates with a "no_eva" tag are now ignored.
- Eva [2018-10-03] Warn about currently unsupported specifications
of some libc functions.
- Eva [2018-10-02] Fix the gauges domain on weak bases.
- Eva [2018-10-02] Some fixes and improvements of the equality domain.
-* Kernel [2018-10-02] Rejects sizeof of an incomplete type. Fixes #@560.
-* Kernel [2018-09-26] Add attribute to allow writing into const lvals in
specific (aka C++ constructors and mutable fields) circumstances.
Fixes #2395.
- Kernel [2018-09-14] New warning (disabled by default) when multiple side
effects are unsequenced (CERT-EXP10-C recommandation).
Fixes #@492
- Eva [2018-09-13] Remove option -val-warn-left-shift-negative, and
comply with kernel option -warn-[left|right]-shift-negative.
- Kernel [2018-09-13] New options -warn-left-shift-negative (enabled by
default) and -warn-right-shift-negative (disabled by default),
to control the emission of alarms on shifts on negative integers.
o! Constant Propagation [2018-09-12] Removing Db API for Constant Propagation
plug-in. Calls to !Db.Constant_Propagation should be replaced by
calls to Constant_Propagation.Api.
- Eva [2018-09-12] Reduction of values leading to division by zero
alarms, when possible.
- Eva [2018-09-11] Better reduction of floating-point values cast into
integer types when an alarm is emitted.
- Metrics [2018-09-06] Add option -metrics-used-files, to help identify
unnecessary files given in the command line
- RTE [2018-09-05] Remove option -rte-precond.
- Eva [2018-08-31] Supports the ACSL functions \min and \max.
- Eva [2018-08-30] Fixes the alarms on subtractions and comparisons of
pointers on weak bases (created by allocations in loops).
-! ACSL [2018-08-28] Introduce extensions to global annotations and
better characterization of each extension kind.
See development guide for more information
- Eva [2018-08-28] All options of Eva start with -eva. Aliases to
previous option names preserve backward compatibility.
-! Eva [2018-08-28] Rename plug-in shortname from 'value' to 'eva'. Eva
is now properly named Eva in all logs, in the GUI, and as the
emitter of the alarms.
-! Kernel [2018-08-23] Introduce Filepath dataype for more consistent
normalization of filenames
-* Kernel [2018-08-23] Do not allow compound assignments to const variables
Fixes #@384
-! Kernel [2018-08-23] Remove option -const-writable: const globals are
unconditionally constants
-* Eva [2018-08-02] Deprecate option -val-warn-builtin-override in favor
of warning category builtins:override.
- Kernel [2018-07-26] Fix compilation on OpenBSD
patch contributed by madroach. Fixes #2379
- Kernel [2018-07-26] New option -remove-inlined to remove function(s)
after -inline-calls, add category @inline to refer to all
functions with inline attribute (for both options).
- Eva [2018-07-23] The debug category "garbled-mix" becomes a warning
category. Better track of garbled mix created by specification.
-* ACSL [2018-07-23] Avoid removing cast of void ptr used as
argument of function expecting a ptr with known size. Fixes #@432
o! Kernel [2018-07-23] Remove completely outdated module Dataflow.
Deprecated since 3+ years. Use Dataflow2 instead.
-* RTE [2018-07-23] Stop generating spurious \initialized alarms.
-* Kernel [2018-07-06] Respect relative order of labels and ACSL annots.
Fixes #@524
o* Ptests [2018-07-02] Do not keep oracles for empty stderr. Fixes #@402
-*! ACSL [2018-07-02] introduce ACSL operators \le_double, \ge_double, ...
in addition to \le_float, \ge_float, ... Remove overloading of
\le_float that made it accept double as arguments. Fixes #@502
- Eva [2018-06-28] New option -eva-report-red-statuses listing in
a csv file the properties invalid for some states of the analysis
(as in the "Red Alarms" panel of the GUI).
- Eva [2018-06-25] Release all builtins, including memset and memcpy,
as open-source.
- Eva [2018-06-15] When a cvalue builtin is used, other domains use the
frama-c libc specification to interpret the call without losing
too much information.
- Eva [2018-06-14] The variables from the frama-c libc are no longer
shown in the initial state print.
- Eva [2018-06-11] Improved precision of string builtins for strlen,
strchr and memchr.
- Eva [2018-04-25] Renamed option -wlevel into -eva-widening-delay. New
option -eva-widening-period to control the number of iterations
between two widenings.
- Eva [2018-04-25] New propagation strategy that allows unrolling loops
even when the slevel has been exceeded. Unroll the N first loop
iterations via the global option -eva-min-loop-unrolling N or via
specific code annotations /*@ loop unroll N; */. The new strategy
may affect analyses even without loop unrolling.
###############################################################################
Open Source Release 17.1 (Chlorine-20180502)
###############################################################################
- Libc [2018-07-05] Fix C++ compatibility for Frama-Clang plug-in
###############################################################################
Open Source Release 17.0 (Chlorine-20180501)
###############################################################################
- Eva [2018-04-25] Added scripts and templates to help automate case
studies (in $FRAMAC_SHARE/analysis-scripts)
-* Typing [2018-04-23] Stronger checks w.r.t. implicit conversions in
function pointers (must have compatible types) and assignments
(modifiable lvalues). Fixes #@479
- Kernel [2018-04-23] Added option -inline-calls for syntactic inlining
-* Kernel [2018-04-19] Avoid crash when re-declaring a function with
formals after it has been called without any. Fixes #@454
- Kernel [2018-04-13] Deprecate option -warn-decimal-float in favor of
warning category parser:decimal-float
- Kernel [2018-04-13] More possible statuses for warning categories.
Fixes #@486
o Kernel [2018-04-13] Change Cil.typeHasAttributeDeep into
Cil.typeHasAttributeMemoryBlock. Fixes #@489
o* Logic [2018-04-11] properly reset logic environment in case of typing
errors. Fixes #@326
- Eva [2018-04-10] Interpret the logic constants \pi and \e.
- Eva [2018-04-06] Initialization of volatile pointers now keeps the
base addresses of the pointer (with arbitrary offsets).
- Eva [2018-04-06] Fix the initialization of local volatile variables,
which can always have any value.
- Eva [2018-04-06] In the logic, interpret the ACSL function \sign and
the constructors \Positive and \Negative.
- Metrics [2018-04-05] When the value coverage is computed, also shows the
total number of statements by function in the filetree of the Gui.
- Gui [2018-04-04] Added Preferences menu (shortcut: Ctrl+P) to set
themes for property bullets and external source editor
o Lib [2018-03-30] New Rich_text module to create message with tags
o! Kernel [2018-03-30] Never or rarely used Log functions have been
removed or deprecated
- Eva [2018-03-15] Avoid enumeration on values with too many bases —
fixes a performance issue.
- Gui [2018-03-07] The preconditions of a function call can now be
displayed before the call statement itself (click on status
bullets with '+' or '-' to unfold/fold them)
- Typing [2018-03-02] Support for CERT EXP46-C
- Eva [2018-03-01] Fix a soundness bug in the equality domain: do not
infer incorrect equalities between incomparable pointers,
or between -0. and +0.
- Eva [2018-02-26] deprecate option -val-warn-on-alarms in favor of
warning category alarm
- Kernel [2018-02-26] deprecate option -continue-annot-error in favor of
warning category annot-error
-! Kernel [2018-02-26] introduce warning categories, with various
possible behaviors. Refactor management of debug categories
-* RTE [2018-02-23] Do not emit spurious 'idx < 0' assert
on gcc-style FAM. Fixes #@393
-* Kernel [2018-02-23] Handle anonymous struct/union init. Fixes #@376
- Eva [2018-02-22] Equalities can be propagated through function calls.
New options -eva-equality-through-calls[-function] to decide
(globally or by function) which ones are kept from the caller.
- Eva [2018-02-21] When an lvalue lv is assigned or leaves the scope,
the equality domain tries to replace lv by an equal term (if any)
in the expressions depending on lv (instead of removing them).
o! Occurrence [2018-02-20] Removing Db API for Occurrence plug-in. Calls to
!Db.Occurrence should be replaced by calls to Occurrence.Register.
o! Impact [2018-02-20] Removing Db API for Impact plug-in. Calls to
!Db.Impact should be replaced by calls to Impact.Register.
o! Users [2018-02-20] Removing Db API for Users plug-in. Calls to
!Db.Users should be replaced by calls to Users.Users_register.
- Eva [2018-02-13] Removed *_alloced_return base created for functions
without body that return pointers. Such bases were imprecise
and could be unsound in corner cases.
- Eva [2018-02-08] Shifts of addresses now create garbled mixes (as any
other arithmetic operation).
- Logic [2018-02-07] Ghost code now supports /@ ... @/ annotations
- Eva [2018-02-06] By default, do not emit pointer_comparable alarms for
non pointer operations. Always compute {0;1} for non pointer
comparisons involving incomparable addresses.
- Eva [2018-02-01] Warn about unsupported allocates clauses.
- Eva [2018-01-30] The subdivision of evaluations (through the option
-val-subdivide-non-linear) can subdivide the values of several
lvalues simultaneously (on expressions such as x*x - 2*x*y + y*y).
- Kernel [2018-01-24] Better renaming of variables in case of name
collision.
o! Kernel [2018-01-24] Keep information about syntactic scope of local
static variables. Accessed through
Globals.Syntactic_search.find_in_scope.
-! Eva [2018-01-24] Renamed option -val-malloc-returns-null to
-val-alloc-returns-null, which also applies to realloc builtins.
- Kernel [2018-01-16] Added option -json-compilation-database to help with
preprocessing. Requires yojson during Frama-C compilation.
- Eva [2018-01-15] New function post_analysis in abstract domains,
called at the end of the analysis.
- Eva [2018-01-11] The Simple_memory functor lets builtins interpret C
functions from the value of arguments to the result value.
- Eva [2018-01-11] Evaluate the preconditions of the functions for which
a builtin is used; builtins do not emit alarms anymore.
-! Kernel [2018-01-11] Alarms Logic_memory_access and Valid_string, that
were only emitted by Eva builtins, are removed.
-* ACSL [2017-12-14] Reinforce rejection of void* pointer types in the
arguments of ACSL built-in constructs related to memory blocks
and pointer dereferencing.
-* ACSL [2017-12-14] Reinforce rejection of implicit casts from array
types to pointer types in the arguments of ACSL built-in
constructs related to memory blocks and pointer dereferencing.
-* Kernel [2017-12-13] Clean up typechecking environment when dropping
side-effects (in sizeof et al.). Fixes #@430
o! Kernel [2017-12-13] Old Cil.isCharType renamed as Cil.isAnyCharType.
New Cil.isCharType is now only true for plain char, neither signed
nor unsigned. Derived functions (isCharPtr et al.) also updated
- Eva [2017-12-12] Fix a crash when using -val-stop-at-nth-alarm.
- Eva [2017-12-07] Eva complies with option -warn-special-float, and
propagates or warns on NaN and infinite values accordingly.
-! Kernel [2017-12-07] Option -warn-not-finite-float renamed into
-warn-special-float and extended (accepts non-finite/nan/none).
- Kernel [2017-12-07] Make some typechecking warnings controllable with
-kernel-msg-key keys.
- Eva [2017-12-07] New option -val-skip-stdlib-specs, set by default.
When analyzing the body of a function from Frama-C's standard
library, specifications will be skipped.
- Eva [2017-11-28] New builtins for the single-precision mathematical
functions fmodf, cosf, sinf and atan2f.
-! Eva [2017-11-16] In the log, messages on preconditions are now
reported with the location of the call site.
o! Eva [2017-11-09] The Fval module now supports NaN and infinite values.
Major API changes in Fval, Ival and Cvalue.V (regarding casts,
mostly)
-o Eva [2017-11-09] Option -all-rounding-modes has been removed
-* Eva [2017-11-09] Fix bugs in builtins for cos and sin. The results