Merge branch 'fix/eva/subdivision-strategy' into 'master'
[Eva] Adjusts the strategy to subdivide floating-point intervals Closes Value/Value#128 See merge request frama-c/frama-c!2539
Showing
- src/kernel_services/abstract_interp/float_interval.ml 15 additions, 13 deletionssrc/kernel_services/abstract_interp/float_interval.ml
- src/kernel_services/plugin_entry_points/kernel.ml 2 additions, 2 deletionssrc/kernel_services/plugin_entry_points/kernel.ml
- src/plugins/value/engine/subdivided_evaluation.ml 35 additions, 12 deletionssrc/plugins/value/engine/subdivided_evaluation.ml
- src/plugins/value/eval.ml 2 additions, 2 deletionssrc/plugins/value/eval.ml
- tests/float/nonlin.c 41 additions, 1 deletiontests/float/nonlin.c
- tests/float/oracle/nonlin.0.res.oracle 114 additions, 60 deletionstests/float/oracle/nonlin.0.res.oracle
- tests/float/oracle/nonlin.1.res.oracle 159 additions, 95 deletionstests/float/oracle/nonlin.1.res.oracle
- tests/float/oracle/nonlin.2.res.oracle 174 additions, 115 deletionstests/float/oracle/nonlin.2.res.oracle
- tests/float/oracle/nonlin.3.res.oracle 159 additions, 128 deletionstests/float/oracle/nonlin.3.res.oracle
- tests/float/oracle/nonlin.4.res.oracle 392 additions, 0 deletionstests/float/oracle/nonlin.4.res.oracle
- tests/float/oracle/nonlin.5.res.oracle 364 additions, 0 deletionstests/float/oracle/nonlin.5.res.oracle
- tests/misc/oracle/widen_hints_float.res.oracle 1 addition, 1 deletiontests/misc/oracle/widen_hints_float.res.oracle
- tests/value/nonlin.c 3 additions, 5 deletionstests/value/nonlin.c
- tests/value/oracle/nonlin.res.oracle 36 additions, 36 deletionstests/value/oracle/nonlin.res.oracle
Loading
Please register or sign in to comment