* gcc-interface/lang.opt: Add AdaWhy language, simimlar to Ada.

	* gcc-interface/lang-specs.h: Add handling of AdaWhy specs (calls       
	gnat1why).


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

3 files changed, 45 insertions, 23 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index dcc0de2ec2f..5bbfb6eb6d9 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2011-08-04  Arnaud Charlet  <charlet@adacore.com>
+
+	* gcc-interface/lang.opt: Add AdaWhy language, simimlar to Ada.
+	* gcc-interface/lang-specs.h: Add handling of AdaWhy specs (calls
+	gnat1why).
+
 2011-08-04  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch3.adb, make.adb, a-cohata.ads, sem_prag.adb, makeutl.adb,
diff --git a/gcc/ada/gcc-interface/lang-specs.h b/gcc/ada/gcc-interface/lang-specs.h
index 5fd30b97811..ff3de85b986 100644
--- a/gcc/ada/gcc-interface/lang-specs.h
+++ b/gcc/ada/gcc-interface/lang-specs.h
@@ -6,7 +6,7 @@
  *                                                                          *
  *                              C Header File                               *
  *                                                                          *
- *           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- *
@@ -46,3 +46,16 @@
     %i %{S:%W{o*}%{!o*:-o %b.s}} \
     %{gnatc*|gnats*: -o %j} %{-param*} \
     %{!gnatc*:%{!gnats*:%(invoke_as)}}", 0, 0, 0},
+
+  {"@adawhy",
+   "\
+ %{!c:%e-c required for gnat2why}\
+ gnat1why %{I*} %{k8:-gnatk8} %{!Q:-quiet}\
+    %{nostdinc*} %{nostdlib*}\
+    -dumpbase %{.adb:%b.adb}%{.ads:%b.ads}%{!.adb:%{!.ads:%b.ada}}\
+    %{o*:-auxbase-strip %*}%{!o*:-auxbase %b} \
+    %{a} %{d*} %{f*} \
+    %{gnatea:-gnatez} %{g*&m*} \
+    %1 %{o*:%w%*-gnatO} \
+    %i \
+    %{gnatc*|gnats*: -o %j} %{-param*} ", 0, 0, 0},
diff --git a/gcc/ada/gcc-interface/lang.opt b/gcc/ada/gcc-interface/lang.opt
index 9f1a69f9820..fd79c300112 100644
--- a/gcc/ada/gcc-interface/lang.opt
+++ b/gcc/ada/gcc-interface/lang.opt
@@ -25,89 +25,92 @@
 Language
 Ada
 
+Language
+AdaWhy
+
 -all-warnings
-Ada Alias(Wall)
+Ada AdaWhy Alias(Wall)
 
 -include-barrier
-Ada Alias(I, -)
+Ada AdaWhy Alias(I, -)
 
 -include-directory
-Ada Separate Alias(I)
+Ada AdaWhy Separate Alias(I)
 
 -include-directory=
-Ada Joined Alias(I)
+Ada AdaWhy Joined Alias(I)
 
 -no-standard-includes
-Ada Alias(nostdinc)
+Ada AdaWhy Alias(nostdinc)
 
 -no-standard-libraries
-Ada Alias(nostdlib)
+Ada AdaWhy Alias(nostdlib)
 
 I
-Ada Joined Separate
+Ada AdaWhy Joined Separate
 ; Documented for C
 
 Wall
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wmissing-prototypes
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wstrict-prototypes
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wwrite-strings
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wlong-long
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wvariadic-macros
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wold-style-definition
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Wmissing-format-attribute
-Ada
+Ada AdaWhy
 ; Documented for C
 
 Woverlength-strings
-Ada
+Ada AdaWhy
 ; Documented for C
 
 k8
 Driver
 
 nostdinc
-Ada RejectNegative
+Ada AdaWhy RejectNegative
 ; Don't look for source files
 
 nostdlib
-Ada
+Ada AdaWhy
 ; Don't look for object files
 
 fRTS=
-Ada Joined RejectNegative
+Ada AdaWhy Joined RejectNegative
 ; Selects the runtime
 
 gant
-Ada Joined Undocumented
+Ada AdaWhy Joined Undocumented
 ; Catches typos
 
 gnatO
-Ada Separate
+Ada AdaWhy Separate
 ; Sets name of output ALI file (internal switch)
 
 gnat
-Ada Joined
+Ada AdaWhy Joined
 -gnat<options>	Specify options to GNAT
 
 ; This comment is to ensure we retain the blank line above.