Reputation: 1151
SPARK restricts the calling of potentially blocking subprograms from within protected objects.
However, I've noticed if I call ANY subprogram outside of the package in which the protected object lives I get the warning about a potentially blocking subprogram.
What is missing from the external package I'd like to use to tell it the call will be non-blocking? I've tried just putting a "add one to argument" subprogram in another package and it doesn't work. If I move it into the package containing the protected object it does.
What am I missing?
Upvotes: 2
Views: 137
Reputation: 1151
Thank you @shark8 for your detailed answer.
I examined the body of the method I was trying to call and as it was a simple return statement, it did not have any of the effects mentioned in the manual.
I did however discover that turning on SPARK_Mode => On
in the package I am trying to use fixed the issue.
Here's a MwE that reproduces the issue:
-- main.adb
pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);
with P1;
procedure Main is
begin
-- Insert code here.
null;
end Main;
-- simple.ads
package Simple is
procedure Do_Nothing;
end Simple;
-- simple.adb
package body Simple is
procedure Do_Nothing is
begin
null;
end Do_Nothing;
end Simple;
-- p1.ads
pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);
package P1 with
SPARK_Mode => On
is
protected Protected_Object with
SPARK_Mode => On
is
procedure Do_Something;
end Protected_Object;
end P1;
-- p1.adb
with Simple;
package body P1 with
SPARK_Mode => On
is
protected body Protected_Object
with
SPARK_Mode => On
is
procedure Do_Something is
begin
Simple.Do_Nothing;
end Do_Something;
end Protected_Object;
end P1;
Upvotes: 2
Reputation: 4198
In Ada 2020 there is an attribute Non_Blocking
which explicitly marks the blocking/nonblocking attributes for static-analysis and the compiler ensuring things are correct.
But this doesn't help if you're stuck in Ada 2012 — and there are specific things that are "potentially blocking" like entry-calls and [IIRC] things like Ada.Text_IO.Put
— and SPARK takes the reasoning that if it's potentially blocking then you cannot ensure that it's not non-blocking.
According to the RM, here's what you have to look out for:
During a protected action, it is a bounded error to invoke an operation that is potentially blocking. The following are defined to be potentially blocking operations:
- a select_statement;
- an accept_statement;
- an entry_call_statement;
- a delay_statement;
- an abort_statement;
- task creation or activation;
- an external call on a protected subprogram (or an external requeue) with the same target object as that of the protected action;
- a call on a subprogram whose body contains a potentially blocking operation.
So, if the subprogram you're trying to call has a select
, accept
, delay
, or task
it's potentially blocking.
Upvotes: 2