end if;
end if;
- -- Retain a copy of the pre- or postcondition pragma for formal
- -- verification purposes. The copy is needed because the pragma is
- -- expanded into other constructs which are not acceptable in the
- -- N_Contract node.
+ -- Retain copy of the pre/postcondition pragma in GNATprove mode.
+ -- The copy is needed because the pragma is expanded into other
+ -- constructs which are not acceptable in the N_Contract node.
if Acts_As_Spec (PO)
and then GNATprove_Mode
elsif Nkind (PO) = N_Compilation_Unit_Aux then
- -- In formal verification mode, analyze pragma expression for
- -- correctness, as it is not expanded later. Ditto in ASIS_Mode
- -- where there is no later point at which the aspect will be
- -- analyzed.
+ -- In GNATprove mode, analyze pragma expression for correctness,
+ -- as it is not expanded later. Ditto in ASIS_Mode where there is
+ -- no later point at which the aspect will be analyzed.
if GNATprove_Mode or ASIS_Mode then
Analyze_Pre_Post_Condition_In_Decl_Part
-- Start of processing for Process_Suppress_Unsuppress
begin
- -- Ignore pragma Suppress/Unsuppress in CodePeer and SPARK modes on
- -- user code: we want to generate checks for analysis purposes, as
+ -- Ignore pragma Suppress/Unsuppress in CodePeer and GNATprove modes
+ -- on user code: we want to generate checks for analysis purposes, as
-- set respectively by -gnatC and -gnatd.F
if (CodePeer_Mode or GNATprove_Mode)
Check_Restriction (No_Initialize_Scalars, N);
-- Initialize_Scalars creates false positives in CodePeer, and
- -- incorrect negative results in SPARK mode, so ignore this pragma
- -- in these modes.
+ -- incorrect negative results in GNATprove mode, so ignore this
+ -- pragma in these modes.
if not Restriction_Active (No_Initialize_Scalars)
and then not (CodePeer_Mode or GNATprove_Mode)
when Pragma_Inline_Always =>
GNAT_Pragma;
- -- Pragma always active unless in CodePeer or SPARK mode, since
- -- this causes walk order issues.
+ -- Pragma always active unless in CodePeer or GNATprove mode,
+ -- since this causes walk order issues.
if not (CodePeer_Mode or GNATprove_Mode) then
Process_Inline (Enabled);
Check_Valid_Configuration_Pragma;
-- Normalize_Scalars creates false positives in CodePeer, and
- -- incorrect negative results in SPARK mode, so ignore this pragma
- -- in these modes.
+ -- incorrect negative results in GNATprove mode, so ignore this
+ -- pragma in these modes.
if not (CodePeer_Mode or GNATprove_Mode) then
Normalize_Scalars := True;
-- pragma Validity_Checks (On | Off | ALL_CHECKS | STRING_LITERAL);
when Pragma_Validity_Checks => Validity_Checks : declare
- A : constant Node_Id := Get_Pragma_Arg (Arg1);
+ A : constant Node_Id := Get_Pragma_Arg (Arg1);
S : String_Id;
C : Char_Code;
Check_Arg_Count (1);
Check_No_Identifiers;
- if Nkind (A) = N_String_Literal then
- S := Strval (A);
+ -- Pragma always active unless in CodePeer or GNATprove modes,
+ -- which use a fixed configuration of validity checks.
- declare
- Slen : constant Natural := Natural (String_Length (S));
- Options : String (1 .. Slen);
- J : Natural;
+ if not (CodePeer_Mode or GNATprove_Mode) then
+ if Nkind (A) = N_String_Literal then
+ S := Strval (A);
- begin
- J := 1;
- loop
- C := Get_String_Char (S, Int (J));
- exit when not In_Character_Range (C);
- Options (J) := Get_Character (C);
+ declare
+ Slen : constant Natural := Natural (String_Length (S));
+ Options : String (1 .. Slen);
+ J : Natural;
- if J = Slen then
- Set_Validity_Check_Options (Options);
- exit;
- else
- J := J + 1;
- end if;
- end loop;
- end;
+ begin
+ -- Couldn't we use a for loop here over Options'Range???
- elsif Nkind (A) = N_Identifier then
- if Chars (A) = Name_All_Checks then
- Set_Validity_Check_Options ("a");
- elsif Chars (A) = Name_On then
- Validity_Checks_On := True;
- elsif Chars (A) = Name_Off then
- Validity_Checks_On := False;
+ J := 1;
+ loop
+ C := Get_String_Char (S, Int (J));
+
+ -- This is a weird test, it skips setting validity
+ -- checks entirely if any element of S is out of
+ -- range of Character, what is that about ???
+
+ exit when not In_Character_Range (C);
+ Options (J) := Get_Character (C);
+
+ if J = Slen then
+ Set_Validity_Check_Options (Options);
+ exit;
+ else
+ J := J + 1;
+ end if;
+ end loop;
+ end;
+
+ elsif Nkind (A) = N_Identifier then
+ if Chars (A) = Name_All_Checks then
+ Set_Validity_Check_Options ("a");
+ elsif Chars (A) = Name_On then
+ Validity_Checks_On := True;
+ elsif Chars (A) = Name_Off then
+ Validity_Checks_On := False;
+ end if;
end if;
end if;
end Validity_Checks;
and then not Has_Null_State
then
Error_Msg_NE
- ("useless refinement, subprogram & does not depends on abstract "
+ ("useless refinement, subprogram & does not depend on abstract "
& "state with visible refinement", N, Spec_Id);
return;
end if;
projects / platform / upstream / gcc.git / commitdiff