comparison gcc/ada/libgnat/a-tifiio.ads @ 145:1830386684a0

gcc-9.2.0
author anatofuz
date Thu, 13 Feb 2020 11:34:05 +0900
parents 04ced10e8804
children
comparison
equal deleted inserted replaced
131:84e7813d76e9 145:1830386684a0
30 Default_Exp : Field := 0; 30 Default_Exp : Field := 0;
31 31
32 procedure Get 32 procedure Get
33 (File : File_Type; 33 (File : File_Type;
34 Item : out Num; 34 Item : out Num;
35 Width : Field := 0); 35 Width : Field := 0)
36 with
37 Pre => Is_Open (File) and then Mode (File) = In_File,
38 Global => (In_Out => File_System);
36 39
37 procedure Get 40 procedure Get
38 (Item : out Num; 41 (Item : out Num;
39 Width : Field := 0); 42 Width : Field := 0)
43 with
44 Post =>
45 Line_Length'Old = Line_Length
46 and Page_Length'Old = Page_Length,
47 Global => (In_Out => File_System);
40 48
41 procedure Put 49 procedure Put
42 (File : File_Type; 50 (File : File_Type;
43 Item : Num; 51 Item : Num;
44 Fore : Field := Default_Fore; 52 Fore : Field := Default_Fore;
45 Aft : Field := Default_Aft; 53 Aft : Field := Default_Aft;
46 Exp : Field := Default_Exp); 54 Exp : Field := Default_Exp)
55 with
56 Pre => Is_Open (File) and then Mode (File) /= In_File,
57 Post =>
58 Line_Length (File)'Old = Line_Length (File)
59 and Page_Length (File)'Old = Page_Length (File),
60 Global => (In_Out => File_System);
47 61
48 procedure Put 62 procedure Put
49 (Item : Num; 63 (Item : Num;
50 Fore : Field := Default_Fore; 64 Fore : Field := Default_Fore;
51 Aft : Field := Default_Aft; 65 Aft : Field := Default_Aft;
52 Exp : Field := Default_Exp); 66 Exp : Field := Default_Exp)
67 with
68 Post =>
69 Line_Length'Old = Line_Length
70 and Page_Length'Old = Page_Length,
71 Global => (In_Out => File_System);
53 72
54 procedure Get 73 procedure Get
55 (From : String; 74 (From : String;
56 Item : out Num; 75 Item : out Num;
57 Last : out Positive); 76 Last : out Positive)
77 with
78 Global => null;
58 79
59 procedure Put 80 procedure Put
60 (To : out String; 81 (To : out String;
61 Item : Num; 82 Item : Num;
62 Aft : Field := Default_Aft; 83 Aft : Field := Default_Aft;
63 Exp : Field := Default_Exp); 84 Exp : Field := Default_Exp)
85 with
86 Global => null;
64 87
65 private 88 private
66 pragma Inline (Get); 89 pragma Inline (Get);
67 pragma Inline (Put); 90 pragma Inline (Put);
68 91