Feature/wp/region analysis

See merge request frama-c/frama-c!2352

# Conflicts:
#	src/plugins/wp/Cint.ml
#	src/plugins/wp/MemTyped.ml
#	src/plugins/wp/why3_api.ml

Resolve "option -wp-msg-key builtins"

Closes #540

See merge request frama-c/frama-c!2393

[Eva] Dynamic registration of abstractions

See merge request frama-c/frama-c!2359

Domains are built by increasing order of priority, so domains with higher
priority are added at the top of the domains tree, and thus are processed
first during the analysis.

This ensures that the cvalue domain (and other optimized domains) are always
called first in the engine.

Do not lift the abstract locations if it is not needed.

Domain_product works on Internal modules.
Location_lift and Domain_lift promote leaf modules into internal modules,
by creating the suitable structure.

Complete rewrite of abstraction.ml, with even more first class modules and GADT.
All current abstract values and domains are registered with this generic
mecanism in abstractions.ml, except the Apron binding and the Numerors domain.

The configuration is now the set of abstractions that should be instantiated.

In abstract.ml, the structure of compound abstract values, locations and states
carries the first class module of their leaf components as data.

A type is now completely described by its structure.

Keys for abstract values, locations and states are created in structure.ml.
Shapes are created in the respective modules Value, Location and Domain
in abstract.ml.

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.

[Server] Basic testing

See merge request frama-c/frama-c!2384

Feature/bobot/eva trace

See merge request frama-c/frama-c!1481

[Eva] Fixes the computation of the mask in hptmap.

See merge request frama-c/frama-c!2382

[Eva] Memexec: fixes the computation of the set of bases related to the inputs.

See merge request frama-c/frama-c!2386

[kernel] avoid generating ill-formed asm contracts in presence of void ptrs

Closes #609

See merge request frama-c/frama-c!2387

Fix/andre/wp minor fixes

See merge request frama-c/frama-c!2308

When a `void *` lval is referenced in an asm directive, use its conversion
as `char *` in the contract to obtain well-formed `assigns` clauses.

Fixes #609

[configure] improved native thread detection

See merge request frama-c/frama-c!2361

Thanks to madroach for spotting the issue and providing a patch.

Thanks to madroach for spotting the issue and providing a patch.

[Cabs2cil] fix crash due to align attribute in FAM

See merge request frama-c/frama-c!2368