From 406935b64c887e2e7bb2882f4db5d2fa2e451b73 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 5 Aug 2011 15:32:13 +0200 Subject: [multiple changes] 2011-08-05 Yannick Moy * 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 * 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 * 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 * prj-conf.adb (Do_Autoconf): Look also for --RTS in Builder'Default_Switches. 2011-08-05 Vincent Celier * makeusg.adb: Add lines for --create-map-file switches. 2011-08-05 Ed Schonberg * 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. From-SVN: r177432 --- gcc/ada/ChangeLog | 47 +++++++++++++++++++++++++++++ gcc/ada/adaint.c | 33 ++++++++++++++++---- gcc/ada/debug.adb | 12 ++++---- gcc/ada/exp_ch7.adb | 10 +++++++ gcc/ada/exp_prag.adb | 5 +++- gcc/ada/freeze.adb | 23 ++++++++++++++ gcc/ada/gnat1drv.adb | 85 +++++++++++++++++++++++++++++++++++++++++++++++----- gcc/ada/makeusg.adb | 10 ++++++- gcc/ada/opt.ads | 22 +++++--------- gcc/ada/prj-conf.adb | 46 ++++++++++++++++++++-------- gcc/ada/restrict.adb | 9 +++--- gcc/ada/s-os_lib.ads | 6 ++-- gcc/ada/sem_ch6.adb | 8 +++++ gcc/ada/sem_prag.adb | 37 +++++++++++++---------- gcc/ada/sem_type.adb | 19 ++++++++++-- 15 files changed, 295 insertions(+), 77 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6a0b21d..5759eae 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,50 @@ +2011-08-05 Yannick Moy + + * 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 + + * 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 + + * 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 + + * prj-conf.adb (Do_Autoconf): Look also for --RTS in + Builder'Default_Switches. + +2011-08-05 Vincent Celier + + * makeusg.adb: Add lines for --create-map-file switches. + +2011-08-05 Ed Schonberg + + * 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 * init.c [__alpha__ && __osf__] (__gnat_error_handler): Use diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c index ab8446d..556101d 100644 --- a/gcc/ada/adaint.c +++ b/gcc/ada/adaint.c @@ -56,6 +56,10 @@ extern "C" { #include #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__) @@ -84,6 +88,17 @@ extern "C" { #include #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) @@ -2191,7 +2206,8 @@ __gnat_set_writable (char *name) 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) @@ -2213,7 +2229,8 @@ __gnat_set_executable (char *name) 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) @@ -2240,7 +2257,8 @@ __gnat_set_non_writable (char *name) 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) @@ -2262,7 +2280,8 @@ __gnat_set_readable (char *name) 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) @@ -2283,7 +2302,8 @@ __gnat_set_non_readable (char *name) 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) @@ -3555,7 +3575,8 @@ char __gnat_environment_char = '$'; 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) diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index e024927..329e687 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -122,8 +122,8 @@ package body Debug is -- 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 @@ -580,11 +580,9 @@ package body Debug is -- 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 diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 9138442..443c6ff 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -3532,6 +3532,16 @@ package body Exp_Ch7 is 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; diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index b1900a9..5c3d2ca 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -321,7 +321,10 @@ package body Exp_Prag is -- 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; diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index a31e647..9bd0e9c 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2461,6 +2461,18 @@ package body Freeze is 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) @@ -2631,6 +2643,17 @@ package body Freeze is -- 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 diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index eabf112..be04785 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -390,17 +390,86 @@ procedure Gnat1drv is 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; -------------------- diff --git a/gcc/ada/makeusg.adb b/gcc/ada/makeusg.adb index bc34387..f2889a2 100644 --- a/gcc/ada/makeusg.adb +++ b/gcc/ada/makeusg.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -249,6 +249,14 @@ begin 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; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index d4d0373..55e57c4 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1855,24 +1855,16 @@ package Opt is -- 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 diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb index 2df6693..ab297e5 100644 --- a/gcc/ada/prj-conf.adb +++ b/gcc/ada/prj-conf.adb @@ -976,23 +976,24 @@ package body Prj.Conf is 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); @@ -1057,6 +1058,25 @@ package body Prj.Conf is 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; diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 44e3b5f..a8dcff6 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -375,11 +375,12 @@ package body Restrict is 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; diff --git a/gcc/ada/s-os_lib.ads b/gcc/ada/s-os_lib.ads index a6418de..85e77eb 100755 --- a/gcc/ada/s-os_lib.ads +++ b/gcc/ada/s-os_lib.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -343,7 +343,7 @@ package System.OS_Lib is -- 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; @@ -371,7 +371,7 @@ package System.OS_Lib is -- 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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 986a1e8..537aa02 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4527,6 +4527,14 @@ package body Sem_Ch6 is 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; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index fe9cb2e..de3e307 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -5059,9 +5059,9 @@ package body Sem_Prag is -- 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; @@ -5283,10 +5283,13 @@ package body Sem_Prag is -- 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; @@ -9444,11 +9447,12 @@ package body Sem_Prag is 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; @@ -9475,10 +9479,10 @@ package body Sem_Prag is 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; @@ -10917,10 +10921,11 @@ package body Sem_Prag is 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; @@ -11287,9 +11292,9 @@ package body Sem_Prag is -- 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 diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb index 12f3913..1474677 100644 --- a/gcc/ada/sem_type.adb +++ b/gcc/ada/sem_type.adb @@ -1932,11 +1932,18 @@ package body Sem_Type is 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)) @@ -1945,7 +1952,13 @@ package body Sem_Type is 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; -- cgit v1.1