]> git.ipfire.org Git - thirdparty/gcc.git/blame - gcc/ada/libgnat/s-imgllli.ads
ada: Refactor the proof of the Value and Image runtime units
[thirdparty/gcc.git] / gcc / ada / libgnat / s-imgllli.ads
CommitLineData
cb7584a4
EB
1------------------------------------------------------------------------------
2-- --
3-- GNAT RUN-TIME COMPONENTS --
4-- --
5-- S Y S T E M . I M G _ L L L I --
6-- --
7-- S p e c --
8-- --
cccef051 9-- Copyright (C) 1992-2023, Free Software Foundation, Inc. --
cb7584a4
EB
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 routines for supporting the Image attribute for
33-- signed integer types larger than Long_Long_Integer, and also for conversion
34-- operations required in Text_IO.Integer_IO for such types.
35
91d68769
YM
36-- Preconditions in this unit are meant for analysis only, not for run-time
37-- checking, so that the expected exceptions are raised. This is enforced by
38-- setting the corresponding assertion policy to Ignore. Postconditions and
39-- contract cases should not be executed at runtime as well, in order not to
40-- slow down the execution of these functions.
41
42pragma Assertion_Policy (Pre => Ignore,
43 Post => Ignore,
44 Contract_Cases => Ignore,
45 Ghost => Ignore,
46 Subprogram_Variant => Ignore);
47
cb7584a4 48with System.Image_I;
91d68769 49with System.Unsigned_Types;
70bcf5c4
CD
50with System.Vs_LLLI;
51with System.Vs_LLLU;
91d68769
YM
52
53package System.Img_LLLI
54 with SPARK_Mode
55is
56 subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
cb7584a4 57
b3ae28dc 58 package Impl is new Image_I
70bcf5c4
CD
59 (Int => Long_Long_Long_Integer,
60 Uns => Long_Long_Long_Unsigned,
61 U_Spec => System.Vs_LLLU.Spec,
62 I_Spec => System.Vs_LLLI.Spec);
cb7584a4
EB
63
64 procedure Image_Long_Long_Long_Integer
65 (V : Long_Long_Long_Integer;
66 S : in out String;
67 P : out Natural)
68 renames Impl.Image_Integer;
69
70 procedure Set_Image_Long_Long_Long_Integer
71 (V : Long_Long_Long_Integer;
72 S : in out String;
73 P : in out Natural)
74 renames Impl.Set_Image_Integer;
75
76end System.Img_LLLI;