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;

Reply via email to