[e-acsl] fix typing problem when using rationals
The occurrence of rationals in the following logic function lead to an assertion failure in Interval_utils.extract_ival, which was only defined for non-integer arguments. /*@ logic integer signum(ℝ x) = x > 0. ? 1 : x < 0. ? -1 : 0; */ Regression test added: src/plugins/e-acsl/tests/arith/sign_rational.c
Showing
- src/plugins/e-acsl/src/analyses/interval.ml 24 additions, 17 deletionssrc/plugins/e-acsl/src/analyses/interval.ml
- src/plugins/e-acsl/src/analyses/interval.mli 1 addition, 1 deletionsrc/plugins/e-acsl/src/analyses/interval.mli
- src/plugins/e-acsl/src/code_generator/quantif.ml 15 additions, 11 deletionssrc/plugins/e-acsl/src/code_generator/quantif.ml
- src/plugins/e-acsl/src/code_generator/translate_ats.ml 3 additions, 4 deletionssrc/plugins/e-acsl/src/code_generator/translate_ats.ml
- src/plugins/e-acsl/src/libraries/interval_utils.ml 2 additions, 2 deletionssrc/plugins/e-acsl/src/libraries/interval_utils.ml
- src/plugins/e-acsl/src/libraries/interval_utils.mli 2 additions, 2 deletionssrc/plugins/e-acsl/src/libraries/interval_utils.mli
- src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c 149 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
- src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle 4 additions, 0 deletions...lugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
- src/plugins/e-acsl/tests/arith/sign_rational.c 15 additions, 0 deletionssrc/plugins/e-acsl/tests/arith/sign_rational.c
Loading
Please register or sign in to comment