to a Frama-C run

Changes to e-acsl-gcc.sh (Issue #7 )

This merge request introduces the following updates:
   - Structural improvements to the `e-acsl-gcc.sh` wrapper script.
   - Options allowing to specify names of the Frama-C and GCC executables in `e-acsl-gcc.sh`.
   - Improvements of the documentation and the proper man page for `e-acsl-gcc.sh`. 
   - Convenience wrapper around `e-acsl-gcc.sh` to be used with testing (`scripts/testrun.sh`).

Julien, please have a look at the `scripts/testrun.sh`, it may implement some of the features that you may find useful need for testing. If you like the script I am happy to extend it with other features that may be lacking for the moment. 

See merge request !25

- 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