gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-02/bad_types.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
with Ada.Float_Text_IO;
procedure Bad_Types with
  Annotate => (GNATprove, Might_Not_Return)
is
   Room_Length    : Float;   -- length of room in feet
   Wall_Thickness : Float;   -- thickness of wall in inches
   Total          : Float;   -- in feet
begin
   Ada.Float_Text_IO.Get (Room_Length);
   Ada.Float_Text_IO.Get (Wall_Thickness);
   Total := Room_Length + 2.0 * Wall_Thickness;
   Ada.Float_Text_IO.Put (Item => Total, Fore => 1, Aft  => 2, Exp  => 0);
end Bad_Types;