[e-acsl] fixed bug with casts from integer to integral C type
[e-acsl] support of field accesses in logic [e-acsl] support of array accesses (yet missing guards) in logic [e-acsl] support of pointer dereferences (yet missing guards) in logic [e-acsl] support of \null in logic
Showing
- src/plugins/e-acsl/TODO 5 additions, 1 deletionsrc/plugins/e-acsl/TODO
- src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h 10 additions, 0 deletionssrc/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
- src/plugins/e-acsl/tests/e-acsl-runtime/array.i 17 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/array.i
- src/plugins/e-acsl/tests/e-acsl-runtime/cast.i 4 additions, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/cast.i
- src/plugins/e-acsl/tests/e-acsl-runtime/null.i 9 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/null.i
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle 1 addition, 1 deletion...gins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle 246 additions, 246 deletions...ugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.err.oracle 0 additions, 0 deletions...ugins/e-acsl/tests/e-acsl-runtime/oracle/array.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle 192 additions, 0 deletions...ugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle 101 additions, 2 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle 79 additions, 79 deletions.../e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle 129 additions, 129 deletions.../tests/e-acsl-runtime/oracle/function_contract.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c 7 additions, 5 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c 7 additions, 5 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c 604 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c 35 additions, 5 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c 7 additions, 5 deletions...ugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c 7 additions, 5 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c 7 additions, 5 deletions...-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c 7 additions, 5 deletions...e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
Loading
Please register or sign in to comment