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 <m...@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.
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
