[E-ACSL] clause 'assumes' now checked during pre_analysis
[E-ACSL] fixed bug in Pre_analysis with pointer arithmetics in logic [E-ACSL] does not check some possible cases during pre analysis Thx to two first items, fully fixed bug #1324
Showing
- src/plugins/e-acsl/TODO 1 addition, 0 deletionssrc/plugins/e-acsl/TODO
- src/plugins/e-acsl/pre_analysis.ml 67 additions, 58 deletionssrc/plugins/e-acsl/pre_analysis.ml
- src/plugins/e-acsl/pre_analysis.mli 1 addition, 1 deletionsrc/plugins/e-acsl/pre_analysis.mli
- src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i 27 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle 0 additions, 0 deletions...s/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle 81 additions, 0 deletions...s/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.err.oracle 0 additions, 0 deletions...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle 90 additions, 0 deletions...ins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c 168 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c 293 additions, 0 deletions...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c 16 additions, 0 deletions...-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c 16 additions, 0 deletions...acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle 3 additions, 0 deletions...ests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle 3 additions, 0 deletions.../tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
Loading
Please register or sign in to comment