Precondition on protected entry

Precondition on protected entry

[Simon Wright]

I have this (Ravenscar, STM32F4) code:

   protected Timer_Handler
   with Interrupt_Priority => System.Interrupt_Priority'Last - 1
   is
      entry Wait
      with Pre => Running;
      procedure Start_Waiting (For_Interval : Duration)
      with Pre => For_Interval <= 0.010_000 and not Running;
      function Running return Boolean;
   private
      procedure Handler
      with
        Attach_Handler => Ada.Interrupts.Names.TIM8_TRG_COM_TIM14_Interrupt;
      Triggered : Boolean := False;
      Is_Running : Boolean := False;
   end Timer_Handler;

and GNAT GPL 2016 says

    19.    protected Timer_Handler
    20.    with Interrupt_Priority => System.Interrupt_Priority'Last - 1
    21.    is
    22.       entry Wait
    23.       with Pre => Running;
                          |
        >>> "Running" is undefined

Is this a compiler bug, or is there something in e.g. ARM 6.1.1 that
I've missed?

Re: Precondition on protected entry

[Dennis Lee Bieber]

On Tue, 11 Oct 2016 18:02:31 +0100, Simon Wright <simon@pushface.org>
declaimed the following:

>I have this (Ravenscar, STM32F4) code:
>
	<SNIP>
>      function Running return Boolean;
>   private
	<SNIP>
>Is this a compiler bug, or is there something in e.g. ARM 6.1.1 that
>I've missed?

	Just off the cuff -- does moving the declaration of the function to
before the preconditions change things?
-- 
	Wulfraed                 Dennis Lee Bieber         AF6VN
    wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

Re: Precondition on protected entry

[Simon Wright]

Dennis Lee Bieber <wlfraed@ix.netcom.com> writes:

> On Tue, 11 Oct 2016 18:02:31 +0100, Simon Wright <simon@pushface.org>
> declaimed the following:
>
>>I have this (Ravenscar, STM32F4) code:
>>
> 	<SNIP>
>>      function Running return Boolean;
>>   private
> 	<SNIP>
>>Is this a compiler bug, or is there something in e.g. ARM 6.1.1 that
>>I've missed?
>
> 	Just off the cuff -- does moving the declaration of the function
> to before the preconditions change things?

No, I thought that (note that the precondition of Start_Waiting also
calls the not-yet-declared function Running, and compiles OK).

Re: Precondition on protected entry

[Stephen Leake]

On Tuesday, October 11, 2016 at 3:29:47 PM UTC-5, Simon Wright wrote:
> I have this (Ravenscar, STM32F4) code:
> 

I modified it slightly to compile with Windows GNAT GPL 2016:

with Ada.Interrupts.Names;
with System;
package Timer_Handler is
   protected Timer_Handler
   with Interrupt_Priority => System.Interrupt_Priority'Last
   is
      entry Wait
      with Pre => Running;
      procedure Start_Waiting (For_Interval : Duration)
      with Pre => For_Interval <= 0.010_000 and not Running;
      function Running return Boolean;
   private
      procedure Handler
      with
        Attach_Handler => Ada.Interrupts.Names.SIGFPE;
      Triggered : Boolean := False;
      Is_Running : Boolean := False;
   end Timer_Handler;
end Timer_Handler;

package body Timer_Handler is

   protected body Timer_Handler is

      entry Wait
        when Standard.True
      is
      begin
         null;
      end Wait;

      procedure Start_Waiting
        (For_Interval : Duration)
      is
      begin
         null;
      end Start_Waiting;

      function Running return Boolean is
      begin
         return Is_Running;
      end Running;

      procedure Handler
      is
      begin
         null;
      end Handler;

   end Timer_Handler;

end Timer_Handler;
 
gnatmake timer_handler.adb

no errors.

So this looks like a problem with the cross target only?

Re: Precondition on protected entry

[Simon Wright]

Stephen Leake <stephen_leake@stephe-leake.org> writes:

> On Tuesday, October 11, 2016 at 3:29:47 PM UTC-5, Simon Wright wrote:
>> I have this (Ravenscar, STM32F4) code:
>> 
>
> I modified it slightly to compile with Windows GNAT GPL 2016:
[...]
> gnatmake timer_handler.adb
>
> no errors.
>
> So this looks like a problem with the cross target only?

Most likely pragma Profile (Ravenscar).

Will report the bug, thanks for the check.

Re: Precondition on protected entry

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> Stephen Leake <stephen_leake@stephe-leake.org> writes:
>
>> On Tuesday, October 11, 2016 at 3:29:47 PM UTC-5, Simon Wright wrote:
>>> I have this (Ravenscar, STM32F4) code:
>>> 
>>
>> I modified it slightly to compile with Windows GNAT GPL 2016:
> [...]
>> gnatmake timer_handler.adb
>>
>> no errors.
>>
>> So this looks like a problem with the cross target only?
>
> Most likely pragma Profile (Ravenscar).
>
> Will report the bug, thanks for the check.

I managed to forget this, and have just reported the problem.

It turns out that the problem shows up if assertions are enabled
(-gnata).

Re: Precondition on protected entry

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> I managed to forget this, and have just reported the problem.
>
> It turns out that the problem shows up if assertions are enabled
> (-gnata).

The bug has been fixed in FSF GCC 7.0.0 (still experimental) and, of
course, in AdaCore's current pro version; so expect the fix for this
very obscure problem in GNAT GPL 2017!