gcc/ada/libgnat/a-nbnbig.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --               ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST                --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --            Copyright (C) 2021-2024, Free Software Foundation, Inc.       --
  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 body is provided as a work-around for a GNAT compiler bug, as GNAT
  33 --  currently does not compile instantiations of the spec with imported ghost
  34 --  generics for packages Signed_Conversions and Unsigned_Conversions.
  35
  36 --  Ghost code in this unit is meant for analysis only, not for run-time
  37 --  checking. This is enforced by setting the assertion policy to Ignore.
  38
  39 pragma Assertion_Policy (Ghost => Ignore);
  40
  41 package body Ada.Numerics.Big_Numbers.Big_Integers_Ghost with
  42    SPARK_Mode => Off
  43 is
  44
  45    package body Signed_Conversions with
  46      SPARK_Mode => Off
  47    is
  48
  49       function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
  50       begin
  51          raise Program_Error;
  52          return (null record);
  53       end To_Big_Integer;
  54
  55       function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
  56       begin
  57          raise Program_Error;
  58          return 0;
  59       end From_Big_Integer;
  60
  61    end Signed_Conversions;
  62
  63    package body Unsigned_Conversions with
  64      SPARK_Mode => Off
  65    is
  66
  67       function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
  68       begin
  69          raise Program_Error;
  70          return (null record);
  71       end To_Big_Integer;
  72
  73       function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
  74       begin
  75          raise Program_Error;
  76          return 0;
  77       end From_Big_Integer;
  78
  79    end Unsigned_Conversions;
  80
  81 end Ada.Numerics.Big_Numbers.Big_Integers_Ghost;