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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177432 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 77 insertions, 8 deletions

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index eabf1123d4a..be047854b62 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;
 
    --------------------