ada: Update Assertion_Policy handling in GNATProve mode

ada: Update Assertion_Policy handling in GNATProve mode

Previously in GNATProve_Mode the frontend would overwrite all of
the assertion policies to check in order to force the generation
of all of the assertions.

This however prevents GNATProve from performing policy related
checks in the tool. Since they are all artificially changed to
check.

This patch removes the modifications to the applicable assertion
policies and instead prevents code from ignored entities being
removed when in GNATProve_Mode.

gcc/ada/ChangeLog:

	* contracts.adb: Use Is_Ignored_In_Codegen instead of just
	using Is_Ignored.
	* exp_ch6.adb: Likewise.
	* exp_prag.adb: Likewise.
	* exp_util.adb: Likewise.
	* frontend.adb: Avoid removal of ignored nodes in GNATProve_Mode.
	* gnat1drv.adb: Avoid forcing Assertions_Enabled in GNATProve_Mode.
	* lib-writ.adb (Write_With_File_Names): Avoid early exit
	with ignored entities in GNATProve_Mode.
	* lib-xref.adb: Likewise.
	* opt.adb: Remove check for Assertions_Enabled.
	* sem_attr.adb: Use Is_Ignored_In_Codegen instead of Is_Ignored.
	* sem_ch13.adb: Likewise. Additionally always add predicates in
	GNATProve_Mode.
	* sem_prag.adb: Likewise. Additionally remove modifications
	to applied policies in GNATProve_Mode.
	* sem_util.adb (Is_Ignored_In_Codegen): New function that overrides
	Is_Ignored in GNATProve_Mode and Codepeer_Mode.
	(Is_Ignored_Ghost_Pragma_In_Codegen): Likewise for
	Is_Ignored_Ghost_Pragma.
	(Is_Ignored_Ghost_Entity_In_Codegen): Likewise for
	Is_Ignored_Ghost_Entity.
	(Policy_In_List): Remove overriding of policies in GNATProve_Mode.
	* sem_util.ads: Add specs for new functions.
	* (Predicates_Enabled): Always generate predicates in
	GNATProve_Mode.