diff mbox

[Ada] Extend ALFA marks to more types of nodes

Message ID 20110803151422.GA847@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 3, 2011, 3:14 p.m. UTC 
Follow-up of work on marking nodes as being in ALFA for formal verification.
Mark more nodes in ALFA when a reasonable translation exists for verification.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox

Patch

Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 177275)
+++ sem_ch4.adb	(working copy)
@@ -1520,11 +1520,23 @@ 
          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 @@ 
    --  Start of processing for Analyze_Membership_Op
 
    begin
-      Mark_Non_ALFA_Subprogram;
-
       Analyze_Expression (L);
 
       if No (R)
@@ -4375,8 +4385,6 @@ 
       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 @@ 
       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.
 
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 177284)
+++ sem_ch6.adb	(working copy)
@@ -8881,13 +8881,12 @@ 
 
          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);
Index: sem_ch11.adb
===================================================================
--- sem_ch11.adb	(revision 177275)
+++ sem_ch11.adb	(working copy)
@@ -602,7 +602,6 @@ 
    --  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