src/plugins/wp/MemVar.ml

src/plugins/wp/MemoryContext.ml

src/plugins/wp/MemoryContext.mli

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

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

src/plugins/wp/tests/wp_hoare/alias_assigns_hypotheses.i

...tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle

.../wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle

...p_hoare/oracle_qualif/alias_assigns_hypotheses.res.oracle

...ts/wp_hoare/oracle_qualif/reference_and_struct.res.oracle

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

...ns/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle

...plugins/wp/tests/wp_typed/oracle/user_injector.res.oracle

...p/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle

...p/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle

src/plugins/wp/wp_parameters.ml

src/plugins/wp/wp_parameters.mli