--- a/gcc/ada/libgnat/a-tienio.ads	Thu Oct 25 07:37:49 2018 +0900
+++ b/gcc/ada/libgnat/a-tienio.ads	Thu Feb 13 11:34:05 2020 +0900
@@ -28,28 +28,49 @@
    Default_Width : Field := 0;
    Default_Setting : Type_Set := Upper_Case;
 
-   procedure Get (File : File_Type; Item : out Enum);
-   procedure Get (Item : out Enum);
+   procedure Get (File : File_Type; Item : out Enum) with
+     Pre    => Is_Open (File) and then Mode (File) = In_File,
+     Global => (In_Out => File_System);
+   procedure Get (Item : out Enum) with
+     Post   =>
+       Line_Length'Old = Line_Length
+       and Page_Length'Old = Page_Length,
+     Global => (In_Out => File_System);
 
    procedure Put
      (File  : File_Type;
       Item  : Enum;
       Width : Field := Default_Width;
-      Set   : Type_Set := Default_Setting);
+      Set   : Type_Set := Default_Setting)
+   with
+     Pre    => Is_Open (File) and then Mode (File) /= In_File,
+     Post   =>
+       Line_Length (File)'Old = Line_Length (File)
+       and Page_Length (File)'Old = Page_Length (File),
+     Global => (In_Out => File_System);
 
    procedure Put
      (Item  : Enum;
       Width : Field := Default_Width;
-      Set   : Type_Set := Default_Setting);
+      Set   : Type_Set := Default_Setting)
+   with
+     Post   =>
+       Line_Length'Old = Line_Length
+       and Page_Length'Old = Page_Length,
+     Global => (In_Out => File_System);
 
    procedure Get
      (From : String;
       Item : out Enum;
-      Last : out Positive);
+      Last : out Positive)
+   with
+     Global => null;
 
    procedure Put
      (To   : out String;
       Item : Enum;
-      Set  : Type_Set := Default_Setting);
+      Set  : Type_Set := Default_Setting)
+   with
+     Global => null;
 
 end Ada.Text_IO.Enumeration_IO;