+2018-10-09 Maroua Maalej <maalej@adacore.com>
+
+ * sem_spark.adb (Check_Declaration): fix bug related to non
+ access object permissions.
+
2018-10-09 Doug Rupp <rupp@adacore.com>
* libgnat/a-ncelfu.ads: Fix name in header to match package.
end if;
end if;
- elsif Nkind_In (Expression (Decl),
- N_Attribute_Reference,
- N_Attribute_Reference,
- N_Expanded_Name,
- N_Explicit_Dereference,
- N_Indexed_Component,
- N_Reference,
- N_Selected_Component,
- N_Slice)
- then
- if Is_Access_Type (Etype (Prefix (Expression (Decl))))
- or else Is_Deep (Etype (Prefix (Expression (Decl))))
- then
- Current_Checking_Mode := Observe;
- Check := True;
- end if;
end if;
end if;
Check_Node (Expression (Decl));
end if;
- -- If lhs is not a pointer, we still give it the appropriate
+ -- If lhs is not a pointer, we still give it the unrestricted
-- state which is useless but not harmful.
declare
when N_Attribute_Reference =>
case Attribute_Name (Expr) is
when Name_Access =>
- Error_Msg_N ("access attribute not allowed in SPARK", Expr);
+ Error_Msg_N ("access attribute not allowed", Expr);
when Name_Last
| Name_First