[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 0b7932b5c69262eb4e657ea7178feab1e1299571..10b2b5a47252e3bce6c2441393dad695b2827bf7 100644 (file)
--- 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 7e622148b482731e58582eb2f419418ceab1d552..944438b2071d547a46b7baf7b79ece359f32ecba 100644 (file)
--- 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 ea3b0cc19fe1b62cd5d93d41e3d280fa283296de..8062563ad64a32ec650f239314a5e891ee44234e 100644 (file)
--- 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 3e55e647011d37659bb23d443fdccfe8cddaffa2..030239da13826fd10d088c2e70936dfbe3f432c1 100644 (file)
--- 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