[Ada] Issue warning on unused quantified expression
Commit Message
It is common that a quantified expression takes the form of a
conjunction or disjunction. In such a case, it is expected that all
conjuncts/ disjuncts reference the quantified variable. Not doing so can
be either the symptom of an error, or of a non-optimal expression, as
that sub-expression could be extracted from the quantified expression.
This is beneficial for both execution (speed) and for proof
(automation).
Issue a warning in such a case.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_ch4.adb (Analyze_QUantified_Expression): Issue warning on
conjunct/disjunct sub-expression of the full expression inside a
quantified expression, when it does not reference the quantified
variable.
@@ -4299,21 +4299,67 @@ package body Sem_Ch4 is
Loop_Id := Defining_Identifier (Loop_Parameter_Specification (N));
end if;
- if Warn_On_Suspicious_Contract
- and then not Referenced (Loop_Id, Cond)
- and then not Is_Internal_Name (Chars (Loop_Id))
- then
- -- Generating C, this check causes spurious warnings on inlined
- -- postconditions; we can safely disable it because this check
- -- was previously performed when analyzing the internally built
- -- postconditions procedure.
+ declare
+ type Subexpr_Kind is (Full, Conjunct, Disjunct);
- if Modify_Tree_For_C and then In_Inlined_Body then
- null;
- else
- Error_Msg_N ("?T?unused variable &", Loop_Id);
+ procedure Check_Subexpr (Expr : Node_Id; Kind : Subexpr_Kind);
+ -- Check that the quantified variable appears in every sub-expression
+ -- of the quantified expression. If Kind is Full, Expr is the full
+ -- expression. If Kind is Conjunct (resp. Disjunct), Expr is a
+ -- conjunct (resp. disjunct) of the full expression.
+
+ -------------------
+ -- Check_Subexpr --
+ -------------------
+
+ procedure Check_Subexpr (Expr : Node_Id; Kind : Subexpr_Kind) is
+ begin
+ if Nkind (Expr) in N_Op_And | N_And_Then
+ and then Kind /= Disjunct
+ then
+ Check_Subexpr (Left_Opnd (Expr), Conjunct);
+ Check_Subexpr (Right_Opnd (Expr), Conjunct);
+
+ elsif Nkind (Expr) in N_Op_Or | N_Or_Else
+ and then Kind /= Conjunct
+ then
+ Check_Subexpr (Left_Opnd (Expr), Disjunct);
+ Check_Subexpr (Right_Opnd (Expr), Disjunct);
+
+ elsif Kind /= Full
+ and then not Referenced (Loop_Id, Expr)
+ then
+ declare
+ Sub : constant String :=
+ (if Kind = Conjunct then "conjunct" else "disjunct");
+ begin
+ Error_Msg_NE
+ ("?T?unused variable & in " & Sub, Expr, Loop_Id);
+ Error_Msg_NE
+ ("\consider extracting " & Sub & " from quantified "
+ & "expression", Expr, Loop_Id);
+ end;
+ end if;
+ end Check_Subexpr;
+
+ begin
+ if Warn_On_Suspicious_Contract
+ and then not Is_Internal_Name (Chars (Loop_Id))
+
+ -- Generating C, this check causes spurious warnings on inlined
+ -- postconditions; we can safely disable it because this check
+ -- was previously performed when analyzing the internally built
+ -- postconditions procedure.
+
+ and then not (Modify_Tree_For_C and In_Inlined_Body)
+ then
+ if not Referenced (Loop_Id, Cond) then
+ Error_Msg_N ("?T?unused variable &", Loop_Id);
+ else
+ Check_Subexpr (Cond, Kind => Full);
+ end if;
end if;
- end if;
+ end;
-- Diagnose a possible misuse of the SOME existential quantifier. When
-- we have a quantified expression of the form: