[E-ACSL] fixed bug #1390 about typing of logic variables of type long long
[E-ACSL] compute a more precise type for quantified variable with a strict upper bound [E-ACSL] do not modify the type of a quantified variable anymore
Showing
- src/plugins/e-acsl/env.ml 13 additions, 11 deletionssrc/plugins/e-acsl/env.ml
- src/plugins/e-acsl/env.mli 1 addition, 1 deletionsrc/plugins/e-acsl/env.mli
- src/plugins/e-acsl/mpz.ml 1 addition, 1 deletionsrc/plugins/e-acsl/mpz.ml
- src/plugins/e-acsl/quantif.ml 8 additions, 9 deletionssrc/plugins/e-acsl/quantif.ml
- src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c 27 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle 0 additions, 0 deletions...s/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle 22 additions, 0 deletions...s/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle 0 additions, 0 deletions...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle 23 additions, 0 deletions...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c 8 additions, 8 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c 3 additions, 3 deletions...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c 294 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c 331 additions, 0 deletions...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c 9 additions, 9 deletions...ns/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c 15 additions, 12 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c 4 additions, 5 deletions...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
- src/plugins/e-acsl/tests/test_config.in 1 addition, 1 deletionsrc/plugins/e-acsl/tests/test_config.in
- src/plugins/e-acsl/translate.ml 1 addition, 2 deletionssrc/plugins/e-acsl/translate.ml
- src/plugins/e-acsl/typing.ml 2 additions, 0 deletionssrc/plugins/e-acsl/typing.ml
Loading
Please register or sign in to comment