From 4e23dd56955bf029d249445e93cf7f40a97672a2 Mon Sep 17 00:00:00 2001 From: Adrian-Ken Rueegsegger Date: Wed, 8 May 2019 14:58:48 +0200 Subject: [PATCH] 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. --- Makefile | 4 +++- libxhcidbg.gpr | 4 ++-- src/hw-dbc.adb | 1 + src/hw-dbc.ads | 1 + 4 files changed, 7 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index ac51fb1..37d186f 100644 --- 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 b3aba9e..a948d36 100644 --- 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 566eff7..77937f3 100644 --- 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 f0ec11b..ef54d25 100644 --- 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 -- 2.30.2