https://gcc.gnu.org/bugzilla/show_bug.cgi?id=118052
Bug ID: 118052
Summary: gnatproves bugs, nothing more indicated.
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.
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;
