Merge branch 'feature/eva/modulo-alarms' into 'master'
[Eva] Improves the emission of integer overflow alarms on a/b and a%b See merge request frama-c/frama-c!4809
Showing
- Changelog 3 additions, 0 deletionsChangelog
- src/plugins/eva/ast/eva_ast_builder.ml 1 addition, 0 deletionssrc/plugins/eva/ast/eva_ast_builder.ml
- src/plugins/eva/ast/eva_ast_builder.mli 1 addition, 0 deletionssrc/plugins/eva/ast/eva_ast_builder.mli
- src/plugins/eva/engine/evaluation.ml 67 additions, 13 deletionssrc/plugins/eva/engine/evaluation.ml
- src/plugins/eva/utils/eval_typ.ml 7 additions, 0 deletionssrc/plugins/eva/utils/eval_typ.ml
- src/plugins/eva/utils/eval_typ.mli 4 additions, 0 deletionssrc/plugins/eva/utils/eval_typ.mli
- src/plugins/rte/rte.ml 1 addition, 4 deletionssrc/plugins/rte/rte.ml
- src/plugins/rte/visit.ml 4 additions, 4 deletionssrc/plugins/rte/visit.ml
- src/plugins/wp/tests/wp_gallery/euclid.c 1 addition, 0 deletionssrc/plugins/wp/tests/wp_gallery/euclid.c
- src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle 8 additions, 5 deletions...ugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
- tests/rte/oracle/divmod.res.oracle 8 additions, 0 deletionstests/rte/oracle/divmod.res.oracle
- tests/rte/oracle/divmod_typedef.res.oracle 8 additions, 0 deletionstests/rte/oracle/divmod_typedef.res.oracle
- tests/value/div.i 54 additions, 4 deletionstests/value/div.i
- tests/value/modulo.i 49 additions, 1 deletiontests/value/modulo.i
- tests/value/oracle/addition.res.oracle 7 additions, 10 deletionstests/value/oracle/addition.res.oracle
- tests/value/oracle/div.1.res.oracle 0 additions, 138 deletionstests/value/oracle/div.1.res.oracle
- tests/value/oracle/div.res.oracle 90 additions, 17 deletionstests/value/oracle/div.res.oracle
- tests/value/oracle/modulo.res.oracle 62 additions, 19 deletionstests/value/oracle/modulo.res.oracle
- tests/value/oracle_equality/addition.res.oracle 9 additions, 8 deletionstests/value/oracle_equality/addition.res.oracle
Loading
Please register or sign in to comment