Merge branch 'bugfix/basile/eacsl134-rte-assumes' into 'master'
[eacsl] Ensure that RTE are checked for every part of a specification Closes e-acsl#134 See merge request frama-c/frama-c!2965
No related branches found
No related tags found
Showing
- src/plugins/e-acsl/src/code_generator/env.ml 18 additions, 5 deletionssrc/plugins/e-acsl/src/code_generator/env.ml
- src/plugins/e-acsl/src/code_generator/env.mli 19 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/env.mli
- src/plugins/e-acsl/src/code_generator/memory_translate.ml 12 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/memory_translate.ml
- src/plugins/e-acsl/src/code_generator/translate.ml 86 additions, 58 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/src/code_generator/translate_annots.ml 16 additions, 6 deletionssrc/plugins/e-acsl/src/code_generator/translate_annots.ml
- src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle 4 additions, 0 deletions...s/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
- src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c 61 additions, 21 deletions.../tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
- src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c 168 additions, 0 deletionssrc/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c
- src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle 13 additions, 0 deletionssrc/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle
- src/plugins/e-acsl/tests/constructs/oracle_dev/rte.e-acsl.err.log 0 additions, 0 deletions...ins/e-acsl/tests/constructs/oracle_dev/rte.e-acsl.err.log
- src/plugins/e-acsl/tests/constructs/rte.i 26 additions, 0 deletionssrc/plugins/e-acsl/tests/constructs/rte.i
- src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c 10 additions, 4 deletions...ins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
- src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c 31 additions, 13 deletions...plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
Loading
Please register or sign in to comment