Warns at the start of an analysis when the inout plugin is missing.

The new file eva_dynamic contains all accesses via the dynamic API.

Only the functions whose body is analyzed are counted as covered by the
analysis. The functions reached by the analysis but for which a builtin or the
specification is used are not considered analyzed anymore.

Summary: computes statistics only for analyzed function. Returns [None] for
other functions.

Valentin Perrelle authored 3 years ago and David Bühler committed 3 years ago

- Whole program statistics are aggregated from function by function
  statistics
- Also ordered the alarms output by count by category, except for
  the Other category

Cleans up and saves partial results on sigint signal.
Signal handlers are now registered at the start of an analysis, and previous
signal handlers are restored at the end.
New function [protect f ~cleanup] in value_util, that runs [f] and applies
[cleanup] in case of a user interruption or a Frama-C error, only if option
-save is set.

Catches Log.AbortError and Log.AbortFatal to properly clean-up the analysis
states on a failure.

Other plugins may want to use the analysis results anyway, and some functions
fail when the tables have not been marked as computed.

Instead, calls Domain.Store.mark_as_computed at the end of the analysis.

In domains, changes [Store.register_global_state] that now takes a boolean
argument indicating whether the domain states must be saved during the
analysis.

- Removes the [recursion] boolean field from [call] type.
- Functions in [compute_function] takes a [recursion option] in argument.

- [cacheable] is given at the registration of a builtin, and not separately
  for each result of the builtin.
- Removes the offsetmap for the arguments: no builtin were using it anyway.
- Returns a Cvalue.V.t for the result instead of an offsetmap.
- Builtins can also return:
  + only the value of the result, in which case the post-state from the
    interpretation of the specification is used with the resulting value
    computed by the builtin.
  + only the post-states for functions with no froms dependency (other than the
    result and arguments) and no write of local variable addresses.

Simplifies some builtins accordingly.

Type [cacheable] is now defined in Eval.
Type [call_result] is defined in Builtins.
Changes the type of callbacks Db.Call_Type_Value_Callbacks.

This function links the kernel functions to their builtins for a given analysis.
Checks that the builtin replacing a function has a compatible type and a
specification. These requirements are not checked each time a builtin is used.

The type of a builtin is now a function "unit -> typ" applied when the analysis
starts, allowing builtins to use types defined from the machdep, such as size_t.

These module definitions were previously in abstract_value, abstract_location
and abstract_domain. They are now grouped in this new file for the three
abstractions.
These module types should only be useful for the engine, and need not to be
visible in the implementation of the various abstractions.

New module type Leaf in abstract_value, abstract_location and abstract_domain
with the key identifying the module. The internal structure is no longer needed
in these abstractions, and is instead built by the engine from this key.

Keys are no longer exported outside the modules.
For abstract domains, the key is automatically created by the functor
Domain_builder.Complete from the domain name.

Many changes throughout the analyzer:
- in the engine, Abstract_value.{Internal|External} becomes
  Abstract.Value.{Internal|External}.
- in the abstractions, Abstract_value.Internal becomes Abstract_value.Leaf.

This module type simplifies the signature of functors using evaluation
functions.

(blind make headers from specifications)