Merge branch 'bugfix/basile/eacsl-148-ranges' into 'master'
[eacsl] Fix generated pointer in `&a[x..y]` annotation Closes e-acsl#148 See merge request frama-c/frama-c!3233
No related branches found
No related tags found
Showing
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/src/code_generator/memory_translate.ml 1 addition, 2 deletionssrc/plugins/e-acsl/src/code_generator/memory_translate.ml
- src/plugins/e-acsl/src/code_generator/translate.ml 4 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/src/libraries/misc.ml 0 additions, 3 deletionssrc/plugins/e-acsl/src/libraries/misc.ml
- src/plugins/e-acsl/src/libraries/misc.mli 0 additions, 2 deletionssrc/plugins/e-acsl/src/libraries/misc.mli
- src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
- src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c 25 additions, 6 deletions...ns/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
- src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c 37 additions, 38 deletionssrc/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
- src/plugins/e-acsl/tests/memory/ranges_in_builtins.c 5 additions, 0 deletionssrc/plugins/e-acsl/tests/memory/ranges_in_builtins.c
Loading
Please register or sign in to comment