This proves the functionality of Interfaces.C with GNATprove. Ada RM specifications are added as comments in the spec, next to the formalization of specifications as contracts.
As a side-effect of this proof, fix two errors in the 4 procedure
versions of To_Ada, which may raise a range check failure and an
overflow check failure.
GNATprove is run with switches --level=4 --timeout=120.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/i-c.adb: Add ghost code.
(C_Length_Ghost): New ghost functions to query the C length of a
string.
(To_Ada): Insert constant Count_Cst where needed to comply with
SPARK. Homogeneize code between variants for char, wchar_t,
char16_t and char32_t. Use char16_nul and char32_nul
systematically instead of their value. Fix the type of index To
to be Integer instead of Positive, to avoid a possible range
check failure on an empty Target. Insert an exit statement to
avoid a possible overflow failure when the last index in Target
is Natural'Last (possibly on a small string as well).
* libgnat/i-c.ads: Add contracts.
(C_Length_Ghost): New ghost functions to query the C length of a
string.
* libgnat/s-os_lib.adb: Remove pragma Compiler_Unit_Warning
causing a spurious error during compilation of GNAT, as this
pragma is not needed anymore now that we bootstrap (stage1) with
the base compiler runtime.
patch.diff.gz
Description: application/gzip
