/usr/lib/spark/current/spark-ada-strings-maps-not_spark.ads is in spark 2012.0.deb-11build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 | -------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
-------------------------------------------------------------------------------
-- --
-- SPARK.Ada.Strings.Maps.Not_SPARK --
-- --
-- Description --
-- This package provides the features of Ada.Strings.Maps which are not --
-- compatible with SPARK. Please refer to the Ada LRM description of --
-- Ada.Strings.Maps for usage information. --
-- --
-------------------------------------------------------------------------------
with Ada.Strings.Maps;
package SPARK.Ada.Strings.Maps.Not_SPARK is
type Character_Ranges is new Standard.Ada.Strings.Maps.Character_Ranges;
function To_Set (Ranges : Character_Ranges) return Character_Set;
function To_Ranges (Set : Character_Set) return Character_Ranges;
function "<="
(Left : Character_Set;
Right : Character_Set) return Boolean
renames Is_Subset;
subtype Character_Sequence is String;
-- Alternative representation for a set of character values
function To_Sequence (Set : Character_Set) return Character_Sequence;
function To_Domain
(Map : Character_Mapping) return Character_Sequence;
function To_Range
(Map : Character_Mapping) return Character_Sequence;
type Character_Mapping_Function is
new Standard.Ada.Strings.Maps.Character_Mapping_Function;
------------------------------------------------
-- Conversion functions from SPARK.Ada to Ada --
------------------------------------------------
function To_Character_Set
(From : Character_Set)
return Standard.Ada.Strings.Maps.Character_Set;
function To_Character_Range
(From : Character_Range)
return Standard.Ada.Strings.Maps.Character_Range;
function To_Character_Mapping
(From : Character_Mapping)
return Standard.Ada.Strings.Maps.Character_Mapping;
end SPARK.Ada.Strings.Maps.Not_SPARK;
|