Re: Odd Behaviour

[Mark Wilson <markwilson@wilsonnet.technology>]

On Tuesday, January 18, 2022 at 11:28:41 AM UTC, Jeffrey R.Carter wrote:
> On 2022-01-18 12:05, Mark Wilson wrote: 
> > 
> > Pre => (if HandleType = SQL_HANDLE_ENV then 
> > InputHandle = SQL_NULL_HANDLE 
> > else 
> > InputHandle /= SQL_NULL_HANDLE), 
> > Post => (if SQL_OK (Result) then 
> > OutputHandlePtr /= SQL_NULL_HANDLE 
> > else 
> > OutputHandlePtr = SQL_NULL_HANDLE);
> What happens with 
> 
> Pre => (Handletype = SQL_Handle_Env) = (Inputhandle = SQL_Null_Handle) 
> 
> and 
> 
> Post => SQL_OK (Result) = (Outputhandleptr /= SQL_Null_Handle) 
> 
> which seem to be equivalent? 
> 
> -- 
> Jeff Carter 
> "Monsieur Arthur King, who has the brain of a duck, you know." 
> Monty Python & the Holy Grail 
> 09

It fails (same warning) with only,

 Pre =>   (Handletype = SQL_Handle_Env);

Guess you can't have Pre or Post with Valued_Procedures. A warning is suppressed that  mentions that these are supported, yet,

pragma Warnings (Off, "*not yet supported*");

But that warning is only issued on Spark Analysis, not on the main Ada compile.

Hrmph. No problem to abstract away - so not a show killer - ie hide an Ada stub in the body, and leave the Spark annotations in the spec so we won't need to use Valued_Procedures. Functions in Spark can't have in out parameters, of course.