Support for ranges in a few builtins

See merge request frama-c/e-acsl!224

  - No superfluous patterns
  - Using Cil.charPtrType
  - call_for_unsupported_constructs as closure given to mmodel_call_with_ranges
  - Style:
    - Indendation
    - No superfluous begin..end
    - Parentheses
    - Spaces

 - Remove double warning for arithmetic over pointers
 - Not yet: size of memory area in GMP
 - Typing of Trange
 - Squashing pattern matchings
 - Use of has_set_as_index
 - No is_offset_of_array
 - Using exception in is_range_free
 - Using `call f`
 - Logic.is_set_type instead of catching Failure
 - Logic.const.taddrof
 - &t, instead of &t[0], is sufficient for arrays
 - No useless rec
 - Typos, useless parentheses, no camel case, comments, indentation

- Interval inference and typing
- Multi-dimensional arrays with ranges as indexes:
  - If the only range is the last index -> single call to builtin
  - Else -> not yet "arithmetic over set of pointers" (requires Mmodel modification)
- Tests for struct
- Richer pattern matching instead of is_trange
- has_range -> Misc.is_range_free
- Using Cil_const.make_logic_var_kind, Logic_const.taddrof, Logic_const.type_of_element and Logic_utils.mk_cast
- [elt] @ list -> elt :: list
- Options.fatal -> Options.abort
- Comments:
  - On the Range Elimination operation
  - Describing the formula for the range-free term
  - Describing mmodel_call_with_ranges and mmodel_call_default

synchronize with frama-c/frama-c!1717

See merge request frama-c/e-acsl!239

synchronize with frama-c/frama-c!1870

See merge request frama-c/e-acsl!237

Improve test stability

See merge request frama-c/e-acsl!236

use sorted iterator to stabilize tests (in frama-c!1736)

See merge request frama-c/e-acsl!235

synchronize with frama-c/frama-c!1860

See merge request frama-c/e-acsl!234

Synchronize with frama-c!1935 : Value becomes Eva

See merge request frama-c/e-acsl!233

synchronize with frama-c/frama-c!1947

See merge request frama-c/e-acsl!232

synchronize with frama-c/frama-c!1936

See merge request frama-c/e-acsl!231

update oracles

See merge request frama-c/e-acsl!229

Use Dataflow2 instead of completely outdated Dataflow

See merge request frama-c/e-acsl!227

[tests] remove some warnings about missing spec

See merge request frama-c/e-acsl!222

Fixes handling of labels in the instrumentation

See merge request frama-c/e-acsl!228

labels.ml was broken since quite some time.

Label.move must compare goto targets to the statement in the original
AST, not its copy. Furthermore moving labels must only be done if we
are about to change the target of the gotos, not if we use the
statement as generated by the plain visitor.