Adjust to buildsystem changes
authorAdrian-Ken Rueegsegger <ken@codelabs.ch>
Wed, 8 May 2019 12:58:48 +0000 (14:58 +0200)
committerReto Buerki <reet@codelabs.ch>
Thu, 9 May 2019 13:06:40 +0000 (15:06 +0200)
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.

Makefile
libxhcidbg.gpr
src/hw-dbc.adb
src/hw-dbc.ads

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
index b3aba9e909c4013385339fd3d821ec1b76d1bde5..a948d36d7200a75794ed85138104943a3ad32015 100644 (file)
@@ -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";
 
index 566eff753274ce92a66c229786dbce4bd7e7b0c3..77937f39a59515bdd5952d85a9762386d792d908 100644 (file)
@@ -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,
index f0ec11bb987cd2b1188322730ea5862d1f39b448..ef54d253678f5b2600ce47c5b71caadf91af216d 100644 (file)
@@ -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