+2011-08-29 Yannick Moy <moy@adacore.com>
+
+ * sem_prag.adb (Check_Precondition_Postcondition): In formal
+ verification mode, analyze pragma expression for correctness, for
+ pre/post on library-level subprogram, as it is not expanded later.
+
+2011-08-29 Yannick Moy <moy@adacore.com>
+
+ * exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates
+ in formal verification.
+
+2011-08-29 Thomas Quinot <quinot@adacore.com>
+
+ * sem_util.adb: Minor reformatting.
+ * freeze.adb, sem_ch13.adb: Fix comment: Bit_Order is an attribute,
+ there's no pragma.
+ * par_sco.ads, par_sco.adb: Update comments.
+
+2011-08-29 Yannick Moy <moy@adacore.com>
+
+ * einfo.adb, einfo.ads: Remove flag Is_Postcondition_Proc and
+ associated getter/setter.
+ * sem_ch6.adb: Remove reference to Is_Postcondition_Proc.
+
+2011-08-29 Vincent Celier <celier@adacore.com>
+
+ * prj-attr.adb: New Compiler attribute Dependency_Kind and Language_Kind
+ * prj-conf.adb: Add_Default_GNAT_Naming_Scheme: Add a package Compiler
+ with declarations for Language_Kind and Dependency_Kind for Ada.
+ * prj-nmsc.adb (Check_Unit_Name): New name of procedure Check_Ada_Name
+ (Process_Compiler): Take into account the new attributes Dependency_Kind
+ and Language_Kind.
+ (Check_Configuration): Check if language kind is unit based, not if the
+ language name is Ada.
+ (Process_Exceptions_Unit_Based): Ditto
+ (Add_Language): Remove default additions of language and dependency kind
+ * prj.ads: Minor comment change
+ * snames.ads-tmpl: New standard names Dependency_Kind and Language_Kind
+
+2011-08-29 Johannes Kanig <kanig@adacore.com>
+
+ * debug.adb: Update comments.
+
2011-08-24 Joseph Myers <joseph@codesourcery.com>
* gcc-interface/Make-lang.in (CFLAGS-ada/tracebak.o)
-- d.E
-- d.F ALFA mode
-- d.G Precondition only mode for gnat2why
- -- d.H
+ -- d.H Standard package only mode for gnat2why
-- d.I SCIL generation mode
-- d.J Disable parallel SCIL generation mode
-- d.K
-- only generate Why code that checks for the well-guardedness of
-- preconditions.
+ -- d.H Standard package only mode for gnat2why. In this mode, gnat2why
+ -- will only generate Why code for package Standard. Any given input
+ -- file will be ignored.
+
-- d.I Generate SCIL mode. Generate intermediate code for the sake of
-- of static analysis tools, and ensure additional tree consistency
-- between different compilations of specs.
-- Is_Safe_To_Reevaluate Flag249
-- Has_Predicates Flag250
- -- (Has_Implicit_Dereference) Flag251
+ -- Has_Implicit_Dereference Flag251
-- Is_Processed_Transient Flag252
- -- Is_Postcondition_Proc Flag253
+ -- (unused) Flag253
-- (unused) Flag254
-----------------------
return Flag138 (Id);
end Is_Packed_Array_Type;
- function Is_Postcondition_Proc (Id : E) return B is
- begin
- pragma Assert (Ekind (Id) = E_Procedure);
- return Flag253 (Id);
- end Is_Postcondition_Proc;
-
function Is_Potentially_Use_Visible (Id : E) return B is
begin
pragma Assert (Nkind (Id) in N_Entity);
Set_Flag138 (Id, V);
end Set_Is_Packed_Array_Type;
- procedure Set_Is_Postcondition_Proc (Id : E; V : B := True) is
- begin
- pragma Assert (Ekind (Id) = E_Procedure);
- Set_Flag253 (Id, V);
- end Set_Is_Postcondition_Proc;
-
procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True) is
begin
pragma Assert (Nkind (Id) in N_Entity);
W ("Is_Package_Body_Entity", Flag160 (Id));
W ("Is_Packed", Flag51 (Id));
W ("Is_Packed_Array_Type", Flag138 (Id));
- W ("Is_Postcondition_Proc", Flag253 (Id));
W ("Is_Potentially_Use_Visible", Flag9 (Id));
W ("Is_Preelaborated", Flag59 (Id));
W ("Is_Primitive", Flag218 (Id));
-- an entity, then the Original_Array_Type field of this entity points
-- to the original array type for which this is the packed array type.
--- Is_Postcondition_Proc (Flag253)
--- Present in procedures. Set if entity is a procedure generated by the
--- compiler for a postcondition.
-
-- Is_Potentially_Use_Visible (Flag9)
-- Present in all entities. Set if entity is potentially use visible,
-- i.e. it is defined in a package that appears in a currently active
-- Is_Intrinsic_Subprogram (Flag64)
-- Is_Machine_Code_Subprogram (Flag137) (non-generic case only)
-- Is_Null_Init_Proc (Flag178)
- -- Is_Postcondition_Proc (Flag253) (non-generic case only)
-- Is_Primitive (Flag218)
-- Is_Primitive_Wrapper (Flag195) (non-generic case only)
-- Is_Private_Descendant (Flag53)
function Is_Package_Body_Entity (Id : E) return B;
function Is_Packed (Id : E) return B;
function Is_Packed_Array_Type (Id : E) return B;
- function Is_Postcondition_Proc (Id : E) return B;
function Is_Potentially_Use_Visible (Id : E) return B;
function Is_Preelaborated (Id : E) return B;
function Is_Primitive (Id : E) return B;
procedure Set_Is_Package_Body_Entity (Id : E; V : B := True);
procedure Set_Is_Packed (Id : E; V : B := True);
procedure Set_Is_Packed_Array_Type (Id : E; V : B := True);
- procedure Set_Is_Postcondition_Proc (Id : E; V : B := True);
procedure Set_Is_Potentially_Use_Visible (Id : E; V : B := True);
procedure Set_Is_Preelaborated (Id : E; V : B := True);
procedure Set_Is_Primitive (Id : E; V : B := True);
pragma Inline (Is_Overloadable);
pragma Inline (Is_Packed);
pragma Inline (Is_Packed_Array_Type);
- pragma Inline (Is_Postcondition_Proc);
pragma Inline (Is_Potentially_Use_Visible);
pragma Inline (Is_Preelaborated);
pragma Inline (Is_Primitive);
pragma Inline (Set_Is_Package_Body_Entity);
pragma Inline (Set_Is_Packed);
pragma Inline (Set_Is_Packed_Array_Type);
- pragma Inline (Set_Is_Postcondition_Proc);
pragma Inline (Set_Is_Potentially_Use_Visible);
pragma Inline (Set_Is_Preelaborated);
pragma Inline (Set_Is_Primitive);
Check_Same_Aggr_Bounds (N, 1);
end if;
+ -- In formal verification mode, leave the aggregate non-expanded
+
+ if ALFA_Mode then
+ return;
+ end if;
+
-- STEP 2
-- Here we test for is packed array aggregate that we can handle at
Next_Entity (Comp);
end loop;
- -- Deal with pragma Bit_Order setting non-standard bit order
+ -- Deal with Bit_Order attribute definition specifying a non-default
+ -- bit order.
if Reverse_Bit_Order (Rec) and then Base_Type (Rec) = Rec then
if not Placed_Component then
Pragma_Sloc : Source_Ptr := No_Location;
begin
-- For the case of a statement SCO for a pragma controlled by
- -- Set_SCO_Pragma_Enable, set Pragma_Sloc so that the SCO (and
+ -- Set_SCO_Pragma_Enabled, set Pragma_Sloc so that the SCO (and
-- those of any nested decision) is emitted only if the pragma
-- is enabled.
-- original tree associated with Cond.
procedure Set_SCO_Pragma_Enabled (Loc : Source_Ptr);
- -- This procedure is called from Sem_Prag when a pragma is disabled (i.e.
- -- when the Pragma_Enabled flag is unset). Loc is the Sloc of the N_Pragma
- -- node. This is used to disable the corresponding SCO table entry. Note
+ -- This procedure is called from Sem_Prag when a pragma is enabled (i.e.
+ -- when the Pragma_Enabled flag is set). Loc is the Sloc of the N_Pragma
+ -- node. This is used to enable the corresponding statement SCO entry. Note
-- that we use the Sloc as the key here, since in the generic case, the
-- analysis is on a copy of the node, which is different from the node
-- seen by Par_SCO in the parse tree (but the Sloc values are the same).
-- Configuration - Compiling
"Sadriver#" &
+ "Salanguage_kind#" &
+ "Sadependency_kind#" &
"Larequired_switches#" &
"Laleading_required_switches#" &
"Latrailing_required_switches#" &
-- Local variables
- Name : Name_Id;
- Naming : Project_Node_Id;
+ Name : Name_Id;
+ Naming : Project_Node_Id;
+ Compiler : Project_Node_Id;
-- Start of processing for Add_Default_GNAT_Naming_Scheme
Create_Attribute (Name_Default_Language, "ada");
+ Compiler := Create_Package (Project_Tree, Config_File, "compiler");
+ Create_Attribute
+ (Name_Language_Kind, "unit_based", "ada", Pkg => Compiler);
+ Create_Attribute
+ (Name_Dependency_Kind, "ALI_File", "ada", Pkg => Compiler);
+
Naming := Create_Package (Project_Tree, Config_File, "naming");
Create_Attribute (Name_Spec_Suffix, ".ads", "ada", Pkg => Naming);
Create_Attribute (Name_Separate_Suffix, ".adb", "ada", Pkg => Naming);
-- Copy Str into Name_Buffer, replacing Pattern with Replacement. Str is
-- converted to lower-case at the same time.
- procedure Check_Ada_Name (Name : String; Unit : out Name_Id);
- -- Check that a name is a valid Ada unit name
+ procedure Check_Unit_Name (Name : String; Unit : out Name_Id);
+ -- Check that a name is a valid unit name
procedure Check_Package_Naming
(Project : Project_Id;
Debug_Decrease_Indent ("done check");
end Check;
- --------------------
- -- Check_Ada_Name --
- --------------------
+ ---------------------
+ -- Check_Unit_Name --
+ ---------------------
- procedure Check_Ada_Name (Name : String; Unit : out Name_Id) is
+ procedure Check_Unit_Name (Name : String; Unit : out Name_Id) is
The_Name : String := Name;
Real_Name : Name_Id;
Need_Letter : Boolean := True;
end if;
end Is_Reserved;
- -- Start of processing for Check_Ada_Name
+ -- Start of processing for Check_Unit_Name
begin
To_Lower (The_Name);
Unit := No_Name;
end if;
- end Check_Ada_Name;
+ end Check_Unit_Name;
-------------------------
-- Check_Configuration --
if Lang_Index /= No_Language_Index then
case Current_Array.Name is
+ when Name_Dependency_Kind =>
+
+ -- Attribute Dependency_Kind (<language>)
+
+ Get_Name_String (Element.Value.Value);
+
+ begin
+ Lang_Index.Config.Dependency_Kind :=
+ Dependency_File_Kind'Value
+ (Name_Buffer (1 .. Name_Len));
+
+ exception
+ when Constraint_Error =>
+ Error_Msg
+ (Data.Flags,
+ "illegal value for Dependency_Kind",
+ Element.Value.Location,
+ Project);
+ end;
+
when Name_Dependency_Switches =>
-- Attribute Dependency_Switches (<language>)
In_Tree => Data.Tree);
end if;
+ when Name_Language_Kind =>
+ -- Attribute Language_Kind (<language>)
+
+ Get_Name_String (Element.Value.Value);
+
+ begin
+ Lang_Index.Config.Kind :=
+ Language_Kind'Value
+ (Name_Buffer (1 .. Name_Len));
+
+ exception
+ when Constraint_Error =>
+ Error_Msg
+ (Data.Flags,
+ "illegal value for Language_Kind",
+ Element.Value.Location,
+ Project);
+ end;
+
when Name_Include_Switches =>
-- Attribute Include_Switches (<language>)
-- Attribute Include_Path_File (<language>)
Lang_Index.Config.Include_Path_File :=
- Element.Value.Value;
+ Element.Value.Value;
when Name_Driver =>
when Name_Required_Switches |
Name_Leading_Required_Switches =>
Put (Into_List =>
- Lang_Index.Config.
- Compiler_Leading_Required_Switches,
+ Lang_Index.Config.
+ Compiler_Leading_Required_Switches,
From_List => Element.Value.Values,
In_Tree => Data.Tree);
when Name_Trailing_Required_Switches =>
Put (Into_List =>
- Lang_Index.Config.
- Compiler_Trailing_Required_Switches,
+ Lang_Index.Config.
+ Compiler_Trailing_Required_Switches,
From_List => Element.Value.Values,
In_Tree => Data.Tree);
Lang_Index := Project.Languages;
while Lang_Index /= No_Language_Index loop
- if Lang_Index.Name = Name_Ada then
+ if Lang_Index.Config.Kind = Unit_Based then
Lang_Index.Config.Naming_Data.Casing := Casing;
Lang_Index.Config.Naming_Data.Dot_Replacement := Dot_Replacement;
Prev_Index.Next := Lang_Index.Next;
end if;
- elsif Lang_Index.Name = Name_Ada then
+ elsif Lang_Index.Config.Kind = Unit_Based then
Prev_Index := Lang_Index;
-- For unit based languages, Dot_Replacement, Spec_Suffix and
if Lang_Index.Config.Naming_Data.Dot_Replacement = No_File then
Error_Msg
(Data.Flags,
- "Dot_Replacement not specified for Ada",
+ "Dot_Replacement not specified for " &
+ Get_Name_String (Lang_Index.Name),
No_Location, Project);
end if;
if Lang_Index.Config.Naming_Data.Spec_Suffix = No_File then
Error_Msg
(Data.Flags,
- "Spec_Suffix not specified for Ada",
+ "Spec_Suffix not specified for " &
+ Get_Name_String (Lang_Index.Name),
No_Location, Project);
end if;
if Lang_Index.Config.Naming_Data.Body_Suffix = No_File then
Error_Msg
(Data.Flags,
- "Body_Suffix not specified for Ada",
+ "Body_Suffix not specified for " &
+ Get_Name_String (Lang_Index.Name),
No_Location, Project);
end if;
(Lang_Id : Language_Ptr;
Kind : Source_Kind)
is
- Lang : constant Name_Id := Lang_Id.Name;
Exceptions : Array_Element_Id;
Element : Array_Element;
Unit : Name_Id;
Get_Name_String (Element.Index);
To_Lower (Name_Buffer (1 .. Name_Len));
- Unit := Name_Find;
Index := Element.Value.Index;
- -- For Ada, check if it is a valid unit name
+ -- Check if it is a valid unit name
- if Lang = Name_Ada then
- Get_Name_String (Element.Index);
- Check_Ada_Name (Name_Buffer (1 .. Name_Len), Unit);
+ Get_Name_String (Element.Index);
+ Check_Unit_Name (Name_Buffer (1 .. Name_Len), Unit);
- if Unit = No_Name then
- Err_Vars.Error_Msg_Name_1 := Element.Index;
- Error_Msg
- (Data.Flags,
- "%% is not a valid unit name.",
- Element.Value.Location, Project);
- end if;
+ if Unit = No_Name then
+ Err_Vars.Error_Msg_Name_1 := Element.Index;
+ Error_Msg
+ (Data.Flags,
+ "%% is not a valid unit name.",
+ Element.Value.Location, Project);
end if;
if Unit /= No_Name then
Project.Languages := Lang;
Lang.Name := Name;
Lang.Display_Name := Display_Name;
-
- if Name = Name_Ada then
- Lang.Config.Kind := Unit_Based;
- Lang.Config.Dependency_Kind := ALI_File;
- else
- Lang.Config.Kind := File_Based;
- end if;
end Add_Language;
-- Start of processing for Check_Programming_Languages
-- Name_Buffer contains the name of the unit in lower-cases. Check
-- that this is a valid unit name
- Check_Ada_Name (Name_Buffer (1 .. Name_Len), Unit);
+ Check_Unit_Name (Name_Buffer (1 .. Name_Len), Unit);
-- If there is a naming exception for the same unit, the file is not
-- a source for the unit.
type Language_Config is record
Kind : Language_Kind := File_Based;
- -- Kind of language. All languages are file based, except Ada which is
- -- unit based.
+ -- Kind of language. Most languages are file based. A few, such as Ada,
+ -- are unit based.
Naming_Data : Lang_Naming_Data;
-- The naming data for the languages (prefixes, etc.)
-- Processing depends on version of Ada
-- For Ada 95, we just renumber bits within a storage unit. We do the
- -- same for Ada 83 mode, since we recognize pragma Bit_Order in Ada 83,
- -- and are free to add this extension.
+ -- same for Ada 83 mode, since we recognize attribute Bit_Order in
+ -- Ada 83, and are free to add this extension.
if Ada_Version < Ada_2005 then
Comp := First_Component_Or_Discriminant (R);
Statements => Plist)));
Set_Ekind (Post_Proc, E_Procedure);
- Set_Is_Postcondition_Proc (Post_Proc);
-- If this is a procedure, set the Postcondition_Proc attribute on
-- the proper defining entity for the subprogram.
-- See if it is in the pragmas after a library level subprogram
elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+
+ -- In formal verification mode, analyze pragma expression for
+ -- correctness, as it is not expanded later.
+
+ if ALFA_Mode then
+ Analyze_PPC_In_Decl_Part
+ (N, Defining_Entity (Unit (Parent (Parent (N)))));
+ end if;
+
Chain_PPC (Unit (Parent (Parent (N))));
return;
end if;
return;
end if;
- -- Ada 2012 AI04-0144-2: Dangerous order dependence. Actuals in nested
+ -- Ada 2012 AI05-0144-2: Dangerous order dependence. Actuals in nested
-- calls within a construct have been collected. If one of them is
-- writable and overlaps with another one, evaluation of the enclosing
-- construct is nondeterministic. This is illegal in Ada 2012, but is
-- Set_Current_Entity --
------------------------
- -- The given entity is to be set as the currently visible definition
- -- of its associated name (i.e. the Node_Id associated with its name).
- -- All we have to do is to get the name from the identifier, and
- -- then set the associated Node_Id to point to the given entity.
+ -- The given entity is to be set as the currently visible definition of its
+ -- associated name (i.e. the Node_Id associated with its name). All we have
+ -- to do is to get the name from the identifier, and then set the
+ -- associated Node_Id to point to the given entity.
procedure Set_Current_Entity (E : Entity_Id) is
begin
end if;
end Get_Scoped_Name;
+ -- Start of processing for Unique_Name
+
begin
if E = Standard_Standard then
return Get_Name_String (Name_Standard);
Name_Default_Language : constant Name_Id := N + $;
Name_Default_Switches : constant Name_Id := N + $;
Name_Dependency_Driver : constant Name_Id := N + $;
+ Name_Dependency_Kind : constant Name_Id := N + $;
Name_Dependency_Switches : constant Name_Id := N + $;
Name_Driver : constant Name_Id := N + $;
Name_Excluded_Source_Dirs : constant Name_Id := N + $;
Name_Include_Path_File : constant Name_Id := N + $;
Name_Inherit_Source_Path : constant Name_Id := N + $;
Name_Languages : constant Name_Id := N + $;
+ Name_Language_Kind : constant Name_Id := N + $;
Name_Leading_Library_Options : constant Name_Id := N + $;
Name_Leading_Required_Switches : constant Name_Id := N + $;
Name_Leading_Switches : constant Name_Id := N + $;
OSDN Git Service
