issue #11]

issue #11]

without memory-related predicates but with heap allocation

without memory-related predicates but with heap allocation

    - 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

containing the segment-based memory model.

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

    - 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

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

containing the segment-based memory model.

propagate change according to kernel changes about vlogic/vgenerated; but Misc.is_generated_varinfo is much less efficient than before

[E-ACSL] my previous tentative patch did not work. I prefer to have E-ACSL that works than non-regression tests...

[E-ACSL] fixed bug in debug mode
[E-ACSL] add missing headers