Merge branch 'feature/virgile/acsl-float-comparisons' into 'master'
[ACSL] coerce comparisons from floats to real Closes #608 See merge request frama-c/frama-c!2152
No related branches found
No related tags found
Showing
- Makefile 3 additions, 3 deletionsMakefile
- src/kernel_services/ast_queries/logic_typing.ml 34 additions, 9 deletionssrc/kernel_services/ast_queries/logic_typing.ml
- src/kernel_services/plugin_entry_points/kernel.ml 3 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.ml
- src/kernel_services/plugin_entry_points/kernel.mli 2 additions, 0 deletionssrc/kernel_services/plugin_entry_points/kernel.mli
- src/plugins/wp/Cfloat.ml 56 additions, 23 deletionssrc/plugins/wp/Cfloat.ml
- src/plugins/wp/Cmath.mli 2 additions, 0 deletionssrc/plugins/wp/Cmath.mli
- src/plugins/wp/LogicBuiltins.ml 1 addition, 1 deletionsrc/plugins/wp/LogicBuiltins.ml
- src/plugins/wp/LogicSemantics.ml 5 additions, 1 deletionsrc/plugins/wp/LogicSemantics.ml
- src/plugins/wp/doc/manual/wp_builtins.tex 14 additions, 0 deletionssrc/plugins/wp/doc/manual/wp_builtins.tex
- src/plugins/wp/tests/wp_acsl/float_compare.i 23 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/float_compare.i
- src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json 39 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
- src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle 3 additions, 3 deletions...plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle 35 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle 17 additions, 0 deletions...s/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
- tests/spec/float-acsl.i 10 additions, 0 deletionstests/spec/float-acsl.i
- tests/spec/oracle/float-acsl.res.oracle 17 additions, 0 deletionstests/spec/oracle/float-acsl.res.oracle
Loading
Please register or sign in to comment