- The default values in `e-acsl-gcc.sh` are removed to always use those
  in `e_acsl_shadow_layout.h`
- The default values in `e_acsl_shadow_layout.h` are set to the values
  that were in `e-acsl-gcc.sh` since they were the values actually used
  by default.

- The option is activated by default.
- The option is deactivated for the tests in DEV config.

When the executable is linked with PIE, it is not possible for E-ACSL
to produce an accurate backtrace. This commit deactivate PIE if
e-acsl-gcc.sh compiles in debug mode.

The `e-acsl-gcc.sh` only looked for the Frama-C executable in the
`$PATH`. This commit updates the search for Frama-C to be able
to detect the binary if installed in a folder not added to the path,
or if running the script from the development sources.

The Variadic plugin translation is incompatible with the use of option
 `-e-acsl-validate-format-strings`, so add the option
 `-variadic-no-translation` if the user activated the validation of
 format strings.

The `-p` option does not exist.

- Deprecate old `full-mmodel` option in E-ACSL plugin and in `e-acsl-gcc.sh`
- Create new `full-mtracking` option
- Update documentation to use the new option

Fonenantsoa Maurica authored 6 years ago and Julien Signoles committed 5 years ago

  - Interval:
    - Not_an_integer -> Is_a_real|Not_a_number.
    - infer -> infer_with_real
      because Not_a_number has priority over Is_a_real
    - Ival.bottom when Is_a_real
      because the interval is for integers
  - Typing:
    - integer_ty -> number_ty=Cty|Gmpz|Libr|Nan
    - Other -> 'Other (Oreal|Onan)'
  - Translate:
    Encode real constants into strings:
      - **NO** conversion to float-point type
      - strnum_ty=StrZ|StrR|Not_a_strnum
        for tracking the type of the string
Add Libr:
  - Gmpz -> Gmp=Gmpz+Gmpq
  - Libr=ref to Gmpq
Add Gmpq builtins:
  - Custom mini-gmp -> libgmp
    because mini-gmp has no support for Q
  - Add arithmetic over Q in e_acsl_gmp_api.h
Misc:
  - dec_to_frac: decimal expansion to fractional representation
    because decimal expansion is interpreted as double by Gmpq
Tests:
  - BTS 1307 has an assertion wrongly evaluated, fixed
  - Add tests/gmp/reals.c
THE MOST IMPORTANT TODO:
  - Completely hide the library for numbers (currently Gmp)
    inside Libr: Typing, Env and Translate should only know
    Libr and never directly call Gmp.
    This is crucial for extending E-ACSL in the future
    (eg: Gmp has no support for elementary functions), and
    also for using it as part of an abstract compiler
    (eg: with Fldlib)
    For the time being, in Translate,
    we have something as ugly as:
      let init_set =
        if Libr.is_t ty then Libr.init_set
        else Gmp.init_set

Patrick Baudin authored 6 years ago and Julien Signoles committed 6 years ago

  internal: use of hdrck for targets headers, check-headers and src-distrib
  external: reviewed target headers

compiled