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;

Reply via email to