only

testrun.sh improvements

A number of improvements to `testrun.sh` script aiming to improve output of non-regression tests during test failures. The improved script reports the details of the following:

- instrumentation and compile-time failures.
- output of failing programs (i.e., programs existing with a non-zero status).
- difference in the outputs of executables generated from instrumented and original sources 

See merge request !37

Doxygen and improvements to bit manipulation library

This merge request suggests the following change:
- Doxygen documentation for C code 
   - Updated makefiles and configure script. Doxygen documentation can be built using either `doxygen` target (which builds only doxygen) or `doc` target that builds all documentation including doxygen. Documentation is generated in `doc/doxygen/html`.
   - Several files were updated to include doxygen comments. To avoid confusion with ACSL annotations `/*! \tag */` syntax was used.
- Several small updates and improvements to bit manipulation header (`e_acsl_bits.h`).

See merge request !36

[tests] improve the testcase for \freeable to take into account BTS entry #1830



See merge request !33

Fix output of freeable test as per change in code generation

Improvements to the C runtime lirbary of E-ACSL

This merge requests brings the updates to the E-ACSL memory model made during development of the segment-based shadow model + some recent changes and improvements. I understand that the change is rather massive and touches many aspects so maybe it would be worthwhile to have a brief meeting where I can give you more detailed explanations before you review the change.

- Improvements to the localized implementation of `printf` (`e_acsl_printf.h`):
    * specifiers for printing memory addresses.
    * specifiers for printing bit-level representation of memory blocks.
    * `abort`/`assert` functionality moved to the `e_acsl_assert.h` header.
- `e_acsl_assert.h` (new):
    * custom implementation of `assert` and `abort` functions.
- `e_acsl_malloc.h` (new):
    * access to memory allocation functions.
- `e_acsl_debug.h` (new):
    * C utilities for debugging.
- `e_acsl_string.h` + `glibc` folder (new):
    * custom (GLIBC) implementations of `memset`, `memcpy`, `strlen`, `memmove`, `strcmp` and `strncmp`. See in-line documentation for further details.
-  `e_acsl_syscall.h` (new):
    * re-declarations of standard system call functions using direct application of `syscall`. See in-line documentation for further details.
- External E-ACSL API (`e_acsl_mmodel.h`) moved one level up.
- Directory `memory_model` renamed to `adt_models`. ADT stands for Abstract Data Type.
- Changes to the E-ACSL public API:
    * removed `__out_of_bound` function unused
    * added `__e_acsl_memory_init` -- functionality relevant for initialization of a memory tracking state.
    * `__memory_size` variable used for tracking of allocated memory on the program's heap renamed to `__heap_size`. In addition renamed the `__get_memory_size` renamed to `__get_heap_size`.
    * function `__init_args` renamed to `__init_argv`. The change is because `__init_argv` is responsible only for tracking of strings captured by `argv` argument to the main function.
    * function `__literal_string` renamed to `__readonly`.
    * `e_acsl_assert` renamed to `__e_acsl_assert`. 
- Changes to ADT-based memory model (`adt_models/e_acsl_mmodel.c`):
    * fixed a bug in `realloc` that caused lookup failure if `realloc` relocates a memory block to a new address.
    * system-wide assertions, print statements and `string.h` functions (e.g., `memset`) replaced by custom implementations.
    * removed `__e_acsl_mmodel_memset` function in favour to the functionality provided by`e_acsl_string.h`.
    * removed definition of `__out_of_bound` (see changes to the public API).

    * reorganization of code of ADT-based models. In the current implementation each model is encapsulated using a single file with all private symbols restricted to its compilation model. Files:
         - `share/e-acsl/adt_models/e_acsl_bittree_mmodel.c` (patricia trie)
         - `share/e-acsl/adt_models/e_acsl_tree_mmodel.c` (binary tree)
         - `share/e-acsl/adt_models/e_acsl_splaytree_mmodel.c` (splay tree)
         - `share/e-acsl/adt_models/e_acsl_list_mmodel.c` (linked list)
    * fixed an issue that caused ADT models to always use 64-bit addresses
    * fixed a bug that caused calloc-allocated blocks appear as uninitialized data
    * fixed a bug leading to incorrect initialization of partially allocated blocks via `realloc`
    * fixed a bug leading to incorrect initialization test for partially allocated blocks
    * implemented a dynamic guard against compiling sources instrumented using different pointer size.
- Changes to the instrumentation engine:
    * `__e_acsl_memory_init` renamed to `__e_acsl_globals_init`
    * calls to `__e_acsl_memory_init` (now provided by the public API) are added by instrumentation for all 
cases that require memory tracking.     
- Other changes:
    * changes to `e-acsl-gcc.sh`, `Makefile.in` and test oracles to accommodate the above.
    * added tests for \initialized and \offset predicates
      


See merge request !31

Merge branch 'feature/kostyantyn/c-updates' of git.frama-c.com:frama-c/e-acsl into feature/kostyantyn/c-updates

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

[tests] execnow specified in test_config is now run on each test case

Patch related to MR frama-c/frama-c!728.
@kvorobyov : fix the issue that you talked me about. The main patch is in Frama-C's ```ptests```.

See merge request !35

internally via __e_acsl_memory_init

initialization of tracked memory blocks

macros in e_acsl_bits.h

manipulations

__e_acsl__memory_clean functions to be consistent with __init_argv