Type system improvements

- fix your reported bug BTS 2252 about typing of offsets
- optimize typing of operators by not propagating the context to the operand: it is useful only for the result and it sometimes introduces useless casts in the generated code.

See merge request !87

[typing] improve typing of operators by preventing propagation of the context to the operands. This way, it prevents to introduce useless type coercions. Indeed, the typing context is only useful to limit the number of generated casts when typing the _result_ of the operation.

Fixed a failure during assertion generation in expressions with shifts



See merge request !85

Use Ival.t for more precise intervals

Replace integer intervals with those in Ival.t.

See merge request !82

New option -e-acsl-builtins

Depends on frama-c/frama-c!873.

See merge request !53

Fix e-acsl version in local_config.ml



See merge request !84

Fix some uses of PLUGIN_DIR



See merge request !81

Update w.r.t. corresponding kernel branch

See Frama-C/Frama-C!973

See merge request !77

BTS test cases

- added test case for resolved bts1292 
- added missing COMMENT header to bts1291 

See merge request !79

Fix 2 bugs with integer casts

This MR fixes two bugs with integer casts:
- when generating a new variable corresponding to a cast ```(ty)t```, its type was the one of the translation of ```t```, not ```ty```
- for a cast ```(ty)t``` the implementation of the type system didn't compute the smallest interval from both operands. It might result in incorrectness of the generated code as reported in https://bts.frama-c.com/view.php?id=2231 (which is now fixed). I guess this patch also solves your gmp issue with SpecCPU Benchmark.

See merge request !78

Reorder generated AST to avoid its corruption and compile-time failures

This merge request suggests the following changes:
- Reordering globals in the generated AST so all added function calls were preceded by function definitions
- Handled renaming of GMP types to move them to "__e_acsl_" namespace for consistency with our public API and also to avoid clashes in naming.

See merge request !76

Conflicts:
	misc.ml
	quantif.ml