diff options
Diffstat (limited to 'gcc/ada/lib-xref.adb')
| -rw-r--r-- | gcc/ada/lib-xref.adb | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index 9cc54eb..eb6ac0a 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -1126,12 +1126,14 @@ package body Lib.Xref is -- Comment needed here for special SPARK code ??? if GNATprove_Mode then - -- Ignore reference to an entity that is a Part_Of single + + -- Ignore references to an entity which is a Part_Of single -- concurrent object. Ideally we would prefer to add it as a -- reference to the corresponding concurrent type, but it is quite -- difficult (as such references are not currently added even for) -- reads/writes of private protected components) and not worth the -- effort. + if Ekind_In (Ent, E_Abstract_State, E_Constant, E_Variable) and then Present (Encapsulating_State (Ent)) and then Is_Single_Concurrent_Object (Encapsulating_State (Ent)) |