-- SPARK_Mode --
----------------
- -- pragma SPARK_Mode [(On | Off)];
+ -- pragma SPARK_Mode [(Auto | On | Off)];
when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
Mode_Id : SPARK_Mode_Type;
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
- Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
+ Check_Arg_Is_One_Of (Arg1, Name_Auto, Name_On, Name_Off);
Mode := Chars (Get_Pragma_Arg (Arg1));
else
Mode := Name_On;
-- the pragma resides to find a potential construct.
else
+ -- An explicit mode of Auto is only allowed as a configuration
+ -- pragma. Escape "pragma" to avoid replacement with "aspect".
+
+ if Mode_Id = None then
+ Error_Pragma_Arg
+ ("only configuration 'p'r'a'g'm'a% can have value &",
+ Arg1);
+ end if;
+
Stmt := Prev (N);
while Present (Stmt) loop
function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type is
begin
- if N = Name_On then
+ if N = Name_Auto then
+ return None;
+ elsif N = Name_On then
return On;
elsif N = Name_Off then
return Off;
Name_Assertion : constant Name_Id := N + $;
Name_Assertions : constant Name_Id := N + $;
Name_Attribute_Name : constant Name_Id := N + $;
+ Name_Auto : constant Name_Id := N + $;
Name_Body_File_Name : constant Name_Id := N + $;
Name_Boolean_Entry_Barriers : constant Name_Id := N + $;
Name_By_Any : constant Name_Id := N + $;