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?

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.

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'

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?

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

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.

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

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.

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?

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

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

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.

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

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!