- Fixed inconsistency in the documentation of testrun.sh

makefile

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

and gcc executables

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

consistency in settings of various flags

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

    - Added man page
    - Fixed memory model option

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

involves getting rid of redundant flags

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

    - structural changes to e-acsl wrapper script
    - --memory-model option in the e-acsl wrapper script that allows
        switching between different memory models
    - added script to facilitate runs of e-acsl during
    testing (scripts/testrun.sh)

Bugfix for memory size computations/Embedded printf

- Fixed a bug in computation of the heap size via updates of the `__memory_size` variable.
- Added a test case for the above (e-acsl-runtime/memsize.c).
- Added embedded printf to the C memory model. This removes functionality from stdio.h and assert.h headers.
- Small updates and stylistic issues in the C code of the memory model.

See merge request !21

Replaced system-wide assertions with custom assertions using embedded
printf library

consistent with the rest of the C files

since the latter is faster

they are more generic and not exposed to the global scope

so they are restricted to e_acsl_mmodel.c compile unit

(__memory_size)  is computed correctly

tracked heap memory to be computed incorrectly for the following cases:
    - realloc is supplied 0
    - realloc fails