Adjust to buildsystem changes

All components are technically 'SPARK' now.

Futhermore, disable proofs for now. Recent GNATprove versions issue many
warnings which should be sorted through and corrected. However, we
postpone this to a later date.

diff --git a/Makefile b/Makefile
index ac51fb1730ce2bb3838e994d6cf81da22f350010..37d186f8e7a8928bfa5fb970ef8cd4a8323caa44 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -2,4 +2,6 @@ COMPONENT = libxhcidbg
 
 COMPONENT_TARGETS = cspecs
 
-include ../library_ada.mk
+NO_PROOF = true
+
+include ../library_spark.mk

diff --git a/libxhcidbg.gpr b/libxhcidbg.gpr
index b3aba9e909c4013385339fd3d821ec1b76d1bde5..a948d36d7200a75794ed85138104943a3ad32015 100644 (file)
--- a/libxhcidbg.gpr
+++ b/libxhcidbg.gpr
@@ -22,8 +22,8 @@ library project Libxhcidbg extends "../library_spark" is
 
    for Languages use ("Ada");
    for Source_Dirs use ("generated", "src");
-   for Object_Dir use "obj";
-   for Library_Dir use "lib";
+   for Object_Dir use "obj/" & Library_Spark.Build_Mode;
+   for Library_Dir use "lib/" & Library_Spark.Build_Mode;
    for Library_Name use "xhcidbg";
    for Library_Kind use "static";
 

diff --git a/src/hw-dbc.adb b/src/hw-dbc.adb
index 566eff753274ce92a66c229786dbce4bd7e7b0c3..77937f39a59515bdd5952d85a9762386d792d908 100644 (file)
--- a/src/hw-dbc.adb
+++ b/src/hw-dbc.adb
@@ -28,6 +28,7 @@ with HW.DbC.TRBs;
 
 package body HW.DbC
 with
+   SPARK_Mode    => Off,
    Refined_State => (State => (Connected, Running,
                                DbC_Run_Deadline, DbC_Poll_Deadline,
                                DbC_Stat_Deadline, Events.State,

diff --git a/src/hw-dbc.ads b/src/hw-dbc.ads
index f0ec11bb987cd2b1188322730ea5862d1f39b448..ef54d253678f5b2600ce47c5b71caadf91af216d 100644 (file)
--- a/src/hw-dbc.ads
+++ b/src/hw-dbc.ads
@@ -22,6 +22,7 @@ pragma Elaborate_All (HW.MMIO_Range);
 
 package HW.DbC
 with
+   SPARK_Mode     => Off,
    Abstract_State => (State, (DMA with External)),
    Initializes    => State
 is