===================================================================
@@ -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;
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 <trojanek@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.