In Alfa mode for formal verification, the default is now to interpret compiler
permissions like GNAT does, with an option to have a stricter standard-only
interpretation. This is currently used for sizes of implicit base types of
integer types.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-27  Yannick Moy  <moy@adacore.com>

	* debug.adb (d.D): New option for strict Alfa mode.
	* opt.ads (Strict_Alfa_Mode): New flag to interpret compiler
	permissions as strictly as possible.
	* sem_ch3.adb (Signed_Integer_Type_Declaration): In non-strict
	Alfa mode, now, interpret ranges of base types like GNAT does; in
	strict mode, simply change the range of the implicit base Itype.
	* gnat1drv.adb: Update comments. Set Strict_Alfa_Mode.