[e-acsl] statically determine some predicates for special pointers
For the special pointers stdin, stdout, stderr, and &errno the results of \pvalid, \pinitialized, \freeable are statically known, so we return the result directly instead of generating calls to the runtime functions. This complements the implementation of the same semantics in the runtime libraries in the previous commit. As the runtime implementation is sufficient, this commit is an optimisation. We currently do not optimise logic functions such as \block_length, \offset, \base_addr, but we do not expect too many occurrences of terms such as \base_addr(*(&stdin + 9)).
Showing
- src/plugins/e-acsl/src/analyses/memory_tracking.ml 45 additions, 0 deletionssrc/plugins/e-acsl/src/analyses/memory_tracking.ml
- src/plugins/e-acsl/src/analyses/memory_tracking.mli 8 additions, 0 deletionssrc/plugins/e-acsl/src/analyses/memory_tracking.mli
- src/plugins/e-acsl/src/code_generator/translate_predicates.ml 62 additions, 45 deletions...plugins/e-acsl/src/code_generator/translate_predicates.ml
- src/plugins/e-acsl/src/main.ml 1 addition, 0 deletionssrc/plugins/e-acsl/src/main.ml
- src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c 0 additions, 9 deletions...ns/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
- src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c 0 additions, 9 deletions...ugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
- src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c 24 additions, 114 deletions...csl/tests/concurrency/oracle/gen_threads_safe_locations.c
- src/plugins/e-acsl/tests/memory/oracle/gen_errno.c 0 additions, 19 deletionssrc/plugins/e-acsl/tests/memory/oracle/gen_errno.c
- src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c 3 additions, 61 deletionssrc/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
- src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle 0 additions, 24 deletionssrc/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
Loading
Please register or sign in to comment