+2014-08-01 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_res.adb (Resolve_Call): Do not perform
+ GNATprove-specific inlining while within a generic.
+
+2014-08-01 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch4.adb (Analyze_Case_Expression): Handle properly a
+ case expression with incompatible alternatives, when the first
+ alternative is overloaded.
+
2014-08-01 Ed Schonberg <schonberg@adacore.com>
* sem_res.adb (Check_Parameterless_Call): Use Relocate_Node
Others_Present : Boolean;
-- Indicates if Others was present
+ Wrong_Alt : Node_Id;
+ -- For error reporting
+
-- Start of processing for Analyze_Case_Expression
begin
if No (Alt) then
Add_One_Interp (N, It.Typ, It.Typ);
+
+ else
+ Wrong_Alt := Alt;
end if;
Get_Next_Interp (I, It);
return;
end if;
+ if Etype (N) = Any_Type and then Present (Wrong_Alt) then
+ Error_Msg_N ("type incompatible with that of previous alternatives",
+ Expression (Wrong_Alt));
+ return;
+ end if;
+
-- If the case expression is a formal object of mode in out, then
-- treat it as having a nonstatic subtype by forcing use of the base
-- type (which has to get passed to Check_Case_Choices below). Also
Eval_Call (N);
Check_Elab_Call (N);
- -- In GNATprove mode, expansion is disabled, but we want to inline
- -- some subprograms to facilitate formal verification. Indirect calls,
- -- through a subprogram type, cannot be inlined. Inlining is only
- -- performed for calls for which SPARK_Mode is On.
+ -- In GNATprove mode, expansion is disabled, but we want to inline some
+ -- subprograms to facilitate formal verification. Indirect calls through
+ -- a subprogram type or within a generic cannot be inlined. Inlining is
+ -- performed only for calls subject to SPARK_Mode on.
if GNATprove_Mode
- and then Is_Overloadable (Nam)
and then SPARK_Mode = On
+ and then Is_Overloadable (Nam)
+ and then not Inside_A_Generic
then
-- Retrieve the body to inline from the ultimate alias of Nam, if
-- there is one, otherwise calls that should be inlined end up not