| commit | 1f3825ef03c6e890afe536ddbd4877f1b2e757fe | [log] [tgz] |
|---|---|---|
| author | Nico Huber <nico.h@gmx.de> | Thu Dec 14 00:05:20 2023 +0100 |
| committer | Nico Huber <nico.h@gmx.de> | Thu Dec 14 00:08:59 2023 +0100 |
| tree | f36d87cea5a572470f29fa60889a82581c3d1c70 | |
| parent | 22173223f4d561746631bbe7099cd01293533e3f [diff] |
Disable SPARK_Mode for use of 'Address
diff --git a/src/filo-blockdev.adb b/src/filo-blockdev.adb index 5bb6732..44f79bd 100644 --- a/src/filo-blockdev.adb +++ b/src/filo-blockdev.adb
@@ -4,6 +4,8 @@ (Buffer : in out Buffer_Type; Offset : in Blockdev_Offset; Success : out Boolean) + with + SPARK_Mode => Off is use Interfaces.C;