]>
Commit | Line | Data |
---|---|---|
b3ae28dc CD |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- S Y S T E M . V A L U E _ I _ S P E C -- | |
6 | -- -- | |
7 | -- S p e c -- | |
8 | -- -- | |
cccef051 | 9 | -- Copyright (C) 2022-2023, Free Software Foundation, Inc. -- |
b3ae28dc CD |
10 | -- -- |
11 | -- GNAT is free software; you can redistribute it and/or modify it under -- | |
12 | -- terms of the GNU General Public License as published by the Free Soft- -- | |
13 | -- ware Foundation; either version 3, or (at your option) any later ver- -- | |
14 | -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- | |
15 | -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- | |
16 | -- or FITNESS FOR A PARTICULAR PURPOSE. -- | |
17 | -- -- | |
18 | -- As a special exception under Section 7 of GPL version 3, you are granted -- | |
19 | -- additional permissions described in the GCC Runtime Library Exception, -- | |
20 | -- version 3.1, as published by the Free Software Foundation. -- | |
21 | -- -- | |
22 | -- You should have received a copy of the GNU General Public License and -- | |
23 | -- a copy of the GCC Runtime Library Exception along with this program; -- | |
24 | -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- | |
25 | -- <http://www.gnu.org/licenses/>. -- | |
26 | -- -- | |
27 | -- GNAT was originally developed by the GNAT team at New York University. -- | |
28 | -- Extensive contributions were provided by Ada Core Technologies Inc. -- | |
29 | -- -- | |
30 | ------------------------------------------------------------------------------ | |
31 | ||
32 | -- This package contains the specification entities using for the formal | |
33 | -- verification of the routines for scanning signed integer values. | |
34 | ||
35 | -- Preconditions in this unit are meant for analysis only, not for run-time | |
36 | -- checking, so that the expected exceptions are raised. This is enforced by | |
37 | -- setting the corresponding assertion policy to Ignore. Postconditions and | |
38 | -- contract cases should not be executed at runtime as well, in order not to | |
39 | -- slow down the execution of these functions. | |
40 | ||
41 | pragma Assertion_Policy (Pre => Ignore, | |
42 | Post => Ignore, | |
43 | Contract_Cases => Ignore, | |
44 | Ghost => Ignore, | |
45 | Subprogram_Variant => Ignore); | |
46 | ||
70bcf5c4 CD |
47 | with System.Value_U_Spec; |
48 | with System.Val_Spec; use System.Val_Spec; | |
b3ae28dc CD |
49 | |
50 | generic | |
51 | ||
52 | type Int is range <>; | |
53 | ||
54 | type Uns is mod <>; | |
55 | ||
70bcf5c4 | 56 | -- Additional parameters for ghost subprograms used inside contracts |
b3ae28dc | 57 | |
70bcf5c4 | 58 | with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; |
b3ae28dc CD |
59 | |
60 | package System.Value_I_Spec with | |
61 | Ghost, | |
62 | SPARK_Mode, | |
b1c3d016 | 63 | Always_Terminates |
b3ae28dc CD |
64 | is |
65 | pragma Preelaborate; | |
70bcf5c4 | 66 | use all type U_Spec.Uns_Option; |
b3ae28dc CD |
67 | |
68 | function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is | |
69 | (if Minus then Uval <= Uns (Int'Last) + 1 | |
70 | else Uval <= Uns (Int'Last)) | |
71 | with Post => True; | |
72 | -- Return True if Uval (or -Uval when Minus is True) is a valid number of | |
73 | -- type Int. | |
74 | ||
75 | function Is_Int_Of_Uns | |
76 | (Minus : Boolean; | |
77 | Uval : Uns; | |
78 | Val : Int) | |
79 | return Boolean | |
80 | is | |
81 | (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First | |
82 | elsif Minus then Val = -(Int (Uval)) | |
83 | else Val = Int (Uval)) | |
84 | with | |
85 | Pre => Uns_Is_Valid_Int (Minus, Uval), | |
86 | Post => True; | |
87 | -- Return True if Uval (or -Uval when Minus is True) is equal to Val | |
88 | ||
89 | function Abs_Uns_Of_Int (Val : Int) return Uns is | |
90 | (if Val = Int'First then Uns (Int'Last) + 1 | |
91 | elsif Val < 0 then Uns (-Val) | |
92 | else Uns (Val)); | |
93 | -- Return the unsigned absolute value of Val | |
94 | ||
95 | function Slide_To_1 (Str : String) return String | |
96 | with | |
97 | Post => | |
98 | Only_Space_Ghost (Str, Str'First, Str'Last) = | |
99 | (for all J in Str'First .. Str'Last => | |
100 | Slide_To_1'Result (J - Str'First + 1) = ' '); | |
101 | -- Slides Str so that it starts at 1 | |
102 | ||
103 | function Slide_If_Necessary (Str : String) return String is | |
104 | (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str); | |
105 | -- If Str'Last = Positive'Last then slides Str so that it starts at 1 | |
106 | ||
107 | function Is_Integer_Ghost (Str : String) return Boolean is | |
108 | (declare | |
109 | Non_Blank : constant Positive := First_Non_Space_Ghost | |
110 | (Str, Str'First, Str'Last); | |
111 | Fst_Num : constant Positive := | |
112 | (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); | |
113 | begin | |
70bcf5c4 CD |
114 | U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) |
115 | and then U_Spec.Raw_Unsigned_No_Overflow_Ghost | |
b3ae28dc CD |
116 | (Str, Fst_Num, Str'Last) |
117 | and then | |
118 | Uns_Is_Valid_Int | |
119 | (Minus => Str (Non_Blank) = '-', | |
70bcf5c4 | 120 | Uval => U_Spec.Scan_Raw_Unsigned_Ghost |
b3ae28dc CD |
121 | (Str, Fst_Num, Str'Last)) |
122 | and then Only_Space_Ghost | |
70bcf5c4 | 123 | (Str, U_Spec.Raw_Unsigned_Last_Ghost |
b3ae28dc CD |
124 | (Str, Fst_Num, Str'Last), Str'Last)) |
125 | with | |
126 | Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) | |
127 | and then Str'Last /= Positive'Last, | |
128 | Post => True; | |
129 | -- Ghost function that determines if Str has the correct format for a | |
130 | -- signed number, consisting in some blank characters, an optional | |
131 | -- sign, a raw unsigned number which does not overflow and then some | |
132 | -- more blank characters. | |
133 | ||
134 | function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is | |
135 | (declare | |
136 | Non_Blank : constant Positive := First_Non_Space_Ghost | |
137 | (Str, Str'First, Str'Last); | |
138 | Fst_Num : constant Positive := | |
139 | (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); | |
140 | Uval : constant Uns := | |
70bcf5c4 | 141 | U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); |
b3ae28dc CD |
142 | begin |
143 | Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', | |
144 | Uval => Uval, | |
145 | Val => Val)) | |
146 | with | |
147 | Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) | |
148 | and then Str'Last /= Positive'Last | |
149 | and then Is_Integer_Ghost (Str), | |
150 | Post => True; | |
151 | -- Ghost function that returns True if Val is the value corresponding to | |
152 | -- the signed number represented by Str. | |
153 | ||
154 | procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) | |
155 | with | |
156 | Ghost, | |
157 | Pre => Str'Last /= Positive'Last | |
158 | and then Str'Length >= 2 | |
159 | and then Str (Str'First) in ' ' | '-' | |
160 | and then (Str (Str'First) = '-') = (Val < 0) | |
70bcf5c4 CD |
161 | and then U_Spec.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) |
162 | and then U_Spec.Scan_Based_Number_Ghost | |
b3ae28dc | 163 | (Str, Str'First + 1, Str'Last) |
70bcf5c4 | 164 | = U_Spec.Wrap_Option (Abs_Uns_Of_Int (Val)), |
b3ae28dc CD |
165 | Post => Is_Integer_Ghost (Slide_If_Necessary (Str)) |
166 | and then Is_Value_Integer_Ghost (Str, Val); | |
167 | -- Ghost lemma used in the proof of 'Image implementation, to prove that | |
168 | -- the result of Value_Integer on a decimal string is the same as the | |
169 | -- signing the result of Scan_Based_Number_Ghost. | |
170 | ||
b3ae28dc CD |
171 | private |
172 | ||
173 | ---------------- | |
174 | -- Slide_To_1 -- | |
175 | ---------------- | |
176 | ||
177 | function Slide_To_1 (Str : String) return String is | |
178 | (declare | |
179 | Res : constant String (1 .. Str'Length) := Str; | |
180 | begin | |
181 | Res); | |
182 | ||
183 | end System.Value_I_Spec; |