Merge branch 'fix/wp/zero-real' into 'master'
[qed] fix int/real zero normalization See merge request frama-c/frama-c!4669
Showing
- src/libraries/qed/term.ml 52 additions, 28 deletionssrc/libraries/qed/term.ml
- src/plugins/wp/ProverWhy3.ml 15 additions, 6 deletionssrc/plugins/wp/ProverWhy3.ml
- src/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle 132 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/zero.0.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle 130 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/zero.1.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle 30 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle_qualif/zero.0.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle 30 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle_qualif/zero.1.res.oracle
- src/plugins/wp/tests/wp_acsl/zero.i 32 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/zero.i
Loading
Please register or sign in to comment