[multiple changes]
2012-12-05 Thomas Quinot <quinot@adacore.com> * par_sco.adb (Traverse_Aspects): Ensure we always have an entry in the sloc -> SCO map for invariants, since Set_SCO_Pragma_Enabled is called with that sloc when checks are enabled. 2012-12-05 Thomas Quinot <quinot@adacore.com> * exp_ch4.adb: Minor reformatting. 2012-12-05 Hristian Kirtchev <kirtchev@adacore.com> * par-prag.adb: Checks and processing of pragma Assume are carried out by Sem_Prag. * sem_prag.adb (Analyze_Pragma): Check the legality of pragma Assume. * snames.ads-tmpl: Add new name Assume. Add a pragma identifier for Assume. From-SVN: r194215
This commit is contained in:
parent
c116143c22
commit
1c66c4f5b7
6 changed files with 90 additions and 32 deletions
|
@ -1,3 +1,23 @@
|
|||
2012-12-05 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* par_sco.adb (Traverse_Aspects): Ensure we always have
|
||||
an entry in the sloc -> SCO map for invariants, since
|
||||
Set_SCO_Pragma_Enabled is called with that sloc when checks
|
||||
are enabled.
|
||||
|
||||
2012-12-05 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* exp_ch4.adb: Minor reformatting.
|
||||
|
||||
2012-12-05 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* par-prag.adb: Checks and processing of pragma Assume are
|
||||
carried out by Sem_Prag.
|
||||
* sem_prag.adb (Analyze_Pragma): Check the legality of pragma
|
||||
Assume.
|
||||
* snames.ads-tmpl: Add new name Assume. Add a pragma identifier
|
||||
for Assume.
|
||||
|
||||
2012-12-05 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* aspects.ads, aspects.adb: Add aspect Relative_Deadline.
|
||||
|
|
|
@ -10405,14 +10405,14 @@ package body Exp_Ch4 is
|
|||
-- Convert: x(y) to x'val (ytyp'val (y))
|
||||
|
||||
Rewrite (N,
|
||||
Make_Attribute_Reference (Loc,
|
||||
Prefix => New_Occurrence_Of (Target_Type, Loc),
|
||||
Attribute_Name => Name_Val,
|
||||
Expressions => New_List (
|
||||
Make_Attribute_Reference (Loc,
|
||||
Prefix => New_Occurrence_Of (Operand_Type, Loc),
|
||||
Attribute_Name => Name_Pos,
|
||||
Expressions => New_List (Operand)))));
|
||||
Make_Attribute_Reference (Loc,
|
||||
Prefix => New_Occurrence_Of (Target_Type, Loc),
|
||||
Attribute_Name => Name_Val,
|
||||
Expressions => New_List (
|
||||
Make_Attribute_Reference (Loc,
|
||||
Prefix => New_Occurrence_Of (Operand_Type, Loc),
|
||||
Attribute_Name => Name_Pos,
|
||||
Expressions => New_List (Operand)))));
|
||||
|
||||
Analyze_And_Resolve (N, Target_Type);
|
||||
end if;
|
||||
|
|
|
@ -1093,6 +1093,7 @@ begin
|
|||
|
||||
when Pragma_Abort_Defer |
|
||||
Pragma_Assertion_Policy |
|
||||
Pragma_Assume |
|
||||
Pragma_Assume_No_Invalid_Values |
|
||||
Pragma_AST_Entry |
|
||||
Pragma_All_Calls_Remote |
|
||||
|
|
|
@ -493,14 +493,14 @@ package body Par_SCO is
|
|||
|
||||
begin
|
||||
case T is
|
||||
when 'I' | 'E' | 'W' | 'a' =>
|
||||
when 'I' | 'E' | 'W' | 'a' | 'A' =>
|
||||
|
||||
-- For IF, EXIT, WHILE, or aspects, the token SLOC is that of
|
||||
-- the parent of the expression.
|
||||
|
||||
Loc := Sloc (Parent (N));
|
||||
|
||||
if T = 'a' then
|
||||
if T = 'a' or else T = 'A' then
|
||||
Nam := Chars (Identifier (Parent (N)));
|
||||
end if;
|
||||
|
||||
|
@ -1378,12 +1378,20 @@ package body Par_SCO is
|
|||
procedure Traverse_Aspects (N : Node_Id) is
|
||||
AN : Node_Id;
|
||||
AE : Node_Id;
|
||||
C1 : Character;
|
||||
|
||||
begin
|
||||
AN := First (Aspect_Specifications (N));
|
||||
while Present (AN) loop
|
||||
AE := Expression (AN);
|
||||
|
||||
-- SCOs are generated before semantic analysis/expansion:
|
||||
-- PPCs are not split yet.
|
||||
|
||||
pragma Assert (not Split_PPC (AN));
|
||||
|
||||
C1 := ASCII.NUL;
|
||||
|
||||
case Get_Aspect_Id (Chars (Identifier (AN))) is
|
||||
|
||||
-- Aspects rewritten into pragmas controlled by a Check_Policy:
|
||||
|
@ -1394,37 +1402,24 @@ package body Par_SCO is
|
|||
when Aspect_Pre |
|
||||
Aspect_Precondition |
|
||||
Aspect_Post |
|
||||
Aspect_Postcondition =>
|
||||
Aspect_Postcondition |
|
||||
Aspect_Invariant =>
|
||||
|
||||
-- SCOs are generated before semantic analysis/expansion:
|
||||
-- PPCs are not split yet.
|
||||
|
||||
pragma Assert (not Split_PPC (AN));
|
||||
|
||||
-- A Pre/Post aspect will be rewritten into a pragma
|
||||
-- Precondition/Postcondition with the same sloc.
|
||||
|
||||
pragma Assert (Current_Pragma_Sloc = No_Location);
|
||||
|
||||
Current_Pragma_Sloc := Sloc (AN);
|
||||
|
||||
-- Create the decision as potentially disabled aspect ('a').
|
||||
-- Set_SCO_Pragma_Enabled will subsequently switch to 'A'.
|
||||
|
||||
Process_Decisions_Defer (AE, 'a');
|
||||
Current_Pragma_Sloc := No_Location;
|
||||
C1 := 'a';
|
||||
|
||||
-- Aspects whose checks are generated in client units,
|
||||
-- regardless of whether or not the check is activated in the
|
||||
-- unit which contains the declaration.
|
||||
-- unit which contains the declaration: create decision as
|
||||
-- unconditionally enabled aspect (but still make a pragma
|
||||
-- entry since Set_SCO_Pragma_Enabled will be called when
|
||||
-- analyzing actual checks, possibly in other units).
|
||||
|
||||
when Aspect_Predicate |
|
||||
Aspect_Static_Predicate |
|
||||
Aspect_Dynamic_Predicate |
|
||||
Aspect_Invariant |
|
||||
Aspect_Type_Invariant =>
|
||||
|
||||
Process_Decisions_Defer (AE, 'A');
|
||||
C1 := 'A';
|
||||
|
||||
-- Other aspects: just process any decision nested in the
|
||||
-- aspect expression.
|
||||
|
@ -1432,11 +1427,23 @@ package body Par_SCO is
|
|||
when others =>
|
||||
|
||||
if Has_Decision (AE) then
|
||||
Process_Decisions_Defer (AE, 'X');
|
||||
C1 := 'X';
|
||||
end if;
|
||||
|
||||
end case;
|
||||
|
||||
if C1 /= ASCII.NUL then
|
||||
pragma Assert (Current_Pragma_Sloc = No_Location);
|
||||
|
||||
if C1 = 'a' or else C1 = 'A' then
|
||||
Current_Pragma_Sloc := Sloc (AN);
|
||||
end if;
|
||||
|
||||
Process_Decisions_Defer (AE, C1);
|
||||
|
||||
Current_Pragma_Sloc := No_Location;
|
||||
end if;
|
||||
|
||||
Next (AN);
|
||||
end loop;
|
||||
end Traverse_Aspects;
|
||||
|
|
|
@ -2233,6 +2233,18 @@ package body Sem_Prag is
|
|||
(Get_Pragma_Arg (Arg2), Standard_String);
|
||||
end if;
|
||||
|
||||
-- For a pragma in the extended main source unit, record enabled
|
||||
-- status in SCO.
|
||||
|
||||
-- This may seem redundant with the call to Check_Enabled occurring
|
||||
-- later on when the pragma is rewritten into a pragma Check but
|
||||
-- is actually required in the case of a postcondition within a
|
||||
-- generic.
|
||||
|
||||
if Check_Enabled (Pname) and then not Split_PPC (N) then
|
||||
Set_SCO_Pragma_Enabled (Loc);
|
||||
end if;
|
||||
|
||||
-- If we are within an inlined body, the legality of the pragma
|
||||
-- has been checked already.
|
||||
|
||||
|
@ -6995,6 +7007,21 @@ package body Sem_Prag is
|
|||
Opt.Check_Policy_List := N;
|
||||
end Assertion_Policy;
|
||||
|
||||
------------
|
||||
-- Assume --
|
||||
------------
|
||||
|
||||
-- pragma Assume (boolean_EXPRESSION);
|
||||
|
||||
when Pragma_Assume => Assume : declare
|
||||
begin
|
||||
GNAT_Pragma;
|
||||
S14_Pragma;
|
||||
Check_Arg_Count (1);
|
||||
|
||||
Analyze_And_Resolve (Expression (Arg1), Any_Boolean);
|
||||
end Assume;
|
||||
|
||||
------------------------------
|
||||
-- Assume_No_Invalid_Values --
|
||||
------------------------------
|
||||
|
@ -15668,6 +15695,7 @@ package body Sem_Prag is
|
|||
Pragma_Assert => -1,
|
||||
Pragma_Assert_And_Cut => -1,
|
||||
Pragma_Assertion_Policy => 0,
|
||||
Pragma_Assume => 0,
|
||||
Pragma_Assume_No_Invalid_Values => 0,
|
||||
Pragma_Attribute_Definition => +3,
|
||||
Pragma_Asynchronous => -1,
|
||||
|
|
|
@ -362,6 +362,7 @@ package Snames is
|
|||
Name_Ada_2012 : constant Name_Id := N + $; -- GNAT
|
||||
Name_Annotate : constant Name_Id := N + $; -- GNAT
|
||||
Name_Assertion_Policy : constant Name_Id := N + $; -- Ada 05
|
||||
Name_Assume : constant Name_Id := N + $; -- GNAT
|
||||
Name_Assume_No_Invalid_Values : constant Name_Id := N + $; -- GNAT
|
||||
Name_Attribute_Definition : constant Name_Id := N + $; -- GNAT
|
||||
Name_C_Pass_By_Copy : constant Name_Id := N + $; -- GNAT
|
||||
|
@ -1660,6 +1661,7 @@ package Snames is
|
|||
Pragma_Ada_2012,
|
||||
Pragma_Annotate,
|
||||
Pragma_Assertion_Policy,
|
||||
Pragma_Assume,
|
||||
Pragma_Assume_No_Invalid_Values,
|
||||
Pragma_Attribute_Definition,
|
||||
Pragma_C_Pass_By_Copy,
|
||||
|
|
Loading…
Add table
Reference in a new issue