+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.
-- 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;
when Pragma_Abort_Defer |
Pragma_Assertion_Policy |
+ Pragma_Assume |
Pragma_Assume_No_Invalid_Values |
Pragma_AST_Entry |
Pragma_All_Calls_Remote |
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;
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:
when Aspect_Pre |
Aspect_Precondition |
Aspect_Post |
- Aspect_Postcondition =>
-
- -- SCOs are generated before semantic analysis/expansion:
- -- PPCs are not split yet.
-
- pragma Assert (not Split_PPC (AN));
+ Aspect_Postcondition |
+ Aspect_Invariant =>
- -- 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.
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;
(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.
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 --
------------------------------
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,
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
Pragma_Ada_2012,
Pragma_Annotate,
Pragma_Assertion_Policy,
+ Pragma_Assume,
Pragma_Assume_No_Invalid_Values,
Pragma_Attribute_Definition,
Pragma_C_Pass_By_Copy,
projects / platform / upstream / linaro-gcc.git / commitdiff