Merge branch 'master' into feature/nupw/updates-argon

# Conflicts:
#	src/kernel_services/ast_data/property.ml
#	src/kernel_services/ast_data/property.mli
#	src/libraries/utils/sanitizer.ml
#	src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
#	src/plugins/wp/tests/wp/sharing.c.0.report.json
#	src/plugins/wp/tests/wp/wp_behav.c.0.report.json
#	src/plugins/wp/tests/wp/wp_call_pre.c.0.report.json
#	src/plugins/wp/tests/wp/wp_eqb.i.0.report.json
#	src/plugins/wp/tests/wp/wp_strategy.c.0.report.json
#	src/plugins/wp/tests/wp_acsl/assigns_path.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/assigns_range.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/cnf.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/div_mod.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/e_imply.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/equal.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/init_value.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/init_value.i.1.report.json
#	src/plugins/wp/tests/wp_acsl/init_value_mem.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/logic.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/looplabels.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
#	src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
#	src/plugins/wp/tests/wp_acsl/range.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/reads.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/record.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/simpl_is_type.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/struct_use_case.i.0.report.json
#	src/plugins/wp/tests/wp_acsl/unit_bit_test.c.0.report.json
#	src/plugins/wp/tests/wp_bts/bts0843.i.0.report.json
#	src/plugins/wp/tests/wp_bts/bts788.i.0.report.json
#	src/plugins/wp/tests/wp_bts/bts_1601.c.0.report.json
#	src/plugins/wp/tests/wp_bts/bts_2159.i.0.report.json
#	src/plugins/wp/tests/wp_bts/issue_508.c.0.report.json
#	src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i.0.report.json
#	src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
#	src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
#	src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json
#	src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c.0.report.json
#	src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
#	src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
#	src/plugins/wp/tests/wp_hoare/byref.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/byref.i.1.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var2.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/dispatch_var2.i.1.report.json
#	src/plugins/wp/tests/wp_hoare/logicref.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/logicref_simple.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
#	src/plugins/wp/tests/wp_hoare/reference.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/reference_and_struct.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/reference_array.i.0.report.json
#	src/plugins/wp/tests/wp_hoare/refguards.i.0.report.json
#	src/plugins/wp/tests/wp_manual/manual.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/bool.i.1.report.json
#	src/plugins/wp/tests/wp_plugin/copy.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/init_const_guard.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/initarr.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/injector.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
#	src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
#	src/plugins/wp/tests/wp_plugin/overassign.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/prenex.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/repeat.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/sequence.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/stmt.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
#	src/plugins/wp/tests/wp_plugin/struct_hack.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/subset.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/trig.i.0.report.json
#	src/plugins/wp/tests/wp_plugin/unsupported_init.i.0.report.json
#	src/plugins/wp/tests/wp_store/struct.i.0.report.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_And_bis.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Goal_Exist_Or.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_And.json
#	src/plugins/wp/tests/wp_tip/tac_split_quantifiers/wp/typed/typed_split_ensures_Hyp_Forall_Or_bis.json
#	src/plugins/wp/tests/wp_typed/array_initialized.c.1.report.json
#	src/plugins/wp/tests/wp_typed/avar.i.0.report.json
#	src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
#	src/plugins/wp/tests/wp_typed/struct_array_type.i.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_bitwise.c.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_local.c.0.report.json
#	src/plugins/wp/tests/wp_typed/unit_local.c.1.report.json
#	src/plugins/wp/tests/wp_typed/unit_tset.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_bitwise.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_collect.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_init.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_swap.i.0.report.json
#	src/plugins/wp/tests/wp_typed/user_swap.i.1.report.json
#	src/plugins/wp/tests/wp_usage/caveat2.i.0.report.json
#	src/plugins/wp/tests/wp_usage/caveat_range.i.0.report.json
#	src/plugins/wp/tests/wp_usage/issue-189-bis.i.0.report.json
#	src/plugins/wp/tests/wp_usage/issue-189-bis.i.1.report.json