AdaCL.Serial is on Alire — and a call for SPARK eyes

Releases
, ,
1

I am pleased to announce that AdaCL.Serial has been accepted into the Alire index as crate adacl_serial (version 7.2.1).

It is a compact, SPARK-friendly companion to GNAT.Serial_Communications. The crate contains a single package, AdaCL.Serial_IO. A null-record derivation turns Serial_Port into a proper class, so the usual operations read as methods:

Port.Get, Port.Put_Line, Port.Expect, and so on.

What it offers:

  • conversion helpers between Stream_Element / Stream_Element_Array and Character / String;
  • the familiar Get / Put / Get_Line / Put_Line operations;
  • high-level Expect procedures that discard or capture skipped text until a given sequence arrives;
  • full SPARK contracts.

The intended use is console-style protocols on classic and modern retro calculators — SwissMicros DM-series, HP-IL emulators, and similar devices.

The package is proven to SPARK bronze. That is a deliberate, usable baseline: the contracts are there and bronze-level verification completes. I should like to take it further. At present GNATprove hangs when asked for a higher assurance level, rather than finishing with unproved VCs or a clean timeout. A prover should not hang; I suspect this is a known class of tool issue rather than a defect in the contracts themselves. If you have seen the same stall, know a workaround (proof switches, splits, ghost helpers, a different prover backend, a timeout that actually fires), or can spot what in AdaCL.Serial_IO triggers it, I would be very grateful for a note.

An application that uses the library is already in progress and will be released shortly — libraries are more convincing when something real sits on top of them. When that application is out I will also publish a short tutorial showing how the crate is used in practice.

Crate: https://alire.ada.dev/crates/adacl_serial
Depends on: adacl ^7.2
Licence: GPL-3.0-or-later
Project: https://adacl.sourceforge.net/
Repository: https://sourceforge.net/p/adacl/git/ci/develop/tree/

Martin Krischik

2 Likes
2

Hello, The link to the repository fails =>

"Looks like there’s a problem with this site.

The server at git.code.sf.net sent back an error: 404 Not Found"

I already tried copying and pasting directly, but it still fails.

1 Like
3

Try this one: https://sourceforge.net/p/adacl/git/ci/develop/tree/ - That is the main entry and then you can choose protocol as well.

But you could also us alr get adacl_serial :wink:

1 Like
4

Hello,

I can reproduce the hang, apparently if you remove the “-u ” from the gnatprove invocation, it passes. We will investigate this further.

1 Like
5

Thanks for looking into it but I don’t use -u - at least not knowingly. I use the following 4 command to test the various level:

test_1: validation
	alr exec -P1 -- gnatprove --no-subprojects --level=1 --mode=stone --verbose
	cat obj/validation/gnatprove/gnatprove.out

test_2: validation
	alr exec -P1 -- gnatprove --no-subprojects --level=2 --mode=bronze --verbose
	cat obj/validation/gnatprove/gnatprove.out

test_3: validation
	alr exec -P1 -- gnatprove --no-subprojects --level=3 --mode=silver --verbose
	cat obj/validation/gnatprove/gnatprove.out

test_4: validation
	alr exec -P1 -- gnatprove --no-subprojects --level=4 --mode=gold --verbose
	cat obj/validation/gnatprove/gnatprove.out

The test that is actually used by the Alire continues integration is than specified in “adacl_serial_prove.gpr”.

What I noticed is that you can’t specify a level with -no-subprojects. Which makes Alire compatible proves using a child crate a bit more cumbersome.

Regards

Martin

6

you can’t specify a level with -no-subprojects

What do you mean by that?

In any case, it’s strange as I could only ever reproduce it with -u or -U. Just to double check, you are using FSF 16?

The problematic pattern is likely the generic subprogram parameter with post:

  generic
     with procedure Deleter (X : in out Pointer) is <> with
        Post => X = null;

I suggest you remove this postcondition here

1 Like