Merge branch 'feature/basile/eacsl-31-disjoint-separated' into 'master'
[eacsl] Add support of `\separated` See merge request frama-c/frama-c!2767
Showing
- src/plugins/e-acsl/doc/Changelog 4 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/doc/refman/intro_modern.tex 0 additions, 1 deletionsrc/plugins/e-acsl/doc/refman/intro_modern.tex
- src/plugins/e-acsl/doc/refman/memory.tex 1 addition, 1 deletionsrc/plugins/e-acsl/doc/refman/memory.tex
- src/plugins/e-acsl/doc/refman/speclang_modern.tex 1 addition, 2 deletionssrc/plugins/e-acsl/doc/refman/speclang_modern.tex
- src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c 8 additions, 2 deletions...on_model/bittree_model/e_acsl_bittree_observation_model.c
- src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c 74 additions, 0 deletions...share/e-acsl/observation_model/e_acsl_observation_model.c
- src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h 23 additions, 1 deletion...share/e-acsl/observation_model/e_acsl_observation_model.h
- src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c 6 additions, 1 deletion...on_model/segment_model/e_acsl_segment_observation_model.c
- src/plugins/e-acsl/src/analyses/memory_tracking.ml 7 additions, 1 deletionsrc/plugins/e-acsl/src/analyses/memory_tracking.ml
- src/plugins/e-acsl/src/analyses/typing.ml 6 additions, 2 deletionssrc/plugins/e-acsl/src/analyses/typing.ml
- src/plugins/e-acsl/src/analyses/typing.mli 5 additions, 2 deletionssrc/plugins/e-acsl/src/analyses/typing.mli
- src/plugins/e-acsl/src/code_generator/memory_translate.ml 297 additions, 163 deletionssrc/plugins/e-acsl/src/code_generator/memory_translate.ml
- src/plugins/e-acsl/src/code_generator/memory_translate.mli 10 additions, 10 deletionssrc/plugins/e-acsl/src/code_generator/memory_translate.mli
- src/plugins/e-acsl/src/code_generator/translate.ml 34 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle 0 additions, 4 deletionssrc/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
- src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c 79 additions, 13 deletionssrc/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
- src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c 15 additions, 3 deletionssrc/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
- src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c 15 additions, 0 deletionssrc/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
- src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle 3 additions, 3 deletionssrc/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
- src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c 282 additions, 236 deletions...ns/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
Loading
Please register or sign in to comment