them from scratch each time

blocks (via constant strings)

- If FRAMAC_SHARE is not already set, either frama-c -print-share-path
  gives a correct result, and there's no need to set FRAMAC_SHARE in the
  first place, or it does not, and putting this result in FRAMAC_SHARE
  won't do any good.
- there's no need (and it seems to confuse Frama-C) to -add-path when in
  internal mode.

[scripts] fix a small bug when running e-acsl-gcc.sh from an uninstalled version of Frama-C. It impacted the test suite in Frama-C internal mode

instead of an instrumented one if --instrumented-only option was used

installed instrumentation engine

only

  - Removed tree, list and splaytree memory models (as obsolete)
  - Directory 'adt_models' renamed to 'bittree_model' as now it contains
  a single bittree model

    - Restricted internal symbols of Patricia trie memory model to its
        compile unit
    - Restructuring/renaming the files belonging to ADT models
    to make the names consistent with the contents of the files
    - Patricia trie model as a single file

  - Stylistic updates
  - Refactoring of assertions (production/debugging)
  - Refactoring iheader placement

containing the segment-based memory model.

  - --e-acsl-share option allowing to specify the location of RTL
  - compile using a local version of RTL if uninstalled version of the
  script is used.

Kostyantyn Vorobyov authored 9 years ago and Julien Signoles committed 9 years ago

    - Restricted internal symbols of Patricia trie memory model to its
        compile unit
    - Restructuring/renaming the files belonging to ADT models
    to make the names consistent with the contents of the files
    - Patricia trie model as a single file

Kostyantyn Vorobyov authored 9 years ago and Julien Signoles committed 9 years ago

  - Stylistic updates
  - Refactoring of assertions (production/debugging)
  - Refactoring iheader placement

Kostyantyn Vorobyov authored 9 years ago and Julien Signoles committed 9 years ago

containing the segment-based memory model.