AdaCore-led effort brings a practical approach to verifying FACE® conformance for Ada Software.

A major milestone for Ada and the FACE community was reached this past Autumn when the FACE Consortium formally approved a proposed approach to FACE conformance verification for Ada software. Performed under the auspices of the Operating Systems Subcommittee of the FACE Consortium’s Technical Working Group, this effort was led by AdaCore’s FACE team comprising Ben Brosgol, Dudrey Smith, Michael Frank, and Dana Binkley.

Conformance verification for Ada has previously been a problem since the FACE conformance process is designed to enforce source-code portability through link-time tests against standard stubbed run-time libraries. Such an approach works well for C and C++,  but Ada code is portable not simply by invoking standard APIs but also through standard syntax whose object code calls functions in a compiler-specific runtime.

The new solution works within and extends the current FACE approach by defining a mechanism for incorporating an Ada toolchain with a compiler-specific runtime in the Conformance Test Suite, and determining whether it enforces the restrictions imposed by the FACE Technical Standard. If the Ada toolchain with its stubbed compiler-specific runtime does not detect a violation, then the developer of the Ada software component will need to furnish inspection evidence to demonstrate that the prohibited feature is not used. AdaCore’s Static Analysis Suite, in particular the GNATcheck tool with FACE-specific rules, can help customers construct such evidence.

The details of the Ada conformance procedures can be found in a paper, authored by AdaCore’s FACE team, which was published in the proceedings of the 2024 FACE/SOSA Technical Interchange Meeting.

By helping to provide an official approach to FACE conformance verification for Ada—both Ada 95 and Ada 2012—AdaCore has continued its mission of making Ada a “first-class citizen” in the FACE community. Next on the agenda is to define a practical process for conformance verification when the software component comprises both Ada and C code. Work is in progress on a solution.