- improvements for the \offset test
    - new test case for testing behaviours of \base_addr predicate

that explore behaviours of initialized using un-allocated memory blocks

predicates

  - Incorrect initialization via realloc
  - Incorrect initialization test for partially initialized blocks
  - Unsupported specifiers in debug-level print

appear as uninitialized data

smaller than 512KB in 32-bit systems and 32MB in 64-bit systems.

externally for the case when a program is compiled with debug features

debug macro

multiple inclusions

    Reworked binary tree (tree) and linked list (list) memory models
    to have the same structure as the rest of the ADT models

Patricia trie (bittree)  memory model.
See commit e3d588eed2e9909f481371a6bbd4950dcb725291

    - 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-gcc.sh]

Fix for issue #8:

- --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.

See merge request !34

  - --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

    - improvements for the \offset test
    - new test case for testing behaviours of \base_addr predicate

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

that explore behaviours of initialized using un-allocated memory blocks

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

predicates

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

  - Incorrect initialization via realloc
  - Incorrect initialization test for partially initialized blocks
  - Unsupported specifiers in debug-level print