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
7

Interesting. But that generic subprogram is in the AdaCL base library and some of the code is 20 years old and not at all at the quality level of the new AdaCL_Serial library. This is why I check with --no-subprojects.

I’ll do have a look at it because I do want to improve the quality level of the base library.

When using Alire it is better to keep tests and proofs in separate nested crates, so that aunit and gnatprove do not leak into the published library crate. A prove crate then holds only dummy packages whose purpose is to drive GNATprove; the library under proof is a normal dependency of that crate.

GNATprove is started on the prove crate, so that crate is the root project. The library is a withed subproject.

  • With --no-subprojects, only the root project is analysed. That is just the dummy packages, so nothing useful is proved.
  • Without --no-subprojects, GNATprove walks the whole project tree: the library and every project the library itself withs. Proof therefore spills into the next level of dependencies as well.

What one actually wants is a single hop: prove the library that the prove crate depends on, but not that library’s own dependencies. GNATprove has no depth switch today; --no-subprojects is only on or off. A hypothetical --no-subprojects=1 would mean “analyse the root project and its direct subprojects, then stop.”

8

I also use dummy subcrates to contain my GNATprove dependencies, but you only need to use it to get the environment with GNATprove in it; you don’t need to use any dummy GPR file.

For example, in my libcrc library I have a subcrate under the proof/ directory to hide the dependency on GNATprove. When I want to run GNATprove I point it at my main GPR file in the directory above. So the command I would use is:

cd proof/
alr exec -- gnatprove -P ../libcrc.gpr -j0

So in your case, where you have a command like:

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

You can avoid -P1 and pass the path to the GPR file you’re interested in:

test_1: validation
	alr exec -- gnatprove -P ../path/to/project.gpr --no-subprojects --level=1 --mode=stone --verbose
	cat obj/validation/gnatprove/gnatprove.out
1 Like
9

Follow-up on the proof trouble.

The hang was not in adacl_serial. GNATprove was walking into the old AdaCL base — the crate that will become adacl_desktop. That crate is built for programmer convenience: unbounded strings, controlled types, smart pointers. As @ksson pointed out, the smart-pointer Deleter contract is exactly the sort of thing SPARK will choke on. You do not get more SPARK-unfriendly than a smart pointer.

For 8.0 the library will be split. adacl will be a small SPARK-gold core with no smart pointers and no desktop convenience layer. adacl_serial will depend only on that core. adacl_desktop will keep the old API for hosted applications and will no longer be on the proof path.

Thank you to everyone who looked — and especially to @ksson for putting the finger on the smart pointer.

1 Like