'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
and special floating-point values (infinite and NaN).

These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
option, which is @all by default. These alarms can be disabled for some function
by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
the argument expressions of calls to [f].

However:
- the @all default value did not include functions without definition
  (for which a specification or a builtin is used).
- 'indeterminate' alarms were emitted anyway for the arguments of calls to
  functions without definition, except for builtins.
So no indeterminate alarms were emitted for the argument expressions of calls
to builtins (unless their definitions were included).

This commit fixes this behavior:
the @all default of -eva-warn-copy-indeterminate option include all functions
and special case for functions without definition or builtins are removed.

It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.

Renames the function [allowed_machdep].

Removes an heuristic that prevented the inference of octagons when the ival
for [x±y] contains all possible values for the type of [x] or [y].
This heuristic was too strong:
- it prevented some inference of relations about unsigned variables, as it also
  checked incorrectly the negation of the given ival;
- it could prevent the inference of relevant relations between signed variables,
  such as 200 < (int)cx + (int)cy < 200 where [cx] and [cy] have char types.

Instead, we now only checks that a new inferred octagon is not redundant with
the interval values, i.e. that the value for [x±y] cannot be computed solely
from the intervals of [x] and [y].

On casts, uses option -warn-[un]signed-downcast (instead of
-warn-[un]signed-overflow) to known if an integer wrap is possible.

Changes the criterion according to which the symbolic domain retains the value
of an expression:
- if the expression is an lvalue with an imprecise location;
- if the expression is a binary operation between two expressions, each
  containing an lvalue with an imprecise (non-singleton) value.

Otherwise, the value should always be inferred by the cvalue domain, or can
be precisely computed from values inferred by the cvalue domain.

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

A memory location becomes data-tainted through an assignment if the location
assigned depends on data-tainted values.

A memory location only becomes data-tainted when it is assigned to a
data-tainted value.
A memory location becomes control-tainted on an assignement:
- whose execution depends on a tainted condition;
- to a control-tainted value.
- such that the assigned location depends on tainted values.

Improves significantly the domain performance.

Instead of "loop-unroll".

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

Even if we can't evaluate them without the taint domain.

Parses the extension terms in the post-state.

Uses the logic environment to properly evaluates \result and values from the
pre-state when using Eval_terms.

This function now takes a logical environment, as [evaluate_predicate] and
[reduce_by_predicate].

"taint" is an extension for statement annotation, while "taints" is an extension
for contract behaviors.
Registers these extensions in taint_domain.ml instead of eva_annotations, as we
don't need the functions to add/get annotations to/from a statement.