sem_ch11.adb (Analyze_Raise_xxx_Error): do not mark such nodes as not in ALFA.

2011-08-03  Yannick Moy  <moy@adacore.com>

	* sem_ch11.adb (Analyze_Raise_xxx_Error): do not mark such nodes as not
	in ALFA. Instead, they are considered as assertions to prove.
	* sem_ch4.adb (Analyze_Conditional_Expression): do not always mark such
	nodes as not in ALFA. Instead, include conditional expressions in ALFA
	if they have no ELSE part, or if they occur in pre- and postconditions,
	where the Condition cannot have side-effects in ALFA
	(Analyze_Membership_Op): do not mark such nodes as not in ALFA
	(Analyze_Type_Conversion): do not always mark such nodes as not in ALFA.
	Instead, include type conversion between scalar types in ALFA.
	* sem_ch6.adb (Process_Formals): correctly mark a parameter in ALFA
	if-and-only-if its type is in ALFA.

From-SVN: r177285

4 files changed, 39 insertions, 12 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index fb01723..b4f495c 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2011-08-03  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch11.adb (Analyze_Raise_xxx_Error): do not mark such nodes as not
+	in ALFA. Instead, they are considered as assertions to prove.
+	* sem_ch4.adb (Analyze_Conditional_Expression): do not always mark such
+	nodes as not in ALFA. Instead, include conditional expressions in ALFA
+	if they have no ELSE part, or if they occur in pre- and postconditions,
+	where the Condition cannot have side-effects in ALFA
+	(Analyze_Membership_Op): do not mark such nodes as not in ALFA
+	(Analyze_Type_Conversion): do not always mark such nodes as not in ALFA.
+	Instead, include type conversion between scalar types in ALFA.
+	* sem_ch6.adb (Process_Formals): correctly mark a parameter in ALFA
+	if-and-only-if its type is in ALFA.
+
 2011-08-03  Thomas Quinot  <quinot@adacore.com>
 
 	* scos.adb, get_scos.adb, put_scos.adb
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index 53f79cb..6942835 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -602,7 +602,6 @@ package body Sem_Ch11 is
    --  Start of processing for Analyze_Raise_xxx_Error
 
    begin
-      Mark_Non_ALFA_Subprogram;
       Check_SPARK_Restriction ("raise statement is not allowed", N);
 
       if No (Etype (N)) then
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index dd527b2..1e49456 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -1520,11 +1520,23 @@ package body Sem_Ch4 is
          return;
       end if;
 
-      Mark_Non_ALFA_Subprogram;
       Check_SPARK_Restriction ("conditional expression is not allowed", N);
 
       Else_Expr := Next (Then_Expr);
 
+      --  In ALFA, conditional expressions are allowed:
+      --    * if they have no ELSE part, in which case the expression is
+      --      equivalent to
+      --        NOT Condition OR ELSE Then_Expr
+      --    * in pre- and postconditions, where the Condition cannot have side-
+      --      effects (in ALFA) and thus the expression is equivalent to
+      --        (Condition AND THEN Then_Expr)
+      --          and (NOT Condition AND THEN Then_Expr)
+
+      if Present (Else_Expr) and then not In_Pre_Post_Expression then
+         Mark_Non_ALFA_Subprogram;
+      end if;
+
       if Comes_From_Source (N) then
          Check_Compiler_Unit (N);
       end if;
@@ -2483,8 +2495,6 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Membership_Op
 
    begin
-      Mark_Non_ALFA_Subprogram;
-
       Analyze_Expression (L);
 
       if No (R)
@@ -4375,8 +4385,6 @@ package body Sem_Ch4 is
       T    : Entity_Id;
 
    begin
-      Mark_Non_ALFA_Subprogram;
-
       --  If Conversion_OK is set, then the Etype is already set, and the
       --  only processing required is to analyze the expression. This is
       --  used to construct certain "illegal" conversions which are not
@@ -4398,6 +4406,13 @@ package body Sem_Ch4 is
       Analyze_Expression (Expr);
       Validate_Remote_Type_Type_Conversion (N);
 
+      --  Type conversion between scalar types are allowed in ALFA. All other
+      --  type conversions are not allowed.
+
+      if not (Is_Scalar_Type (Etype (Expr)) and then Is_Scalar_Type (T)) then
+         Mark_Non_ALFA_Subprogram;
+      end if;
+
       --  Only remaining step is validity checks on the argument. These
       --  are skipped if the conversion does not come from the source.
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index ebc1c71..854810f 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -8881,13 +8881,12 @@ package body Sem_Ch6 is
 
          Set_Etype (Formal, Formal_Type);
 
-         --  If the type of a subprogram's formal parameter is not in ALFA,
-         --  then the subprogram is not in ALFA.
+         --  The parameter is in ALFA if-and-only-if its type is in ALFA
 
-         if Nkind (Parent (First (T))) in N_Subprogram_Specification
-           and then not Is_In_ALFA (Formal_Type)
-         then
-            Set_Is_In_ALFA (Defining_Entity (Parent (First (T))), False);
+         if Is_In_ALFA (Formal_Type) then
+            Set_Is_In_ALFA (Formal);
+         else
+            Mark_Non_ALFA_Subprogram;
          end if;
 
          Default := Expression (Param_Spec);