[multiple changes]
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Check_In_Out_States.Check_Constituent_Usage): Update the comment on usage. Reimplemented. (Check_Input_States.Check_Constituent_Usage): Update the comment on usage. A Proof_In constituent can now refine an Input state as long as there is at least one Input constituent present. 2016-04-18 Ed Schonberg <schonberg@adacore.com> * sem_ch6.adb (Check_Inline_Pragma): Use the Sloc of the body id as the sloc of the entity in the generated subprogram declaration, to avoid spurious conformance errors when style checks are enabled. From-SVN: r235137
This commit is contained in:
parent
a6363ed30e
commit
274c2cda3e
|
@ -1,3 +1,18 @@
|
||||||
|
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
|
||||||
|
|
||||||
|
* sem_prag.adb (Check_In_Out_States.Check_Constituent_Usage):
|
||||||
|
Update the comment on usage. Reimplemented.
|
||||||
|
(Check_Input_States.Check_Constituent_Usage): Update the comment
|
||||||
|
on usage. A Proof_In constituent can now refine an Input state
|
||||||
|
as long as there is at least one Input constituent present.
|
||||||
|
|
||||||
|
2016-04-18 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
|
* sem_ch6.adb (Check_Inline_Pragma): Use the Sloc of the
|
||||||
|
body id as the sloc of the entity in the generated subprogram
|
||||||
|
declaration, to avoid spurious conformance errors when style
|
||||||
|
checks are enabled.
|
||||||
|
|
||||||
2016-04-18 Ed Schonberg <schonberg@adacore.com>
|
2016-04-18 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
* sem_ch4.adb (Analyze_Selected_Component, Has_Dereference):
|
* sem_ch4.adb (Analyze_Selected_Component, Has_Dereference):
|
||||||
|
|
|
@ -2556,6 +2556,7 @@ package body Sem_Ch6 is
|
||||||
or else (Pragma_Name (N) = Name_Inline
|
or else (Pragma_Name (N) = Name_Inline
|
||||||
and then
|
and then
|
||||||
(Front_End_Inlining or else Optimization_Level > 0)))
|
(Front_End_Inlining or else Optimization_Level > 0)))
|
||||||
|
and then Present (Pragma_Argument_Associations (N))
|
||||||
then
|
then
|
||||||
declare
|
declare
|
||||||
Pragma_Arg : Node_Id :=
|
Pragma_Arg : Node_Id :=
|
||||||
|
@ -2606,11 +2607,14 @@ package body Sem_Ch6 is
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
else
|
else
|
||||||
-- Create a subprogram declaration, to make treatment uniform
|
-- Create a subprogram declaration, to make treatment uniform.
|
||||||
|
-- Make the sloc of the subprogram name that of the entity in
|
||||||
|
-- the body, so that style checks find identical strings.
|
||||||
|
|
||||||
declare
|
declare
|
||||||
Subp : constant Entity_Id :=
|
Subp : constant Entity_Id :=
|
||||||
Make_Defining_Identifier (Loc, Chars (Body_Id));
|
Make_Defining_Identifier
|
||||||
|
(Sloc (Body_Id), Chars (Body_Id));
|
||||||
Decl : constant Node_Id :=
|
Decl : constant Node_Id :=
|
||||||
Make_Subprogram_Declaration (Loc,
|
Make_Subprogram_Declaration (Loc,
|
||||||
Specification =>
|
Specification =>
|
||||||
|
|
|
@ -24246,11 +24246,12 @@ package body Sem_Prag is
|
||||||
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
||||||
-- Determine whether one of the following coverage scenarios is in
|
-- Determine whether one of the following coverage scenarios is in
|
||||||
-- effect:
|
-- effect:
|
||||||
-- 1) there is at least one constituent of mode In_Out
|
-- 1) there is at least one constituent of mode In_Out or Output
|
||||||
-- 2) there is at least one Input and one Output constituent
|
-- 2) there is at least one pair of constituents with modes Input
|
||||||
-- 3) not all constituents are present and one of them is of mode
|
-- and Output, or Proof_In and Output.
|
||||||
-- Output.
|
-- 3) there is at least one constituent of mode Output and not all
|
||||||
-- If this is not the case, emit an error.
|
-- constituents are present.
|
||||||
|
-- If this is not the case, emit an error (SPARK RM 7.2.4(5)).
|
||||||
|
|
||||||
-----------------------------
|
-----------------------------
|
||||||
-- Check_Constituent_Usage --
|
-- Check_Constituent_Usage --
|
||||||
|
@ -24261,8 +24262,9 @@ package body Sem_Prag is
|
||||||
Constit_Id : Entity_Id;
|
Constit_Id : Entity_Id;
|
||||||
Has_Missing : Boolean := False;
|
Has_Missing : Boolean := False;
|
||||||
In_Out_Seen : Boolean := False;
|
In_Out_Seen : Boolean := False;
|
||||||
In_Seen : Boolean := False;
|
Input_Seen : Boolean := False;
|
||||||
Out_Seen : Boolean := False;
|
Output_Seen : Boolean := False;
|
||||||
|
Proof_In_Seen : Boolean := False;
|
||||||
|
|
||||||
begin
|
begin
|
||||||
-- Process all the constituents of the state and note their modes
|
-- Process all the constituents of the state and note their modes
|
||||||
|
@ -24273,22 +24275,16 @@ package body Sem_Prag is
|
||||||
Constit_Id := Node (Constit_Elmt);
|
Constit_Id := Node (Constit_Elmt);
|
||||||
|
|
||||||
if Present_Then_Remove (In_Constits, Constit_Id) then
|
if Present_Then_Remove (In_Constits, Constit_Id) then
|
||||||
In_Seen := True;
|
Input_Seen := True;
|
||||||
|
|
||||||
elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then
|
elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then
|
||||||
In_Out_Seen := True;
|
In_Out_Seen := True;
|
||||||
|
|
||||||
elsif Present_Then_Remove (Out_Constits, Constit_Id) then
|
elsif Present_Then_Remove (Out_Constits, Constit_Id) then
|
||||||
Out_Seen := True;
|
Output_Seen := True;
|
||||||
|
|
||||||
-- A Proof_In constituent cannot participate in the completion
|
|
||||||
-- of an Output state (SPARK RM 7.2.4(5)).
|
|
||||||
|
|
||||||
elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
|
elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
|
||||||
Error_Msg_Name_1 := Chars (State_Id);
|
Proof_In_Seen := True;
|
||||||
SPARK_Msg_NE
|
|
||||||
("constituent & of state % must have mode Input, In_Out "
|
|
||||||
& "or Output in global refinement", N, Constit_Id);
|
|
||||||
|
|
||||||
else
|
else
|
||||||
Has_Missing := True;
|
Has_Missing := True;
|
||||||
|
@ -24297,26 +24293,41 @@ package body Sem_Prag is
|
||||||
Next_Elmt (Constit_Elmt);
|
Next_Elmt (Constit_Elmt);
|
||||||
end loop;
|
end loop;
|
||||||
|
|
||||||
-- A single In_Out constituent is a valid completion
|
-- An In_Out constituent is a valid completion
|
||||||
|
|
||||||
if In_Out_Seen then
|
if In_Out_Seen then
|
||||||
null;
|
null;
|
||||||
|
|
||||||
-- A pair of one Input and one Output constituent is a valid
|
-- A pair of one Input/Proof_In and one Output constituent is a
|
||||||
-- completion.
|
-- valid completion.
|
||||||
|
|
||||||
elsif In_Seen and Out_Seen then
|
elsif (Input_Seen or Proof_In_Seen) and Output_Seen then
|
||||||
null;
|
null;
|
||||||
|
|
||||||
|
elsif Output_Seen then
|
||||||
|
|
||||||
-- A single Output constituent is a valid completion only when
|
-- A single Output constituent is a valid completion only when
|
||||||
-- some of the other constituents are missing (SPARK RM 7.2.4(5)).
|
-- some of the other constituents are missing.
|
||||||
|
|
||||||
elsif Out_Seen and Has_Missing then
|
if Has_Missing then
|
||||||
null;
|
null;
|
||||||
|
|
||||||
|
-- Otherwise all constituents are of mode Output
|
||||||
|
|
||||||
|
else
|
||||||
|
SPARK_Msg_NE
|
||||||
|
("global refinement of state & must include at least one "
|
||||||
|
& "constituent of mode `In_Out`, `Input`, or `Proof_In`",
|
||||||
|
N, State_Id);
|
||||||
|
end if;
|
||||||
|
|
||||||
-- The state lacks a completion
|
-- The state lacks a completion
|
||||||
|
|
||||||
elsif not In_Seen and not In_Out_Seen and not Out_Seen then
|
elsif not Input_Seen
|
||||||
|
and not In_Out_Seen
|
||||||
|
and not Output_Seen
|
||||||
|
and not Proof_In_Seen
|
||||||
|
then
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("missing global refinement of state &", N, State_Id);
|
("missing global refinement of state &", N, State_Id);
|
||||||
|
|
||||||
|
@ -24373,8 +24384,8 @@ package body Sem_Prag is
|
||||||
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
||||||
-- Determine whether at least one constituent of state State_Id with
|
-- Determine whether at least one constituent of state State_Id with
|
||||||
-- visible refinement is used and has mode Input. Ensure that the
|
-- visible refinement is used and has mode Input. Ensure that the
|
||||||
-- remaining constituents do not have In_Out, Output or Proof_In
|
-- remaining constituents do not have In_Out or Output modes. Emit an
|
||||||
-- modes.
|
-- error if this is not the case (SPARK RM 7.2.4(5)).
|
||||||
|
|
||||||
-----------------------------
|
-----------------------------
|
||||||
-- Check_Constituent_Usage --
|
-- Check_Constituent_Usage --
|
||||||
|
@ -24395,17 +24406,22 @@ package body Sem_Prag is
|
||||||
if Present_Then_Remove (In_Constits, Constit_Id) then
|
if Present_Then_Remove (In_Constits, Constit_Id) then
|
||||||
In_Seen := True;
|
In_Seen := True;
|
||||||
|
|
||||||
|
-- A Proof_In constituent can refine an Input state as long as
|
||||||
|
-- there is at least one Input constituent present.
|
||||||
|
|
||||||
|
elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
|
||||||
|
null;
|
||||||
|
|
||||||
-- The constituent appears in the global refinement, but has
|
-- The constituent appears in the global refinement, but has
|
||||||
-- mode In_Out, Output or Proof_In (SPARK RM 7.2.4(5)).
|
-- mode In_Out or Output (SPARK RM 7.2.4(5)).
|
||||||
|
|
||||||
elsif Present_Then_Remove (In_Out_Constits, Constit_Id)
|
elsif Present_Then_Remove (In_Out_Constits, Constit_Id)
|
||||||
or else Present_Then_Remove (Out_Constits, Constit_Id)
|
or else Present_Then_Remove (Out_Constits, Constit_Id)
|
||||||
or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
|
|
||||||
then
|
then
|
||||||
Error_Msg_Name_1 := Chars (State_Id);
|
Error_Msg_Name_1 := Chars (State_Id);
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("constituent & of state % must have mode Input in global "
|
("constituent & of state % must have mode `Input` in "
|
||||||
& "refinement", N, Constit_Id);
|
& "global refinement", N, Constit_Id);
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
Next_Elmt (Constit_Elmt);
|
Next_Elmt (Constit_Elmt);
|
||||||
|
@ -24416,7 +24432,7 @@ package body Sem_Prag is
|
||||||
if not In_Seen then
|
if not In_Seen then
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("global refinement of state & must include at least one "
|
("global refinement of state & must include at least one "
|
||||||
& "constituent of mode Input", N, State_Id);
|
& "constituent of mode `Input`", N, State_Id);
|
||||||
end if;
|
end if;
|
||||||
end Check_Constituent_Usage;
|
end Check_Constituent_Usage;
|
||||||
|
|
||||||
|
@ -24464,7 +24480,7 @@ package body Sem_Prag is
|
||||||
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
procedure Check_Constituent_Usage (State_Id : Entity_Id);
|
||||||
-- Determine whether all constituents of state State_Id with visible
|
-- Determine whether all constituents of state State_Id with visible
|
||||||
-- refinement are used and have mode Output. Emit an error if this is
|
-- refinement are used and have mode Output. Emit an error if this is
|
||||||
-- not the case.
|
-- not the case (SPARK RM 7.2.4(5)).
|
||||||
|
|
||||||
-----------------------------
|
-----------------------------
|
||||||
-- Check_Constituent_Usage --
|
-- Check_Constituent_Usage --
|
||||||
|
@ -24492,7 +24508,7 @@ package body Sem_Prag is
|
||||||
then
|
then
|
||||||
Error_Msg_Name_1 := Chars (State_Id);
|
Error_Msg_Name_1 := Chars (State_Id);
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("constituent & of state % must have mode Output in "
|
("constituent & of state % must have mode `Output` in "
|
||||||
& "global refinement", N, Constit_Id);
|
& "global refinement", N, Constit_Id);
|
||||||
|
|
||||||
-- The constituent is altogether missing (SPARK RM 7.2.5(3))
|
-- The constituent is altogether missing (SPARK RM 7.2.5(3))
|
||||||
|
@ -24501,7 +24517,7 @@ package body Sem_Prag is
|
||||||
if not Posted then
|
if not Posted then
|
||||||
Posted := True;
|
Posted := True;
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("output state & must be replaced by all its "
|
("`Output` state & must be replaced by all its "
|
||||||
& "constituents in global refinement", N, State_Id);
|
& "constituents in global refinement", N, State_Id);
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
@ -24559,6 +24575,7 @@ package body Sem_Prag is
|
||||||
-- Determine whether at least one constituent of state State_Id with
|
-- Determine whether at least one constituent of state State_Id with
|
||||||
-- visible refinement is used and has mode Proof_In. Ensure that the
|
-- visible refinement is used and has mode Proof_In. Ensure that the
|
||||||
-- remaining constituents do not have Input, In_Out or Output modes.
|
-- remaining constituents do not have Input, In_Out or Output modes.
|
||||||
|
-- Emit an error of this is not the case (SPARK RM 7.2.4(5)).
|
||||||
|
|
||||||
-----------------------------
|
-----------------------------
|
||||||
-- Check_Constituent_Usage --
|
-- Check_Constituent_Usage --
|
||||||
|
@ -24588,7 +24605,7 @@ package body Sem_Prag is
|
||||||
then
|
then
|
||||||
Error_Msg_Name_1 := Chars (State_Id);
|
Error_Msg_Name_1 := Chars (State_Id);
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("constituent & of state % must have mode Proof_In in "
|
("constituent & of state % must have mode `Proof_In` in "
|
||||||
& "global refinement", N, Constit_Id);
|
& "global refinement", N, Constit_Id);
|
||||||
end if;
|
end if;
|
||||||
|
|
||||||
|
@ -24600,7 +24617,7 @@ package body Sem_Prag is
|
||||||
if not Proof_In_Seen then
|
if not Proof_In_Seen then
|
||||||
SPARK_Msg_NE
|
SPARK_Msg_NE
|
||||||
("global refinement of state & must include at least one "
|
("global refinement of state & must include at least one "
|
||||||
& "constituent of mode Proof_In", N, State_Id);
|
& "constituent of mode `Proof_In`", N, State_Id);
|
||||||
end if;
|
end if;
|
||||||
end Check_Constituent_Usage;
|
end Check_Constituent_Usage;
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue