OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

2014-01-20 Yannick Moy <moy@adacore.com> 

* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
	* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
	* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
	* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
	GNATprove_Mode.
	* sem_ch13.adb: Remove blank.
	* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
	subprograms by alias for renamings, not for inherited primitive
	operations.
	* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
	in GNATprove mode.
	(Remove_Side_Effects): Apply the removal in
	GNATprove mode, for the full analysis of expressions.
	* expander.adb (Expand): Call the light SPARK expansion in GNATprove
	mode.
	(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
	save/restore actions for Expander_Active flag in GNATprove mode,
	similar to what is done in ASIS mode.
	* frontend.adb (Frontend): Generic bodies are instantiated in
	GNATprove mode.
	* gnat1drv.adb (Adjust_Global_Switches): Set operating
	mode to Check_Semantics in GNATprove mode, although a light
	expansion is still performed.
	(Gnat1drv): Set Back_End_Mode to
	Declarations_Only in GNATprove mode, and later on special case
	the GNATprove mode to continue analysis anyway.
	* lib-writ.adb (Write_ALI): Always generate ALI files in
	GNATprove mode.
	* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
	Expander_Active.
	(SPARK_Mode): Renamed as GNATprove_Mode.
	* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
	tree in GNATprove_Mode.
	* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
	body in GNATprove mode.
	(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
	mode.
	* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
	Make sure side effects are removed in GNATprove mode.

From-SVN: r206805
This commit is contained in:
Yannick Moy 2014-01-20 13:44:07 +00:00 committed by Arnaud Charlet
parent 69675d50f6
commit f5da7a97f5
31 changed files with 207 additions and 168 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
gcc/ada/ChangeLog
View File

@ -1,3 +1,45 @@
2014-01-20 Yannick Moy <moy@adacore.com>
* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
GNATprove_Mode.
* sem_ch13.adb: Remove blank.
* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
subprograms by alias for renamings, not for inherited primitive
operations.
* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
in GNATprove mode.
(Remove_Side_Effects): Apply the removal in
GNATprove mode, for the full analysis of expressions.
* expander.adb (Expand): Call the light SPARK expansion in GNATprove
mode.
(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
save/restore actions for Expander_Active flag in GNATprove mode,
similar to what is done in ASIS mode.
* frontend.adb (Frontend): Generic bodies are instantiated in
GNATprove mode.
* gnat1drv.adb (Adjust_Global_Switches): Set operating
mode to Check_Semantics in GNATprove mode, although a light
expansion is still performed.
(Gnat1drv): Set Back_End_Mode to
Declarations_Only in GNATprove mode, and later on special case
the GNATprove mode to continue analysis anyway.
* lib-writ.adb (Write_ALI): Always generate ALI files in
GNATprove mode.
* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
Expander_Active.
(SPARK_Mode): Renamed as GNATprove_Mode.
* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
tree in GNATprove_Mode.
* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
body in GNATprove mode.
(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
mode.
* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
Make sure side effects are removed in GNATprove mode.
2014-01-20 Eric Botcazou <ebotcazou@adacore.com>
* gcc-interface/decl.c (gnat_to_gnu_entity) <object>: Robustify tests

10
gcc/ada/adabkend.adb
View File

@ -235,12 +235,12 @@ package body Adabkend is
if Is_Switch (Argv) then
Fail ("Object file name missing after -gnatO");
-- In SPARK_Mode, such an object file is never written, and the
-- call to Set_Output_Object_File_Name may fail (e.g. when the
-- object file name does not have the expected suffix). So we
-- skip that call when SPARK_Mode is set.
-- In GNATprove_Mode, such an object file is never written, and
-- the call to Set_Output_Object_File_Name may fail (e.g. when
-- the object file name does not have the expected suffix). So
-- we skip that call when GNATprove_Mode is set.
elsif SPARK_Mode then
elsif GNATprove_Mode then
Output_File_Name_Seen := True;
else

6
gcc/ada/ali-util.adb
View File

@ -274,11 +274,11 @@ package body ALI.Util is
Error_Msg ("{ had errors, must be fixed, and recompiled");
Set_Name_Table_Info (Afile, Int (No_Unit_Id));
-- In formal verification mode, object files are never
-- generated, so No_Object=True is not considered an error.
-- In GNATprove mode, object files are never generated, so
-- No_Object=True is not considered an error.
elsif ALIs.Table (Idread).No_Object
and then not SPARK_Mode
and then not GNATprove_Mode
and then not Ignore_Errors
then
Error_Msg_File_1 := Withs.Table (W).Sfile;

4
gcc/ada/errout.adb
View File

@ -239,7 +239,7 @@ package body Errout is
-- an error status. These errors are handled in the driver of the
-- verification process instead.
elsif SPARK_Mode and not Frame_Condition_Mode then
elsif GNATprove_Mode and not Frame_Condition_Mode then
return False;
else
@ -2970,7 +2970,7 @@ package body Errout is
-- Suppress "size too small" errors in CodePeer mode and SPARK mode,
-- since pragma Pack is also ignored in these configurations.
if CodePeer_Mode or SPARK_Mode then
if CodePeer_Mode or GNATprove_Mode then
return True;
-- When a size is wrong for a frozen type there is no explicit size

8
gcc/ada/exp_ch7.adb
View File

@ -937,7 +937,7 @@ package body Exp_Ch7 is
-- Do not create finalization masters in SPARK mode because they result
-- in unwanted expansion.
elsif SPARK_Mode then
elsif GNATprove_Mode then
return;
end if;
@ -2813,7 +2813,7 @@ package body Exp_Ch7 is
-- Do not perform this expansion in SPARK mode because it is not
-- necessary.
if SPARK_Mode then
if GNATprove_Mode then
return;
end if;
@ -2975,7 +2975,7 @@ package body Exp_Ch7 is
-- Do not perform this expansion in SPARK mode because we do not create
-- finalizers in the first place.
if SPARK_Mode then
if GNATprove_Mode then
return;
end if;
@ -3658,7 +3658,7 @@ package body Exp_Ch7 is
-- this node and enclosed expression are not expanded, so do not apply
-- any transformations here.
elsif SPARK_Mode
elsif GNATprove_Mode
and then Nkind (Wrap_Node) = N_Pragma
and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
then

2
gcc/ada/exp_dbug.adb
View File

@ -1314,7 +1314,7 @@ package body Exp_Dbug is
-- name as being qualified, as Qualify_Entity_Name may be called more
-- than once on the same entity.
elsif SPARK_Mode then
elsif GNATprove_Mode then
if Has_Homonym (Ent) then
Get_Name_String (Chars (Ent));
Append_Homonym_Number (Ent);

62
gcc/ada/exp_spark.adb
View File

@ -31,7 +31,6 @@ with Sem_Aux; use Sem_Aux;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Stand; use Stand;
package body Exp_SPARK is
@ -94,51 +93,28 @@ package body Exp_SPARK is
-----------------------
procedure Expand_SPARK_Call (N : Node_Id) is
Call_Node : constant Node_Id := N;
Parent_Subp : Entity_Id;
begin
-- Ignore if previous error
if Nkind (Call_Node) in N_Has_Etype
and then Etype (Call_Node) = Any_Type
then
return;
end if;
-- Call using access to subprogram with explicit dereference
if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
Parent_Subp := Empty;
-- Case of call to simple entry, where the Name is a selected component
-- whose prefix is the task, and whose selector name is the entry name
elsif Nkind (Name (Call_Node)) = N_Selected_Component then
Parent_Subp := Empty;
-- Case of call to member of entry family, where Name is an indexed
-- component, with the prefix being a selected component giving the
-- task and entry family name, and the index being the entry index.
elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
Parent_Subp := Empty;
-- Normal case
else
Parent_Subp := Alias (Entity (Name (Call_Node)));
end if;
-- If the subprogram is a renaming, replace it in the call with the name
-- of the actual subprogram being called.
-- of the actual subprogram being called. We distinguish renamings from
-- inherited primitive operations, which both have an Alias component,
-- by looking at the parent node of the entity. The entity for a
-- renaming has the function or procedure specification node as
-- parent, while an inherited primitive operation has the derived
-- type declaration as parent.
if Present (Parent_Subp) then
Parent_Subp := Ultimate_Alias (Parent_Subp);
-- The below setting of Entity is suspect, see F109-018 discussion???
Set_Entity (Name (Call_Node), Parent_Subp);
if Nkind (Name (N)) in N_Has_Entity
and then Present (Entity (Name (N)))
then
declare
E : constant Entity_Id := Entity (Name (N));
begin
if Nkind_In (Parent (E), N_Function_Specification,
N_Procedure_Specification)
and then Present (Alias (E))
then
Set_Entity (Name (N), Ultimate_Alias (E));
end if;
end;
end if;
end Expand_SPARK_Call;

7
gcc/ada/exp_spark.ads
View File

@ -23,10 +23,9 @@
-- --
------------------------------------------------------------------------------
-- This package implements a light expansion which is used in formal
-- verification mode (SPARK_Mode = True). Instead of a complete expansion
-- of nodes for code generation, this SPARK expansion targets generation
-- of intermediate code for formal verification.
-- This package implements a light expansion which is used in GNATprove mode.
-- Instead of a complete expansion of nodes for code generation, this light
-- expansion targets generation of intermediate code for formal verification.
-- Expand_SPARK is called directly by Expander.Expand.

24
gcc/ada/exp_util.adb
View File

@ -2034,12 +2034,22 @@ package body Exp_Util is
-- may be constants that depend on the bounds of a string literal, both
-- standard string types and more generally arrays of characters.
if not Expander_Active
-- In GNATprove mode, we also need the more precise subtype to be set.
if not (Expander_Active or GNATprove_Mode)
and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
then
return;
end if;
-- In GNATprove mode, Unc_Type might not be complete when analyzing
-- a generic unit. As generic units are not analyzed directly in
-- GNATprove, return here rather than failing later.
if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then
return;
end if;
if Nkind (Exp) = N_Slice then
declare
Slice_Type : constant Entity_Id := Etype (First_Index (Exp_Typ));
@ -6862,9 +6872,11 @@ package body Exp_Util is
-- Start of processing for Remove_Side_Effects
begin
-- Handle cases in which there is nothing to do
-- Handle cases in which there is nothing to do. In GNATprove mode,
-- removal of side effects is useful for the light expansion of
-- renamings.
if not Expander_Active then
if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
return;
end if;
@ -7074,7 +7086,7 @@ package body Exp_Util is
-- free if the resulting value is captured by a variable or a
-- constant.
if SPARK_Mode
if GNATprove_Mode
and then Nkind (Parent (Exp)) = N_Object_Declaration
then
goto Leave;
@ -7119,7 +7131,7 @@ package body Exp_Util is
-- types, use a different approach which ignores the secondary stack
-- and "copies" the returned object.
if SPARK_Mode then
if GNATprove_Mode then
Res := New_Reference_To (Def_Id, Loc);
Ref_Type := Exp_Type;
@ -7156,7 +7168,7 @@ package body Exp_Util is
-- Do not generate a 'reference in SPARK mode since the access
-- type is not created in the first place.
if SPARK_Mode then
if GNATprove_Mode then
New_Exp := E;
-- Otherwise generate reference, marking the value as non-null

26
gcc/ada/expander.adb
View File

@ -88,8 +88,9 @@ package body Expander is
-- The first is when are not generating code. In this mode the
-- Full_Analysis flag indicates whether we are performing a complete
-- analysis, in which case Full_Analysis = True or a pre-analysis in
-- which case Full_Analysis = False. See the spec of Sem for more
-- info on this.
-- which case Full_Analysis = False. See the spec of Sem for more info
-- on this. Additionally, the GNATprove_Mode flag indicates that a light
-- expansion for formal verification should be used.
--
-- The second reason for the Expander_Active flag to be False is that
-- we are performing a pre-analysis. During pre-analysis all expansion
@ -107,7 +108,7 @@ package body Expander is
-- given that the expansion actions that would normally process it will
-- not take place. This prevents cascaded errors due to stack mismatch.
if not Expander_Active then
if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
Set_Analyzed (N, Full_Analysis);
if Serious_Errors_Detected > 0
@ -127,10 +128,11 @@ package body Expander is
Debug_A_Entry ("expanding ", N);
begin
-- In SPARK mode we only need a very limited subset of the usual
-- expansions. This limited subset is implemented in Expand_SPARK.
-- In GNATprove mode we only need a very limited subset of
-- the usual expansions. This limited subset is implemented
-- in Expand_SPARK.
if SPARK_Mode then
if GNATprove_Mode then
Expand_SPARK (N);
-- Here for normal non-SPARK mode
@ -503,10 +505,10 @@ package body Expander is
procedure Expander_Mode_Restore is
begin
-- Not active (has no effect) in ASIS mode (see comments in spec of
-- Expander_Mode_Save_And_Set).
-- Not active (has no effect) in ASIS and GNATprove modes (see comments
-- in spec of Expander_Mode_Save_And_Set).
if ASIS_Mode then
if ASIS_Mode or GNATprove_Mode then
return;
end if;
@ -530,10 +532,10 @@ package body Expander is
procedure Expander_Mode_Save_And_Set (Status : Boolean) is
begin
-- Not active (has no effect) in ASIS mode (see comments in spec of
-- Expander_Mode_Save_And_Set).
-- Not active (has no effect) in ASIS and GNATprove modes (see comments
-- in spec of Expander_Mode_Save_And_Set).
if ASIS_Mode then
if ASIS_Mode or GNATprove_Mode then
return;
end if;

22
gcc/ada/expander.ads
View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2008, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -150,18 +150,20 @@ package Expander is
-- Saves the current setting of the Expander_Active flag on an internal
-- stack and then sets the flag to the given value.
--
-- Note: this routine has no effect in ASIS_Mode. In ASIS_Mode, all
-- expansion activity is always off, since we want the original semantic
-- tree for ASIS purposes without any expansion. This is achieved by
-- setting Expander_Active False in ASIS_Mode. In situations such as
-- the call to Instantiate_Bodies in Frontend, Expander_Mode_Save_And_Set
-- may be called to temporarily turn the expander on, but this will have
-- no effect in ASIS mode.
-- Note: this routine has no effect in ASIS and GNATprove modes. In ASIS
-- mode, all expansion activity is always off, since we want the original
-- semantic tree for ASIS purposes without any expansion. In GNATprove
-- mode, a very light expansion is performed on specific nodes. Both are
-- achieved by setting Expander_Active False in ASIS and GNATprove modes.
-- In situations such as the call to Instantiate_Bodies in Frontend,
-- Expander_Mode_Save_And_Set may be called to temporarily turn the
-- expander on, but this will have no effect in ASIS and GNATprove modes.
procedure Expander_Mode_Restore;
-- Restores the setting of the Expander_Active flag using the top entry
-- pushed onto the stack by Expander_Mode_Save_And_Reset, popping the
-- stack, except that if any errors have been detected, then the state
-- of the flag is left set to False. Disabled for ASIS_Mode (see above).
-- stack, except that if any errors have been detected, then the state of
-- the flag is left set to False. Disabled for ASIS and GNATprove modes
-- (see above).
end Expander;

4
gcc/ada/freeze.adb
View File

@ -3280,7 +3280,7 @@ package body Freeze is
-- general, neither CodePeer not GNATprove care about the
-- internal representation of objects.
and then not (CodePeer_Mode or SPARK_Mode)
and then not (CodePeer_Mode or GNATprove_Mode)
then
-- If implicit packing enabled, do it
@ -4230,7 +4230,7 @@ package body Freeze is
and then not Is_Limited_Composite (E)
and then not Is_Packed (Root_Type (E))
and then not Has_Component_Size_Clause (Root_Type (E))
and then not (CodePeer_Mode or SPARK_Mode)
and then not (CodePeer_Mode or GNATprove_Mode)
then
-- Compute number of elements in array

2
gcc/ada/frontend.adb
View File

@ -362,7 +362,7 @@ begin
if Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode)
and then (ASIS_Mode or GNATprove_Mode))
then
Instantiate_Bodies;
end if;

37
gcc/ada/gnat1drv.adb
View File

@ -299,15 +299,16 @@ procedure Gnat1drv is
Formal_Extensions := True;
end if;
-- Enable SPARK_Mode when using -gnatd.F switch
-- Enable GNATprove_Mode when using -gnatd.F switch
if Debug_Flag_Dot_FF then
SPARK_Mode := True;
GNATprove_Mode := True;
end if;
-- SPARK_Mode is also activated by default in the gnat2why executable
-- GNATprove_Mode is also activated by default in the gnat2why
-- executable.
if SPARK_Mode then
if GNATprove_Mode then
-- Set strict standard interpretation of compiler permissions
@ -384,11 +385,10 @@ procedure Gnat1drv is
Polling_Required := False;
-- Set operating mode to Generate_Code, but full front-end expansion
-- is not desirable in SPARK mode, so a light expansion is performed
-- instead.
-- Set operating mode to Check_Semantics, but a light front-end
-- expansion is still performed.
Operating_Mode := Generate_Code;
Operating_Mode := Check_Semantics;
-- Skip call to gigi
@ -1054,17 +1054,13 @@ begin
elsif CodePeer_Mode then
Back_End_Mode := Generate_Object;
-- It is not an error to analyze in SPARK mode a spec which requires a
-- body, when the body is not available. During frame condition
-- It is not an error to analyze in GNATprove mode a spec which requires
-- a body, when the body is not available. During frame condition
-- generation, the corresponding ALI file is generated. During
-- translation to Why, Why code is generated for the spec.
elsif SPARK_Mode then
if Frame_Condition_Mode then
Back_End_Mode := Declarations_Only;
else
Back_End_Mode := Generate_Object;
end if;
elsif GNATprove_Mode then
Back_End_Mode := Declarations_Only;
-- In all other cases (specs which have bodies, generics, and bodies
-- where subunits are missing), we cannot generate code and we generate
@ -1168,10 +1164,11 @@ begin
-- since representations are largely symbolic there.
if Back_End_Mode = Declarations_Only
and then (not (Back_Annotate_Rep_Info or Generate_SCIL)
or else Main_Kind = N_Subunit
or else Targparm.Frontend_Layout_On_Target
or else Targparm.VM_Target /= No_VM)
and then
(not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
or else Main_Kind = N_Subunit
or else Targparm.Frontend_Layout_On_Target
or else Targparm.VM_Target /= No_VM)
then
Sem_Ch13.Validate_Unchecked_Conversions;
Sem_Ch13.Validate_Address_Clauses;

9
gcc/ada/lib-writ.adb
View File

@ -841,7 +841,7 @@ package body Lib.Writ is
-- files, which are required to compute frame conditions
-- of subprograms.
or else SPARK_Mode
or else GNATprove_Mode
then
Write_Info_Tab (25);
@ -973,9 +973,10 @@ package body Lib.Writ is
-- If we are not generating code, and there is an up to date ALI file
-- file accessible, read it, and acquire the compilation arguments from
-- this file.
-- this file. In GNATprove mode, always generate the ALI file, which
-- contains a special section for formal verification.
if Operating_Mode /= Generate_Code then
if Operating_Mode /= Generate_Code and then not GNATprove_Mode then
if Up_To_Date_ALI_File_Exists then
Update_Tables_From_ALI_File;
return;
@ -1488,7 +1489,7 @@ package body Lib.Writ is
-- Output SPARK cross-reference information if needed
if Opt.Xref_Active and then SPARK_Mode then
if Opt.Xref_Active and then GNATprove_Mode then
SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
Num_Sdep => Num_Sdep);
SPARK_Specific.Output_SPARK_Xrefs;

8
gcc/ada/lib-xref.adb
View File

@ -644,7 +644,7 @@ package body Lib.Xref is
-- in SPARK mode when the related context comes from an instance.
or else
(SPARK_Mode
(GNATprove_Mode
and then In_Extended_Main_Code_Unit (N)
and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
then
@ -899,7 +899,7 @@ package body Lib.Xref is
and then
(Instantiation_Location (Sloc (N)) = No_Location
or else Typ = 'i'
or else SPARK_Mode)
or else GNATprove_Mode)
-- Ignore dummy references
@ -986,7 +986,7 @@ package body Lib.Xref is
-- the renaming, which is needed to compute a valid set of effects
-- (reads, writes) for the enclosing subprogram.
if SPARK_Mode then
if GNATprove_Mode then
Ent := Get_Through_Renamings (Ent);
-- If no enclosing object, then it could be a reference to any
@ -1015,7 +1015,7 @@ package body Lib.Xref is
Actual_Typ := 'P';
end if;
if SPARK_Mode then
if GNATprove_Mode then
Ref := Sloc (Nod);
Def := Sloc (Ent);

2
gcc/ada/opt.adb
View File

@ -44,7 +44,7 @@ package body Opt is
function Full_Expander_Active return Boolean is
begin
return Expander_Active and not SPARK_Mode;
return Expander_Active;
end Full_Expander_Active;
----------------------------------

4
gcc/ada/opt.ads
View File

@ -1996,7 +1996,7 @@ package Opt is
-----------------------------------
Frame_Condition_Mode : Boolean := False;
-- Specific mode to be used in combination with SPARK_Mode. If set to
-- Specific mode to be used in combination with GNATprove_Mode. If set to
-- true, ALI files containing the frame conditions (global effects) are
-- generated, and Why files are *not* generated. If not true, Why files
-- are generated. Set by debug flag -gnatd.G.
@ -2010,7 +2010,7 @@ package Opt is
-- The mode applicable to the whole compilation. The global mode can be set
-- in a configuration file such as gnat.adc.
SPARK_Mode : Boolean := False;
GNATprove_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through the
-- generation of Why code for those parts of the input code that belong to
-- the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by

2
gcc/ada/restrict.adb
View File

@ -538,7 +538,7 @@ package body Restrict is
-- set in gnat1drv.adb so that we have consistency between each
-- compilation.
if CodePeer_Mode or SPARK_Mode then
if CodePeer_Mode or GNATprove_Mode then
return;
end if;

14
gcc/ada/sem_aggr.adb
View File

@ -454,10 +454,14 @@ package body Sem_Aggr is
Check_Unset_Reference (Exp);
end if;
-- This is really expansion activity, so make sure that expansion
-- is on and is allowed.
-- This is really expansion activity, so make sure that expansion is
-- on and is allowed. In GNATprove mode, we also want check flags to be
-- added in the tree, so that the formal verification can rely on those
-- to be present.
if not Expander_Active or else In_Spec_Expression then
if not (Expander_Active or GNATprove_Mode)
or In_Spec_Expression
then
return;
end if;
@ -996,10 +1000,10 @@ package body Sem_Aggr is
-- frozen so that initialization procedures can properly be called
-- in the resolution that follows. The replacement of boxes with
-- initialization calls is properly an expansion activity but it must
-- be done during revolution.
-- be done during resolution.
if Expander_Active
and then Present (Component_Associations (N))
and then Present (Component_Associations (N))
then
declare
Comp : Node_Id;

2
gcc/ada/sem_attr.adb
View File

@ -4499,7 +4499,7 @@ package body Sem_Attr is
-- not suffer from the out-of-order issue described above. Thus, this
-- expansion is skipped in SPARK mode.
if not Is_Entity_Name (P) and then not SPARK_Mode then
if not Is_Entity_Name (P) and then not GNATprove_Mode then
P_Type := Base_Type (P_Type);
Set_Etype (N, P_Type);
Set_Etype (P, P_Type);

13
gcc/ada/sem_ch12.adb
View File

@ -3616,7 +3616,7 @@ package body Sem_Ch12 is
-- We instantiate the body if we are generating code, if we are
-- generating cross-reference information, or if we are building
-- trees for ASIS use.
-- trees for ASIS use or GNATprove use.
declare
Enclosing_Body_Present : Boolean := False;
@ -3724,7 +3724,7 @@ package body Sem_Ch12 is
and then not Inline_Now
and then (Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode));
and then (ASIS_Mode or GNATprove_Mode)));
-- If front_end_inlining is enabled, do not instantiate body if
-- within a generic context.
@ -4390,17 +4390,18 @@ package body Sem_Ch12 is
or else Is_Inlined (Subp)
or else Is_Inlined (Alias (Subp)))
-- Must be generating code or analyzing code in ASIS mode
-- Must be generating code or analyzing code in ASIS mode or GNATprove
-- mode.
and then (Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode))
and then (ASIS_Mode or GNATprove_Mode)))
-- The body is needed when generating code (full expansion), in ASIS
-- mode for other tools, and in SPARK mode (special expansion) for
-- mode for other tools, and in GNATprove mode (special expansion) for
-- formal verification of the body itself.
and then (Expander_Active or ASIS_Mode)
and then (Expander_Active or ASIS_Mode or GNATprove_Mode)
-- No point in inlining if ABE is inevitable

2
gcc/ada/sem_ch13.adb
View File

@ -2718,7 +2718,7 @@ package body Sem_Ch13 is
Prepend (Aitem,
Visible_Declarations (Specification (N)));
elsif Nkind (N) = N_Package_Instantiation then
elsif Nkind (N) = N_Package_Instantiation then
declare
Spec : constant Node_Id :=
Specification (Instance_Spec (N));

20
gcc/ada/sem_ch3.adb
View File

@ -10084,7 +10084,7 @@ package body Sem_Ch3 is
-- SPARK mode. Since this is legal code with respect to theorem
-- proving, do not emit the error.
if SPARK_Mode
if GNATprove_Mode
and then Nkind (Exp) = N_Function_Call
and then Nkind (Parent (Exp)) = N_Object_Declaration
and then not Comes_From_Source
@ -12223,12 +12223,12 @@ package body Sem_Ch3 is
-- needed, since checks may cause duplication of the expressions
-- which must not be reevaluated.
-- The forced evaluation removes side effects from expressions,
-- which should occur also in SPARK mode. Otherwise, we end up with
-- The forced evaluation removes side effects from expressions, which
-- should occur also in GNATprove mode. Otherwise, we end up with
-- unexpected insertions of actions at places where this is not
-- supposed to occur, e.g. on default parameters of a call.
if Expander_Active then
if Expander_Active or GNATprove_Mode then
Force_Evaluation (Low_Bound (R));
Force_Evaluation (High_Bound (R));
end if;
@ -18865,11 +18865,11 @@ package body Sem_Ch3 is
-- duplication of the expression without forcing evaluation.
-- The forced evaluation removes side effects from expressions,
-- which should occur also in SPARK mode. Otherwise, we end up
-- which should occur also in GNATprove mode. Otherwise, we end up
-- with unexpected insertions of actions at places where this is
-- not supposed to occur, e.g. on default parameters of a call.
if Expander_Active then
if Expander_Active or GNATprove_Mode then
Force_Evaluation (Lo);
Force_Evaluation (Hi);
end if;
@ -18980,11 +18980,11 @@ package body Sem_Ch3 is
-- Case of other than an explicit N_Range node
-- The forced evaluation removes side effects from expressions, which
-- should occur also in SPARK mode. Otherwise, we end up with unexpected
-- insertions of actions at places where this is not supposed to occur,
-- e.g. on default parameters of a call.
-- should occur also in GNATprove mode. Otherwise, we end up with
-- unexpected insertions of actions at places where this is not
-- supposed to occur, e.g. on default parameters of a call.
elsif Expander_Active then
elsif Expander_Active or GNATprove_Mode then
Get_Index_Bounds (R, Lo, Hi);
Force_Evaluation (Lo);
Force_Evaluation (Hi);

4
gcc/ada/sem_ch4.adb
View File

@ -1823,7 +1823,7 @@ package body Sem_Ch4 is
-- In formal verification mode, keep track of all reads and writes
-- through explicit dereferences.
if SPARK_Mode then
if GNATprove_Mode then
SPARK_Specific.Generate_Dereference (N);
end if;
@ -4613,7 +4613,7 @@ package body Sem_Ch4 is
-- In SPARK mode, this is made into an error to simplify
-- the processing of the formal verification backend.
if SPARK_Mode then
if GNATprove_Mode then
Apply_Compile_Time_Constraint_Error
(N, "component not present in }",
CE_Discriminant_Check_Failed,

2
gcc/ada/sem_ch5.adb
View File

@ -1712,7 +1712,7 @@ package body Sem_Ch5 is
-- Do not perform this expansion in SPARK mode, since the formal
-- verification directly deals with the source form of the iterator.
and then not SPARK_Mode
and then not GNATprove_Mode
then
declare
Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);

4
gcc/ada/sem_ch6.adb
View File

@ -1151,7 +1151,7 @@ package body Sem_Ch6 is
-- prepares the contract assertions for generic subprograms or for
-- ASIS. Do not generate contract checks in SPARK mode.
if not SPARK_Mode then
if not GNATprove_Mode then
Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
end if;
@ -3188,7 +3188,7 @@ package body Sem_Ch6 is
-- prepares the contract assertions for generic subprograms or for ASIS.
-- Do not generate contract checks in SPARK mode.
if not SPARK_Mode then
if not GNATprove_Mode then
Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
end if;

2
gcc/ada/sem_ch8.adb
View File

@ -5079,7 +5079,7 @@ package body Sem_Ch8 is
if Is_Object (E)
and then Present (Renamed_Object (E))
and then not SPARK_Mode
and then not GNATprove_Mode
then
Generate_Reference (E, N);

16
gcc/ada/sem_prag.adb
View File

@ -4556,7 +4556,7 @@ package body Sem_Prag is
-- N_Contract node.
if Acts_As_Spec (PO)
and then (SPARK_Mode or Formal_Extensions)
and then (GNATprove_Mode or Formal_Extensions)
then
declare
Prag : constant Node_Id := New_Copy_Tree (N);
@ -4596,7 +4596,7 @@ package body Sem_Prag is
-- where there is no later point at which the aspect will be
-- analyzed.
if SPARK_Mode or else ASIS_Mode then
if GNATprove_Mode or else ASIS_Mode then
Analyze_Pre_Post_Condition_In_Decl_Part
(N, Defining_Entity (Unit (Parent (PO))));
end if;
@ -8345,7 +8345,9 @@ package body Sem_Prag is
-- user code: we want to generate checks for analysis purposes, as
-- set respectively by -gnatC and -gnatd.F
if (CodePeer_Mode or SPARK_Mode) and then Comes_From_Source (N) then
if (CodePeer_Mode or GNATprove_Mode)
and then Comes_From_Source (N)
then
return;
end if;
@ -13700,7 +13702,7 @@ package body Sem_Prag is
-- in these modes.
if not Restriction_Active (No_Initialize_Scalars)
and then not (CodePeer_Mode or SPARK_Mode)
and then not (CodePeer_Mode or GNATprove_Mode)
then
Init_Or_Norm_Scalars := True;
Initialize_Scalars := True;
@ -13819,7 +13821,7 @@ package body Sem_Prag is
-- Pragma always active unless in CodePeer or SPARK mode, since
-- this causes walk order issues.
if not (CodePeer_Mode or SPARK_Mode) then
if not (CodePeer_Mode or GNATprove_Mode) then
Process_Inline (Enabled);
end if;
@ -15460,7 +15462,7 @@ package body Sem_Prag is
-- incorrect negative results in SPARK mode, so ignore this pragma
-- in these modes.
if not (CodePeer_Mode or SPARK_Mode) then
if not (CodePeer_Mode or GNATprove_Mode) then
Normalize_Scalars := True;
Init_Or_Norm_Scalars := True;
end if;
@ -15921,7 +15923,7 @@ package body Sem_Prag is
-- complex front-end expansions related to pragma Pack,
-- so disable handling of pragma Pack in these cases.
if CodePeer_Mode or SPARK_Mode then
if CodePeer_Mode or GNATprove_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly

4
gcc/ada/sem_res.adb
View File

@ -1693,7 +1693,7 @@ package body Sem_Res is
-- case of Ada 2012 constructs such as quantified expressions, which are
-- expanded in two separate steps.
if SPARK_Mode then
if GNATprove_Mode then
Analyze_And_Resolve (N, T);
else
Analyze_And_Resolve (N, T, Suppress => All_Checks);
@ -4206,7 +4206,7 @@ package body Sem_Res is
-- in scope at the point of reference, so the reference should
-- be ignored for computing effects of subprograms.
and then not SPARK_Mode
and then not GNATprove_Mode
then
Set_Entity (Selector_Name (Parent (A)), F);
Generate_Reference (F, Selector_Name (Parent (A)));

11
gcc/ada/sem_util.adb
View File

@ -12802,7 +12802,7 @@ package body Sem_Util is
-- In formal verification mode, keep track of all reads and
-- writes through explicit dereferences.
if SPARK_Mode then
if GNATprove_Mode then
SPARK_Specific.Generate_Dereference (N, 'm');
end if;
@ -12897,11 +12897,12 @@ package body Sem_Util is
-- Generate a reference only if the assignment comes from
-- source. This excludes, for example, calls to a dispatching
-- assignment operation when the left-hand side is tagged.
-- assignment operation when the left-hand side is tagged. In
-- GNATprove mode, we need those references also on generated
-- code, as these are used to compute the local effects of
-- subprograms.
-- Why is SPARK mode different here ???
if Modification_Comes_From_Source or SPARK_Mode then
if Modification_Comes_From_Source or GNATprove_Mode then
Generate_Reference (Ent, Exp, 'm');
-- If the target of the assignment is the bound variable