Unverified Commit 71d622c2 authored by Weijia Wang's avatar Weijia Wang Committed by GitHub
Browse files

gprbuild, gnatprove: configure for aarch64 (#394093)

parents 66917f1c 5f7505bb

pkgs/development/ada-modules/gnatprove/0002-mute-aarch64-warnings.patch

0 → 100644
+22 −0
Original line number Diff line number Diff line 
--- a/src/counterexamples/ce_parsing.adb	2025-03-14 21:48:15.657409808 +0100

+++ b/src/counterexamples/ce_parsing.adb	2025-03-14 22:04:32.114664704 +0100

@@ -975,6 +975,9 @@

                elsif Is_Extended_Precision_Floating_Point_Type (Ty) then

                   pragma Assert (Size (Exp) = 15);

                   pragma Assert (Size (Significand) = 63);

+                  pragma Warnings (Off, "assertion will fail at run time");

+                  pragma Warnings (Off,

+                      "types for unchecked conversion have different sizes");

                   declare

                      package P is new Parse_Conversion

                        (Interfaces.Unsigned_128, Long_Long_Float);

@@ -983,6 +986,9 @@

                   begin

                      return (Float_K, (Extended_K, F));

                   end;

+                  pragma Warnings (On,

+                      "types for unchecked conversion have different sizes");

+                  pragma Warnings (On, "assertion will fail at run time");

                else

                   raise Program_Error;

                end if;

pkgs/development/ada-modules/gnatprove/default.nix

+3 −0
Original line number Diff line number Diff line
@@ -56,6 +56,9 @@ let 
      patches = [

        # Disable Coq related targets which are missing in the fsf-14 branch

        ./0001-fix-install.patch



        # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54

        ./0002-mute-aarch64-warnings.patch

      ];

      commit_date = "2024-01-11";

    };

pkgs/development/ada-modules/gprbuild/nixpkgs-gnat.xml

+33 −0
Original line number Diff line number Diff line
@@ -53,4 +53,37 @@ 
      <grep regexp="[^\r\n]+"></grep>

    </target>

  </compiler_description>

  <configuration>

    <!-- aarch64-linux - native compiler. -->

    <targets>

      <target name="^aarch64-unknown-linux-gnu$" />

    </targets>

    <hosts>

      <host name="^aarch64-unknown-linux-gnu$" />

    </hosts>

    <config>

   for Archive_Builder  use ("ar", "cr");

   for Archive_Builder_Append_Option use ("q");

   for Archive_Indexer  use ("ranlib");

   for Archive_Suffix   use ".a";

    </config>

  </configuration>

  <configuration>

    <!-- aarch64-linux - native compiler. -->

    <targets>

      <target name="^aarch64-unknown-linux-gnu$" />

    </targets>

    <hosts>

      <host name="^aarch64-unknown-linux-gnu$" />

    </hosts>

    <config>

   for Object_Lister use ("nm", "-g");

   for Object_Lister_Matcher use " [TDRBSG] (.*)";



   package Linker is

      for Export_File_Format use "GNU";

      for Export_File_Switch use "-Wl,--version-script=";

   end Linker;

    </config>

  </configuration>

</gprconfig>