In Alfa mode, there is no use in applying formal verification to a codebase with a blatant error such as an access to a component not present in the type, so make the default warning an error in this mode.
Tested on x86_64-pc-linux-gnu, committed on trunk 2012-08-06 Yannick Moy <m...@adacore.com> * sem_ch4.adb (Analyze_Selected_Component): Issue an error in Alfa mode for component not present.
Index: sem_ch4.adb =================================================================== --- sem_ch4.adb (revision 190155) +++ sem_ch4.adb (working copy) @@ -4343,10 +4343,22 @@ -- Emit appropriate message. Gigi will replace the -- node subsequently with the appropriate Raise. - Apply_Compile_Time_Constraint_Error - (N, "component not present in }?", - CE_Discriminant_Check_Failed, - Ent => Prefix_Type, Rep => False); + -- In Alfa mode, this is an made into an error to + -- simplify the treatment of the formal verification + -- backend. + + if Alfa_Mode then + Apply_Compile_Time_Constraint_Error + (N, "component not present in }", + CE_Discriminant_Check_Failed, + Ent => Prefix_Type, Rep => False); + else + Apply_Compile_Time_Constraint_Error + (N, "component not present in }?", + CE_Discriminant_Check_Failed, + Ent => Prefix_Type, Rep => False); + end if; + Set_Raises_Constraint_Error (N); return; end if;