Merge branch 'feature/blanchard/wp/memaddr-theory' into 'master'

src/plugins/wp/MemAddr.ml

src/plugins/wp/MemAddr.mli

src/plugins/wp/MemMemory.ml

src/plugins/wp/MemMemory.mli

src/plugins/wp/MemRegion.ml

src/plugins/wp/MemTyped.ml

src/plugins/wp/TacHavoc.ml

src/plugins/wp/dune

src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw

src/plugins/wp/share/why3/frama_c_wp/memory.mlw

src/plugins/wp/share/wp.driver

src/plugins/wp/tests/why3/spec_memory.why

src/plugins/wp/tests/wp/oracle/sharing.res.oracle

...ns/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle

src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle

src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle

...ts/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle

src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle

src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle

src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle