https://gcc.gnu.org/bugzilla/show_bug.cgi?id=118051
Bug ID: 118051 Summary: gnatprove indicates error Product: gcc Version: 14.2.0 Status: UNCONFIRMED Severity: normal Priority: P3 Component: ada Assignee: unassigned at gcc dot gnu.org Reporter: 00120260a at gmail dot com CC: dkm at gcc dot gnu.org Target Milestone: --- +===========================GNAT BUG DETECTED==============================+ | 1.0 (spark) GCC error: | | File /home/drm/Documents/Administration/Ada/books/sourcecode ~ | | Building High Integrity Applications with SPARK/chapter07/build/gnatprove/messages_wrapper__compute_fletcher_checksum.mlw, marked by (* ERROR: *)(...): This expression has type int, but is expected to have type bv.BV16.t. | | No source file position information available | | Compiling /home/drm/Documents/Administration/Ada/books/sourcecode ~ Building High Integrity Applications with SPARK/chapter07/messages_wrapper.ads| | Please submit a bug report; see https://gcc.gnu.org/bugs/ . | | Use a subject line meaningful to you and us to track the bug. | | Include the entire contents of this bug box in the report. | | Include the exact command that you entered. | | Also include sources listed below. | +==========================================================================+ Code is the following. I do not know what causes it. it compiles well, but gnatprove produces the bug. I assume this is the place to bring that up. pragma SPARK_Mode(On); pragma Ada_2022; with Interfaces.C; package Messages_Wrapper is type Checksum_Type is mod 2**16; function Compute_Checksum (Data : in String) return Checksum_Type with Pre => Data'Length /= 0; private use Interfaces.C; -- needed for visibility in precondition function Compute_Fletcher_Checksum (Buffer : in char_array; Size : in size_t) return unsigned_short with Global => null, Import => True, Convention => C, Pre => Size = Buffer'Length and Buffer'Length in unsigned_short, External_Name => "compute_fletcher_checksum"; function Compute_Checksum (Data : in String) return Checksum_Type is ((declare Buffer: constant Interfaces.C.Char_array := Interfaces.C.To_C (Item => Data, Append_Nul => False); begin Checksum_Type(Compute_Fletcher_Checksum (Buffer, Buffer'Length)))); end Messages_Wrapper;