From: Arnaud Charlet <charlet@gcc.gnu.org>
Date: Wed, 2 Jan 2013 10:15:44 +0000 (+0100)
Subject: [multiple changes]
X-Git-Tag: releases/gcc-4.8.0~1197
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=fab62a15d14a3a8cf4a534f48411108a776b1a81;p=thirdparty%2Fgcc.git

[multiple changes]

2013-01-02  Vincent Celier  <celier@adacore.com>

	* usage.adb: Minor reformatting.

2013-01-02  Arnaud Charlet  <charlet@adacore.com>

	* opt.ads: Fix typo.

2013-01-02  Thomas Quinot  <quinot@adacore.com>

	* par_sco.adb: Generate P decision SCOs for SPARK pragmas
	Assume and Loop_Invariant.

From-SVN: r194791
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0b7932b5c692..10b2b5a47252 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,16 @@
+2013-01-02  Vincent Celier  <celier@adacore.com>
+
+	* usage.adb: Minor reformatting.
+
+2013-01-02  Arnaud Charlet  <charlet@adacore.com>
+
+	* opt.ads: Fix typo.
+
+2013-01-02  Thomas Quinot  <quinot@adacore.com>
+
+	* par_sco.adb: Generate P decision SCOs for SPARK pragmas
+	Assume and Loop_Invariant.
+
 2013-01-02  Robert Dewar  <dewar@adacore.com>
 
 	* vms_data.ads: Add entry for Float_Check_Valid (-gnateF).
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 7e622148b482..944438b2071d 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -281,7 +281,7 @@ package Opt is
    --  Set to True to check that operations on predefined unconstrained float
    --  types (e.g. Float, Long_Float) do not overflow and generate infinities
    --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
-   --  of the -gnateo switch.
+   --  of the -gnateF switch.
 
    Check_Object_Consistency : Boolean := False;
    --  GNATBIND, GNATMAKE
@@ -1737,7 +1737,7 @@ package Opt is
    --  Set to True to check that operations on predefined unconstrained float
    --  types (e.g. Float, Long_Float) do not overflow and generate infinities
    --  or invalid values. Set by the Check_Float_Overflow pragma, or by use
-   --  of the -gnateo switch.
+   --  of the -gnateF switch.
 
    Check_Policy_List_Config : Node_Id;
    --  GNAT
diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb
index ea3b0cc19fe1..8062563ad64a 100644
--- a/gcc/ada/par_sco.adb
+++ b/gcc/ada/par_sco.adb
@@ -1890,10 +1890,13 @@ package body Par_SCO is
 
                begin
                   case Nam is
-                     when Name_Assert        |
-                          Name_Check         |
-                          Name_Precondition  |
-                          Name_Postcondition =>
+                     when Name_Assert         |
+                          Name_Assert_And_Cut |
+                          Name_Assume         |
+                          Name_Check          |
+                          Name_Loop_Invariant |
+                          Name_Precondition   |
+                          Name_Postcondition  =>
 
                         --  For Assert/Check/Precondition/Postcondition, we
                         --  must generate a P entry for the decision. Note
diff --git a/gcc/ada/usage.adb b/gcc/ada/usage.adb
index 3e55e647011d..030239da1382 100644
--- a/gcc/ada/usage.adb
+++ b/gcc/ada/usage.adb
@@ -170,7 +170,7 @@ begin
    --  Line for -gnatea switch
 
    Write_Switch_Char ("ea");
-   Write_Line ("Delimiter for automatically added switches (internal switch");
+   Write_Line ("Delimiter for automatically added switches (internal switch)");
 
    --  Line for -gnateA switch
 
@@ -255,7 +255,7 @@ begin
    --  Line for -gnatez switch
 
    Write_Switch_Char ("ez");
-   Write_Line ("Delimiter for automatically added switches (internal switch");
+   Write_Line ("Delimiter for automatically added switches (internal switch)");
 
    --  Line for -gnatE switch