Re: Odd Behaviour

["Jeffrey R.Carter" <spam.jrcarter.not@spam.acm.org.not>]

On 2022-01-18 13:08, Mark Wilson wrote:
> 
> Even tried (which to be fair is a bit of a long shot),
> 
>     procedure SQLAllocHandle
>       (Result          : out    SQLRETURN;
>        HandleType      : in     SQL_HANDLE_TYPE;
>        InputHandle     : in     SQLHANDLE;
>        OutputHandlePtr : in out SQLHANDLE);
>     --  with
>     --    Pre =>   (Handletype = SQL_Handle_Env);
>     
> 
>     pragma Import (C, SQLAllocHandle);
>     pragma Import_Valued_Procedure
>       (SQLAllocHandle, "SQLAllocHandle",
>        (SQLRETURN, SQL_HANDLE_TYPE, SQLHANDLE, SQLHANDLE),
>        (Reference, Value,           Value,     Reference));
> 
> Do you think I should file a bug report?

Import_Valued_Procedure is GNAT-specific, so it can do whatever they like, but 
presumably this is unintended behavior and you should report it.

You should be able to work around this by making your procedure a wrapper around 
an imported function with an in out parameter, with SPARK checking turned off in 
the procedure body.

-- 
Jeff Carter
"Monsieur Arthur King, who has the brain of a duck, you know."
Monty Python & the Holy Grail
09