Use default switches for ping example

AdaCore · Nov 16, 2020 · 5208aca · 5208aca
1 parent 755ded5
commit 5208aca
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 10 deletions.
diff --git a/examples/apps/ping/ping.gpr b/examples/apps/ping/ping.gpr
@@ -1,3 +1,5 @@
+with "../../../defaults";
+
 project Ping is
 
    for Languages use ("RecordFlux", "Python", "Ada", "C");
@@ -18,6 +20,14 @@ project Ping is
       for Output_Dir use "generated";
    end Recordflux;
 
+   package Builder is
+      for Default_Switches ("Ada") use Defaults.Builder_Switches & Defaults.Compiler_Switches;
+   end Builder;
+
+   package Binder is
+      for Default_Switches ("Ada") use Defaults.Binder_Switches;
+   end Binder;
+
    package Prove is
       for Proof_Switches ("Ada") use (
          "-j0",

diff --git a/examples/apps/ping/src/basalt-strings_generic.adb b/examples/apps/ping/src/basalt-strings_generic.adb
@@ -68,10 +68,14 @@ is
       end if;
    end Image_Ranged;
 
+   pragma Warnings (Off, "condition can only be False if invalid values present");
+
    procedure Lemma_U64_Le16 (B : Base) with
      Ghost,
      Post => SI.Unsigned_64 (B) <= 16;
 
+   pragma Warnings (On, "condition can only be False if invalid values present");
+
    procedure Lemma_U64_Le16 (B : Base) is
    begin
       null;

diff --git a/examples/apps/ping/src/generic_socket.adb b/examples/apps/ping/src/generic_socket.adb
@@ -1,5 +1,4 @@
-with System;
-with RFLX;
+with Interfaces.C;
 
 package body Generic_Socket with
    SPARK_Mode,
@@ -37,7 +36,7 @@ is
          C_Perror ("C_Socket (PF_INET, SOCK_RAW, IPPROTO_ICMP)" & ASCII.NUL);
          return;
       end if;
-      FD_Out := C_Socket (PF_Inet, SOCK_RAW, IPPROTO_RAW);
+      FD_Out := C_Socket (PF_INET, SOCK_RAW, IPPROTO_RAW);
       if FD_Out < 0 then
          C_Perror ("C_Socket (PF_Inet, SOCK_RAW, IPPROTO_RAW)" & ASCII.NUL);
          return;
@@ -95,7 +94,7 @@ is
          Success := True;
          return;
       end if;
-      Result  := C_Send (Fd_Out, Destination, Buffer, IC.size_t (Buffer'Length));
+      Result  := C_Send (FD_Out, Destination, Buffer, IC.size_t (Buffer'Length));
       Success := Result >= IC.int (Buffer'Length);
       if not Success then
          C_Perror ("Error sending packet len: " & Buffer'Length'Img & ASCII.NUL);

diff --git a/examples/apps/ping/src/generic_socket.ads b/examples/apps/ping/src/generic_socket.ads
@@ -1,6 +1,3 @@
-private with Interfaces.C;
-with RFLX.IPv4;
-
 generic
    type Element_Type is (<>);
    type Index_Type is (<>);

diff --git a/examples/apps/ping/src/icmpv4.adb b/examples/apps/ping/src/icmpv4.adb
@@ -8,7 +8,6 @@ with RFLX.ICMP.Message;
 with RFLX.RFLX_Types;
 with Generic_Checksum;
 with Generic_Socket;
-with Ada.Text_IO;
 
 package body ICMPv4 with
    SPARK_Mode,
@@ -50,8 +49,6 @@ is
 
    procedure Ping (Addr : String)
    is
-      use type RFLX.RFLX_Builtin_Types.Length;
-      use type RFLX.RFLX_Builtin_Types.Bytes_Ptr;
       package Socket is new Generic_Socket (RFLX.RFLX_Builtin_Types.Byte,
                                             RFLX.RFLX_Builtin_Types.Index,
                                             RFLX.RFLX_Builtin_Types.Bytes,