(bug introduced in !59)

Aligned memory allocation [RFM]

This merge request suggests the following changes to the C-level memory model:
- Tracking heap allocations via `posix_memalign` (POSIX compatibility)
- Tracking heap allocations via `aligned_alloc` (C11 compatibility)
- Advanced aliasing of public API functions
- Few minor bugs and performance improvements in the bittree memory model

NOTE: This merge request depends on merge request !59 (Custom malloc for RTL).

See merge request !61

Customized malloc tor E-ACSL RTL

This merge request suggests the following changes.

- Improved memory-allocation functions in E-ACSL RTL via a customised implementation of [jemalloc](http://www.canonware.com/jemalloc/). This addresses issue #9. 
- Switch from explicit tracking of heap allocations (by rewriting `malloc` to `__e_acsl_malloc`) to implicit tracking that overrides default `malloc` (and similar functions) with custom implementation. This approach also solves the issues where memory blocks allocated implicitly (e.g., via `strdup` were not recorded.)
- Localised version of GMP library. This is requred for malloc and allows E-ACSL be self-contained.

See merge request !59

Fix issues with the new type system

These issues were found by the Cfp plug-in. Consequently this MR and the upcoming one in CFP are required to fix OCI. This patch generates even less casts than before.

See merge request !62

Add CfP and Security to continuous integration



See merge request !60

fix function Translate.term_to_exp used by plug-in Cfp. This fix requires to call the type system with no context in some cases

New type system

This MR implements the new type system which is used to choose the best type for the generated integer expressions (in particular, either mpz or a standard C integral type).

The core of the implementation follows Figures 3 & 4 of the following paper : http://julien.signoles.free.fr/publis/2015_jfla.pdf. Sorry it is in French, but the Figures are in an international mathematical language  . The main modification is the integration of a context in order to replace the 2 coercion rules (in order to transform a formal system in which more than 1 rule may be applied into an algorithm).

It is probably not a good idea to read this MR commit by commit since interval.ml* are new files and typing.ml* were fully rewritten. It is probably much better to read these files from scratch and look at the differences between the last master commit and the last commit in this branch for the rest.



See merge request !50