From 5e8c8e4457de992f8f7081f20aaf11778656d344 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 3 Aug 2011 15:14:04 +0000 Subject: sem_ch11.adb (Analyze_Raise_xxx_Error): do not mark such nodes as not in ALFA. 2011-08-03 Yannick Moy * 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 --- gcc/ada/ChangeLog | 14 ++++++++++++++ gcc/ada/sem_ch11.adb | 1 - gcc/ada/sem_ch4.adb | 25 ++++++++++++++++++++----- gcc/ada/sem_ch6.adb | 11 +++++------ 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 + + * 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 * 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); -- cgit v1.1