+2016-04-19 Olivier Hainque <hainque@adacore.com>
+
+ * sem_util.adb (Build_Elaboration_Entity): Always request an
+ elab counter when preserving control-flow.
+
+2016-04-19 Olivier Hainque <hainque@adacore.com>
+
+ * sem_ch13.adb (Build_Invariant_Procedure_Declaration): Set
+ Needs_Debug_Info when producing SCOs.
+ * par_sco.adb (Traverse_Aspects): Fix categorization of
+ Type_Invariant to match actual processing as activated depending
+ on pragma Assertion_Policy.
+ * sem_prag.adb (Analyze_Pragma): Remove special case for
+ Name_Invariant regarding SCO generation, which completely disabled
+ the production of SCOs for Invariant pragmas and aspects.
+
2016-04-19 Hristian Kirtchev <kirtchev@adacore.com>
* checks.adb, sem_util.adb, sem_res.adb, sem_attr.adb: Minor
-- specification. The corresponding pragma will have the same
-- sloc.
- when Aspect_Pre |
- Aspect_Precondition |
- Aspect_Post |
- Aspect_Postcondition |
- Aspect_Invariant =>
+ when Aspect_Pre |
+ Aspect_Precondition |
+ Aspect_Post |
+ Aspect_Postcondition |
+ Aspect_Type_Invariant |
+ Aspect_Invariant =>
C1 := 'a';
when Aspect_Predicate |
Aspect_Static_Predicate |
- Aspect_Dynamic_Predicate |
- Aspect_Type_Invariant =>
+ Aspect_Dynamic_Predicate =>
C1 := 'A';
Sync_Def : Node_Id;
-- N's protected or task definition
- Vis_Decl : List_Id;
- -- Sync_Def's Visible_Declarations
+ Vis_Decl, Priv_Decl : List_Id;
+ -- Sync_Def's Visible_Declarations and Private_Declarations
begin
case Nkind (N) is
raise Program_Error;
end case;
- Vis_Decl := Visible_Declarations (Sync_Def);
+ -- Sync_Def may be Empty at least for empty Task_Type_Declarations.
+ -- Querying Visible or Private_Declarations is invalid in this case.
+
+ if Present (Sync_Def) then
+ Vis_Decl := Visible_Declarations (Sync_Def);
+ Priv_Decl := Private_Declarations (Sync_Def);
+ else
+ Vis_Decl := No_List;
+ Priv_Decl := No_List;
+ end if;
Dom_Info := Traverse_Declarations_Or_Statements
(L => Vis_Decl,
-- is dominated by the last visible declaration.
Traverse_Declarations_Or_Statements
- (L => Private_Declarations (Sync_Def),
+ (L => Priv_Decl,
D => Dom_Info);
end Traverse_Sync_Definition;
Set_Is_Invariant_Procedure (SId);
Set_Invariant_Procedure (Typ, SId);
+ -- Source Coverage Obligations might be attached to the invariant
+ -- expression this procedure evaluates, and we need debug info to be
+ -- able to assess the coverage achieved by evaluations.
+
+ if Opt.Generate_SCO then
+ Set_Needs_Debug_Info (SId);
+ end if;
+
-- Mark the invariant procedure explicitly as Ghost because it does not
-- come from source.
case Cname is
- -- Nothing to do for invariants and predicates as the checks
- -- occur in the client units. The SCO for the aspect in the
- -- declaration unit is conservatively always enabled.
+ -- Nothing to do for predicates as the checks occur in the
+ -- client units. The SCO for the aspect in the declaration
+ -- unit is conservatively always enabled.
- when Name_Invariant | Name_Predicate =>
+ when Name_Predicate =>
null;
-- Otherwise mark aspect/pragma SCO as enabled
elsif ASIS_Mode then
return;
- -- See if we need elaboration entity. We always need it for the dynamic
- -- elaboration model, since it is needed to properly generate the PE
- -- exception for access before elaboration.
+ -- See if we need elaboration entity.
+
+ -- We always need an elaboration entity when preserving control-flow, as
+ -- we want to remain explicit about the units elaboration order.
+
+ elsif Opt.Suppress_Control_Flow_Optimizations then
+ null;
+
+ -- We always need an elaboration entity for the dynamic elaboration
+ -- model, since it is needed to properly generate the PE exception for
+ -- access before elaboration.
elsif Dynamic_Elaboration_Checks then
null;