]> git.ipfire.org Git - thirdparty/gcc.git/blame - gcc/ada/libgnat/s-valint.ads
ada: Refactor the proof of the Value and Image runtime units
[thirdparty/gcc.git] / gcc / ada / libgnat / s-valint.ads
CommitLineData
cacbc350
RK
1------------------------------------------------------------------------------
2-- --
3084fecd 3-- GNAT RUN-TIME COMPONENTS --
cacbc350
RK
4-- --
5-- S Y S T E M . V A L _ I N T --
6-- --
7-- S p e c --
8-- --
cccef051 9-- Copyright (C) 1992-2023, Free Software Foundation, Inc. --
cacbc350
RK
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- --
748086b7 13-- ware Foundation; either version 3, or (at your option) any later ver- --
cacbc350
RK
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 --
748086b7
JJ
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/>. --
cacbc350
RK
26-- --
27-- GNAT was originally developed by the GNAT team at New York University. --
71ff80dc 28-- Extensive contributions were provided by Ada Core Technologies Inc. --
cacbc350
RK
29-- --
30------------------------------------------------------------------------------
31
32-- This package contains routines for scanning signed Integer values for use
33-- in Text_IO.Integer_IO, and the Value attribute.
34
336ea8f2
CD
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
41pragma Assertion_Policy (Pre => Ignore,
42 Post => Ignore,
43 Contract_Cases => Ignore,
44 Ghost => Ignore,
45 Subprogram_Variant => Ignore);
46
cb7584a4
EB
47with System.Unsigned_Types;
48with System.Val_Uns;
49with System.Value_I;
70bcf5c4
CD
50with System.Vs_Int;
51with System.Vs_Uns;
cb7584a4 52
336ea8f2 53package System.Val_Int with SPARK_Mode is
ca305a84 54 pragma Preelaborate;
cacbc350 55
cb7584a4
EB
56 subtype Unsigned is Unsigned_Types.Unsigned;
57
336ea8f2 58 package Impl is new Value_I
b3ae28dc
CD
59 (Int => Integer,
60 Uns => Unsigned,
61 Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
70bcf5c4
CD
62 U_Spec => System.Vs_Uns.Spec,
63 Spec => System.Vs_Int.Spec);
cb7584a4 64
649b3efa 65 procedure Scan_Integer
9de61fcb 66 (Str : String;
d90e94c7 67 Ptr : not null access Integer;
649b3efa
CD
68 Max : Integer;
69 Res : out Integer)
cb7584a4 70 renames Impl.Scan_Integer;
cacbc350 71
cb7584a4
EB
72 function Value_Integer (Str : String) return Integer
73 renames Impl.Value_Integer;
cacbc350
RK
74
75end System.Val_Int;