Merge branch 'feature/wp/base-offset' into 'master'
Fixes "[wp] unsoundness for base-offset" Closes #887 See merge request frama-c/frama-c!2843
No related branches found
No related tags found
Showing
- src/plugins/wp/MemMemory.ml 11 additions, 3 deletionssrc/plugins/wp/MemMemory.ml
- src/plugins/wp/MemMemory.mli 1 addition, 1 deletionsrc/plugins/wp/MemMemory.mli
- src/plugins/wp/MemTyped.ml 1 addition, 1 deletionsrc/plugins/wp/MemTyped.ml
- src/plugins/wp/share/coqwp/Memory.v 25 additions, 7 deletionssrc/plugins/wp/share/coqwp/Memory.v
- src/plugins/wp/share/why3/frama_c_wp/memory.mlw 11 additions, 2 deletionssrc/plugins/wp/share/why3/frama_c_wp/memory.mlw
- src/plugins/wp/tests/wp_acsl/base_offset.i 13 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/base_offset.i
- src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle 18 additions, 3 deletionssrc/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle 8 additions, 5 deletions...ins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
- src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json 2 additions, 2 deletions...t.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
- src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json 2 additions, 2 deletions...1.session/script/init_t2_bis_v2_assigns_normal_part2.json
- src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json 2 additions, 2 deletions...t.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
- src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json 2 additions, 2 deletions...t.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
Loading
Please register or sign in to comment