Merge branch 'fix/blanchard/wp/valid_obj' into 'master'
[wp] fix two proof failures with `\object_pointer` See merge request frama-c/frama-c!4788
No related branches found
No related tags found
Showing
- src/plugins/wp/MemAddr.ml 2 additions, 2 deletionssrc/plugins/wp/MemAddr.ml
- src/plugins/wp/MemAddr.mli 2 additions, 2 deletionssrc/plugins/wp/MemAddr.mli
- src/plugins/wp/MemTyped.ml 1 addition, 1 deletionsrc/plugins/wp/MemTyped.ml
- src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw 3 additions, 4 deletionssrc/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
- src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle 1 addition, 1 deletion...lugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
- src/plugins/wp/tests/why3/spec_memory.why 1 addition, 1 deletionsrc/plugins/wp/tests/why3/spec_memory.why
- src/plugins/wp/tests/wp_acsl/object_pointer.i 10 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/object_pointer.i
- src/plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle 49 additions, 32 deletions...plugins/wp/tests/wp_acsl/oracle/object_pointer.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle 13 additions, 8 deletions.../wp/tests/wp_acsl/oracle_qualif/object_pointer.res.oracle
Loading
Please register or sign in to comment