commit 3a9d9a0e899811e57234c7a428754e851ec1a62c
author Nico Huber <nico.h@gmx.de> Wed Apr 01 20:50:10 2026 +0000
committer Nico Huber <nico.h@gmx.de> Fri Apr 03 09:24:12 2026 +0000
tree 72fdd7830dd3783a30d09975f9e530b7162da977
parent d8fae235d53c0376ab320c3d84a9b414bffe9d64

posix file: Explicitly disable SPARK_Mode for hw_file_map()

The GNAT compiler also checks some SPARK rules now and this function
has side-effects. Hence we have to hide it.

Change-Id: I4a113e3b9a34ba0a27e7902a3bd08533fd73fcda
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.sourcearcade.org/c/libhwbase/+/452
Reviewed-by: Angel Pons <th3fanbus@gmail.com>

ada/posix/hw-file.adb

diff --git a/ada/posix/hw-file.adb b/ada/posix/hw-file.adb
index dd9d7f3..9755d13 100644
--- a/ada/posix/hw-file.adb
+++ b/ada/posix/hw-file.adb
@@ -33,7 +33,9 @@
       off   : Word32;
       mode  : Word32;
       copy  : int)
-      return int;
+      return int
+   with
+      SPARK_Mode => Off;
    pragma Import (C, c_map, "hw_file_map");
 
    procedure Map