+2011-08-05 Yannick Moy <moy@adacore.com>
+
+ * exp_ch7.adb (Establish_Transient_Scope): in formal verification mode,
+ if the node to wrap is a pragma check, this node and enclosed
+ expression are not expanded, so do not apply any transformations here.
+ * exp_prag.adb (Expand_Pragma_Check): document the need to avoid
+ introducing transient scopes.
+
+2011-08-05 Jose Ruiz <ruiz@adacore.com>
+
+ * adaint.c (__gnat_set_writable, __gnat_set_readable,
+ __gnat_set_executable, __gnat_set_non_writable, __gnat_set_non_readable,
+ __gnat_copy_attribs): On VxWorks 6.x and later, the required chmod
+ routine is available, so we use the default implementation of these
+ functions.
+ * s-os_lib.ads (Copy_File, Copy_Time_Stamps): Document that there is
+ support for copying attributes on VxWorks 6.
+
+2011-08-05 Yannick Moy <moy@adacore.com>
+
+ * debug.adb: Remove use of -gnatd.D.
+ * gnat1drv.adb (Adjust_Global_Switches): adjust switches for ALFA mode
+ * opt.ads: Simplify variables for ALFA mode, to keep one only
+ * restrict.adb, sem_prag.adb: Adapt treatment done for CodePeer mode
+ to ALFA mode.
+
+2011-08-05 Vincent Celier <celier@adacore.com>
+
+ * prj-conf.adb (Do_Autoconf): Look also for --RTS in
+ Builder'Default_Switches.
+
+2011-08-05 Vincent Celier <celier@adacore.com>
+
+ * makeusg.adb: Add lines for --create-map-file switches.
+
+2011-08-05 Ed Schonberg <schonberg@adacore.com>
+
+ * freeze.adb (Freeze_Entity): For a subprogram, if a type in the
+ profile is incomplete and the full view is available, replace it with
+ the full view.
+ * sem_ch6.adb (Possible_Freeze): if a type in the profile is
+ incomplete, freezing the subprogram is delayed until the full view is
+ frozen.
+ * sem_type.adb (Disambiguate): an ambiguity between a user-defined
+ fixed-point multiplication operator and the predefined operator is
+ resolved in favor of the user-defined one.
+
2011-08-05 Rainer Orth <ro@CeBiTec.Uni-Bielefeld.DE>
* init.c [__alpha__ && __osf__] (__gnat_error_handler): Use
#include <vxCpuLib.h>
#endif /* _WRS_CONFIG_SMP */
+/* We need to know the VxWorks version because some file operations
+ (such as chmod) are only available on VxWorks 6. */
+#include "version.h"
+
#endif /* VxWorks */
#if (defined (__mips) && defined (__sgi)) || defined (__APPLE__)
#include <unixio.h>
#endif
+#ifdef __vxworks
+/* S_IREAD and S_IWRITE are not defined in VxWorks */
+#ifndef S_IREAD
+#define S_IREAD (S_IRUSR | S_IRGRP | S_IROTH)
+#endif
+
+#ifndef S_IWRITE
+#define S_IWRITE (S_IWUSR)
+#endif
+#endif
+
/* We don't have libiberty, so use malloc. */
#define xmalloc(S) malloc (S)
#define xrealloc(V,S) realloc (V,S)
SetFileAttributes
(wname, GetFileAttributes (wname) & ~FILE_ATTRIBUTE_READONLY);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+ ! defined(__nucleus__)
GNAT_STRUCT_STAT statbuf;
if (GNAT_STAT (name, &statbuf) == 0)
if (__gnat_can_use_acl (wname))
__gnat_set_OWNER_ACL (wname, GRANT_ACCESS, FILE_GENERIC_EXECUTE);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+ ! defined(__nucleus__)
GNAT_STRUCT_STAT statbuf;
if (GNAT_STAT (name, &statbuf) == 0)
SetFileAttributes
(wname, GetFileAttributes (wname) | FILE_ATTRIBUTE_READONLY);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+ ! defined(__nucleus__)
GNAT_STRUCT_STAT statbuf;
if (GNAT_STAT (name, &statbuf) == 0)
if (__gnat_can_use_acl (wname))
__gnat_set_OWNER_ACL (wname, GRANT_ACCESS, FILE_GENERIC_READ);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+ ! defined(__nucleus__)
GNAT_STRUCT_STAT statbuf;
if (GNAT_STAT (name, &statbuf) == 0)
if (__gnat_can_use_acl (wname))
__gnat_set_OWNER_ACL (wname, DENY_ACCESS, FILE_GENERIC_READ);
-#elif ! defined (__vxworks) && ! defined(__nucleus__)
+#elif ! (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) && \
+ ! defined(__nucleus__)
GNAT_STRUCT_STAT statbuf;
if (GNAT_STAT (name, &statbuf) == 0)
int
__gnat_copy_attribs (char *from, char *to, int mode)
{
-#if defined (VMS) || defined (__vxworks) || defined (__nucleus__)
+#if defined (VMS) || (defined (__vxworks) && _WRS_VXWORKS_MAJOR < 6) || \
+ defined (__nucleus__)
return -1;
#elif defined (_WIN32) && !defined (RTX)
-- d.B
-- d.C Generate concatenation call, do not generate inline code
-- d.D
- -- d.E SPARK generation mode
- -- d.F Why generation mode
+ -- d.E
+ -- d.F ALFA mode
-- d.G
-- d.H
-- d.I SCIL generation mode
-- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases
-- where we would normally generate inline concatenation code.
- -- d.E SPARK generation mode. Generate intermediate code for the sake of
- -- formal verification through SPARK and the SPARK toolset.
-
- -- d.F Why generation mode. Generate intermediate code for the sake of
- -- formal verification through Why and the Why VC generator.
+ -- d.F ALFA mode. Generate AST in a form suitable for formal verification,
+ -- as well as additional cross reference information in ALI files to
+ -- compute effects of subprograms.
-- d.I Generate SCIL mode. Generate intermediate code for the sake of
-- of static analysis tools, and ensure additional tree consistency
elsif Nkind (Wrap_Node) = N_Iteration_Scheme then
null;
+ -- In formal verification mode, if the node to wrap is a pragma check,
+ -- this node and enclosed expression are not expanded, so do not apply
+ -- any transformations here.
+
+ elsif ALFA_Mode
+ and then Nkind (Wrap_Node) = N_Pragma
+ and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
+ then
+ null;
+
else
Push_Scope (New_Internal_Entity (E_Block, Current_Scope, Loc, 'B'));
Set_Scope_Is_Transient;
-- be an explicit conditional in the source, not an implicit if, so we
-- do not call Make_Implicit_If_Statement.
- -- In formal verification mode, we keep the pragma check in the code
+ -- In formal verification mode, we keep the pragma check in the code,
+ -- and its enclosed expression is not expanded. This requires that no
+ -- transient scope is introduced for pragma check in this mode in
+ -- Exp_Ch7.Establish_Transient_Scope.
if ALFA_Mode then
return;
Formal := First_Formal (E);
while Present (Formal) loop
F_Type := Etype (Formal);
+
+ -- AI05-0151 : incomplete types can appear in a profile.
+ -- By the time the entity is frozen, the full view must
+ -- be available, unless it is a limited view.
+
+ if Is_Incomplete_Type (F_Type)
+ and then Present (Full_View (F_Type))
+ then
+ F_Type := Full_View (F_Type);
+ Set_Etype (Formal, F_Type);
+ end if;
+
Freeze_And_Append (F_Type, N, Result);
if Is_Private_Type (F_Type)
-- Freeze return type
R_Type := Etype (E);
+
+ -- AI05-0151: the return type may have been incomplete
+ -- at the point of declaration.
+
+ if Ekind (R_Type) = E_Incomplete_Type
+ and then Present (Full_View (R_Type))
+ then
+ R_Type := Full_View (R_Type);
+ Set_Etype (E, R_Type);
+ end if;
+
Freeze_And_Append (R_Type, N, Result);
-- Check suspicious return type for C function
Back_End_Handles_Limited_Types := False;
end if;
- -- Set switches for formal verification modes
-
- if Debug_Flag_Dot_EE then
- ALFA_Through_SPARK_Mode := True;
- end if;
+ -- Set switches for formal verification mode
if Debug_Flag_Dot_FF then
- ALFA_Through_Why_Mode := True;
- end if;
- ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode;
+ ALFA_Mode := True;
+
+ -- Turn off inlining, which would confuse formal verification output
+ -- and gain nothing.
+
+ Front_End_Inlining := False;
+ Inline_Active := False;
+
+ -- Disable front-end optimizations, to keep the tree as close to the
+ -- source code as possible, and also to avoid inconsistencies between
+ -- trees when using different optimization switches.
+
+ Optimization_Level := 0;
+
+ -- Enable some restrictions systematically to simplify the generated
+ -- code (and ease analysis). Note that restriction checks are also
+ -- disabled in ALFA mode, see Restrict.Check_Restriction, and user
+ -- specified Restrictions pragmas are ignored, see
+ -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
+
+ Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
+
+ -- Suppress all language checks since they are handled implicitly by
+ -- the formal verification backend.
+ -- Turn off dynamic elaboration checks.
+ -- Turn off alignment checks.
+ -- Turn off validity checking.
+
+ Suppress_Options := (others => True);
+ Enable_Overflow_Checks := False;
+ Dynamic_Elaboration_Checks := False;
+ Reset_Validity_Check_Options;
+
+ -- Kill debug of generated code, since it messes up sloc values
+
+ Debug_Generated_Code := False;
+
+ -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
+
+ Xref_Active := True;
+
+ -- Polling mode forced off, since it generates confusing junk
+
+ Polling_Required := False;
+
+ -- Set operating mode to Generate_Code to benefit from full front-end
+ -- expansion (e.g. default arguments).
+
+ Operating_Mode := Generate_Code;
+
+ -- Skip call to gigi
+
+ Debug_Flag_HH := True;
+
+ -- Enable assertions and debug pragmas, since they give valuable
+ -- extra information for formal verification.
+
+ Assertions_Enabled := True;
+ Debug_Pragmas_Enabled := True;
+
+ -- Turn off style check options since we are not interested in any
+ -- front-end warnings when we are getting ALFA output.
+
+ Reset_Style_Check_Options;
+
+ -- Suppress compiler warnings, since what we are
+ -- interested in here is what formal verification can find out.
+
+ Warning_Mode := Suppress;
+
+ -- Always perform semantics and generate ALI files in ALFA mode,
+ -- so that a gnatmake -c -k will proceed further when possible.
+
+ Force_ALI_Tree_File := True;
+ Try_Semantics := True;
+ end if;
end Adjust_Global_Switches;
--------------------
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
Write_Eol;
Write_Eol;
+ Write_Str (" --create-map-file Create map file mainprog.map");
+ Write_Eol;
+
+ Write_Str (" --create-map-file=mapfile");
+ Write_Eol;
+ Write_Str (" Create map file mapfile");
+ Write_Eol;
+
Write_Str (" --GCC=command Use this gcc command");
Write_Eol;
-- Used to store the ASIS version number read from a tree file to check if
-- it is the same as stored in the ASIS version number in Tree_IO.
- -----------------------------------
- -- Modes for Formal Verification --
- -----------------------------------
+ ----------------------------------
+ -- Mode for Formal Verification --
+ ----------------------------------
- -- These modes are currently defined through debug flags
+ -- This mode is currently defined through a debug flag
ALFA_Mode : Boolean := False;
- -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
-
- ALFA_Through_SPARK_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of SPARK code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
-
- ALFA_Through_Why_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 ALFA subset of Ada. Set by debuf flag -gnatd.F.
+ -- Specific compiling mode targeting formal verification through the
+ -- generation of Why code for those parts of the input code that belong to
+ -- the ALFA subset of Ada. Set by debuf flag -gnatd.F.
private
Builder : constant Package_Id :=
Value_Of (Name_Builder, Project.Decl.Packages, Shared);
Switch_Array_Id : Array_Element_Id;
- Switch_Array : Array_Element;
- Switch_List : String_List_Id := Nil_String;
- Switch : String_Element;
+ procedure Check_RTS_Switches;
+ -- Take into account eventual switches --RTS in
+ -- Switch_Array_Id.
- Lang : Name_Id;
- Lang_Last : Positive;
+ ------------------------
+ -- Check_RTS_SWitches --
+ ------------------------
- begin
- if Builder /= No_Package then
- Switch_Array_Id :=
- Value_Of
- (Name => Name_Switches,
- In_Arrays =>
- Shared.Packages.Table (Builder).Decl.Arrays,
- Shared => Shared);
+ procedure Check_RTS_Switches is
+ Switch_Array : Array_Element;
+
+ Switch_List : String_List_Id := Nil_String;
+ Switch : String_Element;
+ Lang : Name_Id;
+ Lang_Last : Positive;
+ begin
while Switch_Array_Id /= No_Array_Element loop
Switch_Array :=
Shared.Array_Elements.Table (Switch_Array_Id);
Switch_Array_Id := Switch_Array.Next;
end loop;
+ end Check_RTS_Switches;
+
+ begin
+ if Builder /= No_Package then
+ Switch_Array_Id :=
+ Value_Of
+ (Name => Name_Switches,
+ In_Arrays =>
+ Shared.Packages.Table (Builder).Decl.Arrays,
+ Shared => Shared);
+ Check_RTS_Switches;
+
+ Switch_Array_Id :=
+ Value_Of
+ (Name => Name_Default_Switches,
+ In_Arrays =>
+ Shared.Packages.Table (Builder).Decl.Arrays,
+ Shared => Shared);
+ Check_RTS_Switches;
end if;
end;
end if;
begin
Msg_Issued := False;
- -- In CodePeer mode, we do not want to check for any restriction, or set
- -- additional restrictions other than those already set in gnat1drv.adb
- -- so that we have consistency between each compilation.
+ -- In CodePeer and ALFA mode, we do not want to check for any
+ -- restriction, or set additional restrictions other than those already
+ -- set in gnat1drv.adb so that we have consistency between each
+ -- compilation.
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
return;
end if;
-- --
-- S p e c --
-- --
--- Copyright (C) 1995-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1995-2011, 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- --
-- effect of "cp -p" on Unix systems, and None corresponds to the typical
-- effect of "cp" on Unix systems.
- -- Note: Time_Stamps and Full are not supported on VMS and VxWorks
+ -- Note: Time_Stamps and Full are not supported on VMS and VxWorks 5
procedure Copy_File
(Name : String;
-- furthermore Dest must be writable. Success will be set to True if the
-- operation was successful and False otherwise.
--
- -- Note: this procedure is not supported on VMS and VxWorks. On these
+ -- Note: this procedure is not supported on VMS and VxWorks 5. On these
-- platforms, Success is always set to False.
function Read
elsif Ekind (T) = E_Incomplete_Type and then From_With_Type (T) then
Set_Has_Delayed_Freeze (Designator);
+
+ -- AI05-0151 : incomplete types can now appear in the profile of a
+ -- subprogram or entry declaration.
+
+ elsif Ekind (T) = E_Incomplete_Type
+ and then Ada_Version >= Ada_2012
+ then
+ Set_Has_Delayed_Freeze (Designator);
end if;
end Possible_Freeze;
-- Start of processing for Process_Restrictions_Or_Restriction_Warnings
begin
- -- Ignore all Restrictions pragma in CodePeer mode
+ -- Ignore all Restrictions pragma in CodePeer and ALFA modes
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
return;
end if;
-- Start of processing for Process_Suppress_Unsuppress
begin
- -- Ignore pragma Suppress/Unsuppress in codepeer mode on user code:
- -- we want to generate checks for analysis purposes, as set by -gnatC
+ -- Ignore pragma Suppress/Unsuppress in CodePeer and ALFA modes on
+ -- user code: we want to generate checks for analysis purposes, as
+ -- set respectively by -gnatC and -gnatd.F
- if CodePeer_Mode and then Comes_From_Source (N) then
+ if (CodePeer_Mode or else ALFA_Mode)
+ and then Comes_From_Source (N)
+ then
return;
end if;
Check_Valid_Configuration_Pragma;
Check_Restriction (No_Initialize_Scalars, N);
- -- Initialize_Scalars creates false positives in CodePeer,
- -- so ignore this pragma in this mode.
+ -- Initialize_Scalars creates false positives in CodePeer, and
+ -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- in these modes.
if not Restriction_Active (No_Initialize_Scalars)
- and then not CodePeer_Mode
+ and then not (CodePeer_Mode or else ALFA_Mode)
then
Init_Or_Norm_Scalars := True;
Initialize_Scalars := True;
when Pragma_Inline_Always =>
GNAT_Pragma;
- -- Pragma always active unless in CodePeer mode, since this causes
- -- walk order issues.
+ -- Pragma always active unless in CodePeer or ALFA mode, since
+ -- this causes walk order issues.
- if not CodePeer_Mode then
+ if not (CodePeer_Mode or else ALFA_Mode) then
Process_Inline (True);
end if;
Check_Arg_Count (0);
Check_Valid_Configuration_Pragma;
- -- Normalize_Scalars creates false positives in CodePeer, so
- -- ignore this pragma in this mode.
+ -- Normalize_Scalars creates false positives in CodePeer, and
+ -- incorrect negative results in ALFA mode, so ignore this pragma
+ -- in these modes.
- if not CodePeer_Mode then
+ if not (CodePeer_Mode or else ALFA_Mode) then
Normalize_Scalars := True;
Init_Or_Norm_Scalars := True;
end if;
-- In the context of static code analysis, we do not need
-- complex front-end expansions related to pragma Pack,
- -- so disable handling of pragma Pack in this case.
+ -- so disable handling of pragma Pack in these cases.
- if CodePeer_Mode then
+ if CodePeer_Mode or else ALFA_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly
end if;
-- Otherwise, the predefined operator has precedence, or if the user-
- -- defined operation is directly visible we have a true ambiguity. If
- -- this is a fixed-point multiplication and division in Ada83 mode,
+ -- defined operation is directly visible we have a true ambiguity.
+
+ -- If this is a fixed-point multiplication and division in Ada83 mode,
-- exclude the universal_fixed operator, which often causes ambiguities
-- in legacy code.
+ -- Ditto in Ada2012, where an ambiguity may arise for an operation on
+ -- a partial view that is completed with a fixed point type. See
+ -- AI05-0020 and AI05-0209. The ambiguity is resolved in favor of the
+ -- user-defined subprogram so that a client of the package has the
+ -- same resulution as the body of the package.
+
else
if (In_Open_Scopes (Scope (User_Subp))
or else Is_Potentially_Use_Visible (User_Subp))
if Is_Fixed_Point_Type (Typ)
and then (Chars (Nam1) = Name_Op_Multiply
or else Chars (Nam1) = Name_Op_Divide)
- and then Ada_Version = Ada_83
+ and then
+ (Ada_Version = Ada_83
+ or else
+ (Ada_Version >= Ada_2012
+ and then
+ In_Same_Declaration_List
+ (Typ, Unit_Declaration_Node (User_Subp))))
then
if It2.Nam = Predef_Subp then
return It1;
projects / gcc.git / commitdiff