Merge branch 'fix/kernel/logic-decay' into 'master'
Rejects C arrays as argument of builtin ACSL predicates See merge request frama-c/e-acsl!177
Showing
- src/plugins/e-acsl/tests/runtime/base_addr.c 7 additions, 5 deletionssrc/plugins/e-acsl/tests/runtime/base_addr.c
- src/plugins/e-acsl/tests/runtime/block_length.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/runtime/block_length.c
- src/plugins/e-acsl/tests/runtime/compound_initializers.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/runtime/compound_initializers.c
- src/plugins/e-acsl/tests/runtime/freeable.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/runtime/freeable.c
- src/plugins/e-acsl/tests/runtime/initialized.c 3 additions, 3 deletionssrc/plugins/e-acsl/tests/runtime/initialized.c
- src/plugins/e-acsl/tests/runtime/offset.c 2 additions, 2 deletionssrc/plugins/e-acsl/tests/runtime/offset.c
- src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle 5 additions, 5 deletionssrc/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
- src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c 132 additions, 112 deletionssrc/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
Loading
Please register or sign in to comment