This patch modifies the processing of aspect or pragma SPARK_Mode to avoid a
crash when the annotation appears with an illegal mode.
------------
-- Source --
------------
-- pack.ads
package Pack is
package Nested_1 with SPARK_Mode => False is
end Nested_1;
Obj : constant String := "Illegal";
package Nested_2 with SPARK_Mode => Obj is
end Nested_2;
package Nested_3 is
pragma SPARK_Mode (True);
end Nested_3;
package Nested_4 is
pragma SPARK_Mode (1.2);
end Nested_4;
end Pack;
-----------------
-- Compilation --
-----------------
$ gcc -c pack.ads
$ gcc -c pack.ads -gnatd.F
pack.ads:2:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:7:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:11:26: argument for pragma "Spark_Mode" must be "On" or "Off"
pack.ads:15:26: argument for pragma "Spark_Mode" must be identifier
pack.ads:2:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:7:40: entity for aspect "Spark_Mode" must be "On" or "Off"
pack.ads:11:26: argument for pragma "Spark_Mode" must be "On" or "Off"
pack.ads:15:26: argument for pragma "Spark_Mode" must be identifier
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-09 Piotr Trojanek <troja...@adacore.com>
* sem_prag.adb (Analyze_Part_Of): Reword error message.
(Get_SPARK_Mode_Type): Do not raise Program_Error in case pragma
SPARK_Mode appears with an illegal mode, treat this as a non-existent
mode.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 254568)
+++ sem_prag.adb (working copy)
@@ -3287,8 +3287,8 @@
if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
SPARK_Msg_NE
- ("indicator Part_Of must denote abstract state or public "
- & "descendant of & (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote abstract state of & "
+ & "or of its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
@@ -3301,8 +3301,8 @@
else
SPARK_Msg_NE
- ("indicator Part_Of must denote abstract state or public "
- & "descendant of & (SPARK RM 7.2.6(3))",
+ ("indicator Part_Of must denote abstract state of & "
+ & "or of its public descendant (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
return;
end if;
@@ -29364,10 +29364,11 @@
elsif N = Name_Off then
return Off;
- -- Any other argument is illegal
+ -- Any other argument is illegal. Assume that no SPARK mode applies to
+ -- avoid potential cascaded errors.
else
- raise Program_Error;
+ return None;
end if;
end Get_SPARK_Mode_Type;
