gnatprove_11.2.3_f7ece6d3/share/examples/spark/spark_book/Chapter-07/main.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
with Interfaces.C;
with Console_IO;
with Messages;

procedure Main
  with
    SPARK_Mode,
    Global => (In_Out => Console_IO.IO_Subsystem) is

   Text : String := "Hello";
   Checksum : Interfaces.C.unsigned_short;
begin
   pragma Assert(Text'Length /= 0);  -- If Text'Length is zero, To_C propagates Constraint_Error.
   Checksum := Messages.Compute_Fletcher_Checksum(Interfaces.C.To_C(Text, False), Text'Length);
   Console_IO.Put_Line(Integer'Image(Integer(Checksum)));
end Main;