Skip to content
Snippets Groups Projects
Commit a755216c authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'feature/kostyantyn/c-updates' into 'master'

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
parents 4e644339 a9b1dda7
No related branches found
No related tags found
No related merge requests found
Showing
with 682 additions and 352 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment