Odd Behaviour

Odd Behaviour

[Mark Wilson]

If I use,

   procedure SQLAllocHandle
     (Result          : out    SQLRETURN;
      HandleType      : in     SQL_HANDLE_TYPE;
      InputHandle     : in     SQLHANDLE;
      OutputHandlePtr : in out SQLHANDLE)
     with
       Import        => True,
       Convention    => C,
       External_Name => "SQLAllocHandle";
   pragma Import_Valued_Procedure (SQLAllocHandle);

then everything works as expected. However, if I add the following Pre and Post conditions (it's definitely not the Global or Depends)

   procedure SQLAllocHandle
     (Result          : out    SQLRETURN;
      HandleType      : in     SQL_HANDLE_TYPE;
      InputHandle     : in     SQLHANDLE;
      OutputHandlePtr : in out SQLHANDLE)
     with
       Import        => True,
       Convention    => C,
       External_Name => "SQLAllocHandle",
       Global        => null,
       Depends       => ((Result, OutputHandlePtr) =>
                           (HandleType, InputHandle, OutputHandlePtr)),
       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);

   pragma Import_Valued_Procedure (SQLAllocHandle);

then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]' If I ignore the error, using

 pragma Warnings (Off, "*convention Ada*");

 then it doesn't work at all, as one would expect, raising storage_error.

So, is it the case that, even if you suppress all checks, using an 'if' in a pre or post condition forces a import function stub to only be convention Ada? 

Re: Odd Behaviour

[Marius Amado-Alves]

To find the culprit I would:
Test Pre vs. Post (Pre only vs. Post only).
Unit test function SQL_OK for storage error just in case.

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 11:16:57 AM UTC, amado...@gmail.com wrote:
> To find the culprit I would: 
> Test Pre vs. Post (Pre only vs. Post only). 
> Unit test function SQL_OK for storage error just in case.

It's not SQL_OK,

   function SQL_OK
     (rc : in SQLRETURN)
      return Boolean
   is
     (rc = SQL_SUCCESS or else rc = SQL_SUCCESS_WITH_INFO);

And it fails with either Pre or Post, sadly - the only common problem seems to be the 'if' 

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 11:21:22 AM UTC, Mark Wilson wrote:
> On Tuesday, January 18, 2022 at 11:16:57 AM UTC, amado...@gmail.com wrote: 
> > To find the culprit I would: 
> > Test Pre vs. Post (Pre only vs. Post only). 
> > Unit test function SQL_OK for storage error just in case.
> It's not SQL_OK, 
> 
> function SQL_OK 
> (rc : in SQLRETURN) 
> return Boolean 
> is 
> (rc = SQL_SUCCESS or else rc = SQL_SUCCESS_WITH_INFO); 
> 
> And it fails with either Pre or Post, sadly - the only common factor seems to be the 'if' 

Does this look like a compiler bug? Or, hitherto, undocumented behaviour with Pre and Post conditions?

Re: Odd Behaviour

[Jeffrey R.Carter]

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

Re: Odd Behaviour

[Mark Wilson]

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.

Re: Odd Behaviour

[Jeffrey R.Carter]

On 2022-01-18 12:05, Mark Wilson wrote:
> 
> then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]'

The GNAT RM says of pragma Import_Valued_Procedure

"Note that it is important to use this pragma in conjunction with a separate 
pragma Import that specifies the desired convention, since otherwise the default 
convention is Ada, which is almost certainly not what is required."

What happens if you replace the import aspects with pragma Import?

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

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 11:48:23 AM UTC, Jeffrey R.Carter wrote:
> On 2022-01-18 12:05, Mark Wilson wrote: 
> >
> > then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]'
> The GNAT RM says of pragma Import_Valued_Procedure 
> 
> "Note that it is important to use this pragma in conjunction with a separate 
> pragma Import that specifies the desired convention, since otherwise the default 
> convention is Ada, which is almost certainly not what is required." 
> 
> What happens if you replace the import aspects with pragma Import?
> -- 
> Jeff Carter 
> "Monsieur Arthur King, who has the brain of a duck, you know." 
> Monty Python & the Holy Grail 
> 09

Tried pragma Import, and even pragma Convention, so, for instance,

   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, "SQLAllocHandle");
   pragma Import_Valued_Procedure (SQLAllocHandle);

Fails with the same warning. Take the 'pre' out and it works fine.

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 11:51:36 AM UTC, Mark Wilson wrote:
> On Tuesday, January 18, 2022 at 11:48:23 AM UTC, Jeffrey R.Carter wrote: 
> > On 2022-01-18 12:05, Mark Wilson wrote: 
> > > 
> > > then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]' 
> > The GNAT RM says of pragma Import_Valued_Procedure 
> > 
> > "Note that it is important to use this pragma in conjunction with a separate 
> > pragma Import that specifies the desired convention, since otherwise the default 
> > convention is Ada, which is almost certainly not what is required." 
> > 
> > What happens if you replace the import aspects with pragma Import? 
> > -- 
> > Jeff Carter 
> > "Monsieur Arthur King, who has the brain of a duck, you know." 
> > Monty Python & the Holy Grail 
> > 09
> Tried pragma Import, and even pragma Convention, so, for instance,
> 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, "SQLAllocHandle"); 
> pragma Import_Valued_Procedure (SQLAllocHandle); 
> 
> Fails with the same warning. Take the 'pre' out and it works fine.

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?

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 12:08:16 PM UTC, Mark Wilson wrote:
> On Tuesday, January 18, 2022 at 11:51:36 AM UTC, Mark Wilson wrote: 
> > On Tuesday, January 18, 2022 at 11:48:23 AM UTC, Jeffrey R.Carter wrote: 
> > > On 2022-01-18 12:05, Mark Wilson wrote: 
> > > > 
> > > > then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]' 
> > > The GNAT RM says of pragma Import_Valued_Procedure 
> > > 
> > > "Note that it is important to use this pragma in conjunction with a separate 
> > > pragma Import that specifies the desired convention, since otherwise the default 
> > > convention is Ada, which is almost certainly not what is required." 
> > > 
> > > What happens if you replace the import aspects with pragma Import? 
> > > -- 
> > > Jeff Carter 
> > > "Monsieur Arthur King, who has the brain of a duck, you know." 
> > > Monty Python & the Holy Grail 
> > > 09 
> > Tried pragma Import, and even pragma Convention, so, for instance, 
> > 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, "SQLAllocHandle"); 
> > pragma Import_Valued_Procedure (SQLAllocHandle); 
> > 
> > Fails with the same warning. Take the 'pre' out and it works fine.
> 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?

Well, this works - but feels very naughty,

   function SQLAllocHandle
     (HandleType      : in     SQL_HANDLE_TYPE;
      InputHandle     : in     SQLHANDLE;
      OutputHandlePtr : in SQLHANDLE)
     return SQLRETURN;
   --  with
   --    Pre =>   (Handletype = SQL_Handle_Env);
   
   pragma Import (C, SQLAllocHandle);
   pragma Import_Function
     (SQLAllocHandle, "SQLAllocHandle",
      (SQL_HANDLE_TYPE, SQLHANDLE, SQLHANDLE), SQLRETURN,
      (Value, Value, Reference));

However, adding the precondition in results in '<artificial>:(.text+0xb7): undefined reference to `sqlallochandle'''

Re: Odd Behaviour

[Jeffrey R.Carter]

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

Re: Odd Behaviour

[Mark Wilson]

On Tuesday, January 18, 2022 at 12:18:56 PM UTC, Mark Wilson wrote:
> On Tuesday, January 18, 2022 at 12:08:16 PM UTC, Mark Wilson wrote: 
> > On Tuesday, January 18, 2022 at 11:51:36 AM UTC, Mark Wilson wrote: 
> > > On Tuesday, January 18, 2022 at 11:48:23 AM UTC, Jeffrey R.Carter wrote: 
> > > > On 2022-01-18 12:05, Mark Wilson wrote: 
> > > > > 
> > > > > then an error is raised: 'warning: Valued_Procedure has no effect for convention Ada [enabled by default]' 
> > > > The GNAT RM says of pragma Import_Valued_Procedure 
> > > > 
> > > > "Note that it is important to use this pragma in conjunction with a separate 
> > > > pragma Import that specifies the desired convention, since otherwise the default 
> > > > convention is Ada, which is almost certainly not what is required." 
> > > > 
> > > > What happens if you replace the import aspects with pragma Import? 
> > > > -- 
> > > > Jeff Carter 
> > > > "Monsieur Arthur King, who has the brain of a duck, you know." 
> > > > Monty Python & the Holy Grail 
> > > > 09 
> > > Tried pragma Import, and even pragma Convention, so, for instance, 
> > > 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, "SQLAllocHandle"); 
> > > pragma Import_Valued_Procedure (SQLAllocHandle); 
> > > 
> > > Fails with the same warning. Take the 'pre' out and it works fine. 
> > 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?
> Well, this works - but feels very naughty, 
> 
> function SQLAllocHandle 
> (HandleType : in SQL_HANDLE_TYPE; 
> InputHandle : in SQLHANDLE; 
> OutputHandlePtr : in SQLHANDLE) 
> return SQLRETURN;
> -- with 
> -- Pre => (Handletype = SQL_Handle_Env); 
> 
> pragma Import (C, SQLAllocHandle);
> pragma Import_Function 
> (SQLAllocHandle, "SQLAllocHandle", 
> (SQL_HANDLE_TYPE, SQLHANDLE, SQLHANDLE), SQLRETURN, 
> (Value, Value, Reference)); 
> 
> However, adding the precondition in results in '<artificial>:(.text+0xb7): undefined reference to `sqlallochandle'''

This works!

   function SQLAllocHandle
     (HandleType      : in     SQL_HANDLE_TYPE;
      InputHandle     : in     SQLHANDLE;
      OutputHandlePtr : in SQLHANDLE)
     return SQLRETURN
   with
     Pre =>   (Handletype = SQL_Handle_Env);
   
   pragma Import (C, SQLAllocHandle, "SQLAllocHandle");
   
   pragma Import_Function
     (SQLAllocHandle, "SQLAllocHandle",
      (SQL_HANDLE_TYPE, SQLHANDLE, SQLHANDLE), SQLRETURN,
      (Value, Value, Reference));

(so specified the external function name in the Import as well as the Import_Function)

Even the writing to an 'in' parameter worked,

   Result := SQLAllocHandle
     (HandleType      => SQL_HANDLE_ENV,
      InputHandle     => SQL_NULL_HANDLE,
      OutputHandlePtr => SQLHANDLE (Handle));
   
   Put_Line (SQLRETURN'Image (Result));
   Put_Line (Boolean'Image (SQLHANDLE(Handle) /= SQL_NULL_HANDLE));

The first Put_Line returns SQL_SUCCESS, and the second returns TRUE

Ugly as hell, though. Spark complains,

odbc.ads:100:04: warning: pragma "IMPORT_FUNCTION" ignored (not yet supported)
odbc.ads:139:04: warning: pragma "IMPORT_VALUED_PROCEDURE" ignored (not yet supported),

and there's the horrible Ada warning that,

main.adb:10:04: warning: variable "Handle" is read but never assigned [-gnatwv]

I think it is going to be much cleaner (and clearer) to abstract this away to an Ada body.

Re: Odd Behaviour

[Mark Wilson]

> 
> 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.
> -- 

I think that has to be plan. 

I'll actually do it by specifying the 'raw' imports in an Ada spec, then import that into a Spark body keeping it clean and simple.

Re: Odd Behaviour

[Mark Wilson]

Just for completeness, this is what I end up doing

SPEC:

--------------------------------------------------------------------------------
   function SQL_OK
     (rc : in SQLRETURN)
      return Boolean
     with
       Global  => null,
       Depends => (SQL_OK'Result => (rc)),
       Post    => (SQL_OK'Result =
                     (rc = SQL_SUCCESS or rc = SQL_SUCCESS_WITH_INFO));
--------------------------------------------------------------------------------

   procedure SQLAllocEnv
     (hEnv   : in out SQLHENV;
      Result : out    SQLRETURN)
     with
       Inline,
       Global  => (Output => Environment),
       Depends => ((Result, hEnv, Environment) => (hEnv)),
       Pre     => (SQLHANDLE (hEnv) = SQL_NULL_HANDLE),
       Post    => (if SQL_OK (Result) then
                      SQLHANDLE(hEnv) /= SQL_NULL_HANDLE
                   else
                      SQLHANDLE(hEnv) = SQL_NULL_HANDLE);
   
--------------------------------------------------------------------------------

   procedure SQLAllocDbc
     (hEnv   : in     SQLHENV;
      hDbc   : in out SQLHDBC;
      Result : out    SQLRETURN)
     with
       Inline,
       Global  => (Input  => Environment,
                   Output => Database_Connection),
       Depends => ((Result, hDbc, Database_Connection) =>
                     (hEnv, hDbc, Environment)),
       Pre     => (SQLHANDLE (hEnv) /= SQL_NULL_HANDLE and
                   SQLHANDLE (hDbc) =  SQL_NULL_HANDLE),
       Post    => (if SQL_OK (Result) then
                      SQLHANDLE(hDbc) /= SQL_NULL_HANDLE
                   else
                      SQLHANDLE(hDbc) = SQL_NULL_HANDLE);
   
--------------------------------------------------------------------------------



BODY:

--------------------------------------------------------------------------------

   function SQLAllocHandle
     (HandleType      : in     SQL_HANDLE_TYPE;
      InputHandle     : in     SQLHANDLE;
      OutputHandlePtr : in out SQLHANDLE)
      return SQLRETURN
     with
       Import        => True,
       Convention    => C,
       External_Name => "SQLAllocHandle";
   
--------------------------------------------------------------------------------

   function SQL_OK
     (rc : in SQLRETURN)
      return Boolean
   is
     (rc = SQL_SUCCESS or rc = SQL_SUCCESS_WITH_INFO);
   
--------------------------------------------------------------------------------

   procedure SQLAllocEnv
     (hEnv   : in out SQLHENV;
      Result : out    SQLRETURN)
   is
   begin
      Result := SQLAllocHandle
        (HandleType      => SQL_HANDLE_ENV,
         InputHandle     => SQL_NULL_HANDLE,
         OutputHandlePtr => SQLHANDLE (hEnv));
   end SQLAllocEnv;
   
--------------------------------------------------------------------------------
     
   procedure SQLAllocDbc
     (hEnv   : in     SQLHENV;
      hDbc   : in out SQLHDBC;
      Result : out    SQLRETURN)
   is
   begin
      Result := SQLAllocHandle
        (HandleType      => SQL_HANDLE_DBC,
         InputHandle     => SQLHANDLE (hEnv),
         OutputHandlePtr => SQLHANDLE (hDbc));
   end SQLAllocDbc;
   
--------------------------------------------------------------------------------

Thanks for the help!