From 3a8e3f636ac1597af351f7907ab684959d41b226 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 11 Apr 2013 12:18:47 +0200 Subject: [PATCH] [multiple changes] 2013-04-11 Johannes Kanig * opt.ads New global boolean Frame_Condition_Mode to avoid referring to command line switch. * gnat1drv.adb (Gnat1drv) set frame condition mode when -gnatd.G is present, and disable Code generation in that case. Disable ALI file generation when switch is *not* present. 2013-04-11 Ed Schonberg * sem_ch6.adb (Analyze_Expression_Function): Perform the pre-analysis on a copy of the expression, to prevent downstream visbility issues involving operators and instantiations. From-SVN: r197758 --- gcc/ada/ChangeLog | 14 ++++++++++++++ gcc/ada/gnat1drv.adb | 29 ++++++++++++++++------------- gcc/ada/opt.ads | 6 ++++++ gcc/ada/sem_ch6.adb | 7 ++++++- 4 files changed, 42 insertions(+), 14 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index dc0dd405be5..09886035695 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2013-04-11 Johannes Kanig + + * opt.ads New global boolean Frame_Condition_Mode to avoid + referring to command line switch. + * gnat1drv.adb (Gnat1drv) set frame condition mode when -gnatd.G + is present, and disable Code generation in that case. Disable + ALI file generation when switch is *not* present. + +2013-04-11 Ed Schonberg + + * sem_ch6.adb (Analyze_Expression_Function): Perform the + pre-analysis on a copy of the expression, to prevent downstream + visbility issues involving operators and instantiations. + 2013-04-11 Johannes Kanig * debug.adb: Reservation and documentation for -gnatd.G switch. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 47c27da0114..37a4fb2fcae 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -302,6 +302,18 @@ procedure Gnat1drv is Strict_Alfa_Mode := True; end if; + -- Distinguish between the two modes of gnat2why: frame condition + -- generation (generation of ALI files) and translation of Why (no + -- ALI files generated). This is done with the switch -gnatd.G, + -- which activates frame condition mode. The other changes in + -- behavior depending on this switch are done in gnat2why directly. + + if Debug_Flag_Dot_GG then + Frame_Condition_Mode := True; + else + Opt.Disable_ALI_File := True; + end if; + -- Turn off inlining, which would confuse formal verification output -- and gain nothing. @@ -409,16 +421,6 @@ procedure Gnat1drv is Tagged_Type_Expansion := False; - -- Distinguish between the two modes of gnat2why: frame condition - -- generation (generation of ALI files) and translation of Why (no - -- ALI files generated). This is done with the switch -gnatd.G, - -- which activates frame condition mode. The other changes in - -- behavior depending on this switch are done in gnat2why directly. - - if not Debug_Flag_Dot_GG then - Opt.Disable_ALI_File := True; - end if; - end if; -- Set Configurable_Run_Time mode if system.ads flag set @@ -1041,10 +1043,11 @@ begin elsif Main_Kind in N_Generic_Renaming_Declaration then Back_End_Mode := Generate_Object; - -- It is not an error to analyze (in CodePeer or Alfa modes) a spec - -- which requires a body, when the body is not available. + -- It is not an error to analyze (in CodePeer mode or Alfa mode with + -- generation of Why) a spec which requires a body, when the body is + -- not available. - elsif CodePeer_Mode or Alfa_Mode then + elsif CodePeer_Mode or (Alfa_Mode and not Frame_Condition_Mode) then Back_End_Mode := Generate_Object; -- In all other cases (specs which have bodies, generics, and bodies diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index ee1c73f87e1..5e80dc76fe1 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1984,6 +1984,12 @@ package Opt is -- generation of Why code for those parts of the input code that belong to -- the Alfa subset of Ada. Set by debug flag -gnatd.F. + Frame_Condition_Mode : Boolean := False; + -- Specific mode to be used in combination with Alfa_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. + Strict_Alfa_Mode : Boolean := False; -- Interpret compiler permissions as strictly as possible. E.g. base ranges -- for integers are limited to the strict minimum with this option. Set by diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 7b31ff572e6..707ed45f56c 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -444,7 +444,12 @@ package body Sem_Ch6 is Insert_After (Last (Decls), New_Body); Push_Scope (Id); Install_Formals (Id); - Preanalyze_Spec_Expression (Expression (Ret), Etype (Id)); + + -- Do a preanalysis of the expression on a separate copy, to + -- prevent visibility issues later with operators in instances. + + Preanalyze_Spec_Expression + (New_Copy_Tree (Expression (Ret)), Etype (Id)); End_Scope; end; end if;