Small reproducer: ‰ cat repro.sh #!/bin/sh mkdir dir1 dir2 cat > dir1/gfxinit.gpr << EOF with "libhw"; library project gfxinit is for Library_Name use "gfxinit"; end gfxinit; EOF cat > dir2/libhw.gpr << EOF library project libhw is for Library_Name use "hw"; end libhw; EOF cd dir1 gnatprove -Pgfxinit.gpr -aP=../dir2 ‰ ./repro.sh gnatprove: gfxinit.gpr:1:06: unknown project file: "libhw" Error while loading project file: gfxinit.gpr
Does this work with the adacore binary?
I haven't tested it, but another user told me it works fine for him apparently: > I use the binary spark-gpl-2017 with z3 (theorem prover) of my Linux distribution
I retested with spark-2018 getting the same error. If I run GPR_PROJECT_PATH=../dir2 gnatprove -aP /home/alfredo/dir2/ -P gfxinit.gpr I instead get gnatprove: gfxinit.gpr:2:17: attribute Library_Dir not declared gnatprove: libhw.gpr:1:17: attribute Library_Dir not declared Phase 1 of 2: generation of Global contracts ... gfxinit.gpr:2:17: attribute Library_Dir not declared libhw.gpr:1:17: attribute Library_Dir not declared gprbuild: "gfxinit.gpr" processing failed gnatprove: error during generation of Global contracts Adding the Library_Dir declaration I finally get: gnatprove -aP /home/alfredo/dir2/ -P gfxinit.gpr Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... warning: no bodies have been analyzed by GNATprove enable analysis of a body using SPARK_Mode So it is only a misleading error message
No. -aP does not work :( I had GPR_PROJECT_PATH in the environment
Raised an issue upstream https://github.com/AdaCore/spark2014/issues/4
I'm assuming this is fixed in spark-2021 given the upstream bug is closed (admittedly with them unable to repro anymore).
