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