Skip to content
Snippets Groups Projects
Commit c36712fd authored by Jan Rochel's avatar Jan Rochel
Browse files

[e-acsl] exempt standard objects from runtime memory checks

stdin/stdout/stderr/errno not need explicit initialization or
allocation. They are outside of any of the tracked memory segments.
Notably, due to the subsequent commit they are no longer erroneously
inside the TLS segment. Therefore we need to exempt them from the tests
\valid, \valid_read and \initialized. We also need special treatement
for these objects in \offset, \base_addr, \block_length, \freeable.

In this commit this exemption is implemented as a runtime test, as it
cannot be exhaustively implemented statically (see
tests/memory/errno.c). This runtime exemption is sufficient, however we
will in later commits add such static exemptions anyway for easy cases,
as an optimisation that reduces the number of generated assertions.

This commit simplifies and changes the semantics of the (unused)
e_acsl_safe_locations module.
parent 6a48c9b8
No related branches found
No related tags found
No related merge requests found
Showing
with 1096 additions and 198 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