Missing zlib1.dll for gnatprove-11.2.0-3 on Windows

[damaki]

With gnatprove-11.2.0-3 (obtained via Alire), the alt-ergo prover does not work on Windows 10 due to a missing zlib1.dll.

The following error appears when running gnatprove --version:

Here is the complete output of gnatprove --version:

0.0w
Why3 for gnatprove version 1.3.1+git
C:\Users\Dan\.config\alire\cache\dependencies\gnatprove_11.2.3_cd184fa0\libexec\spark\bin\alt-ergo.exe: C:\Users\Dan\.config\alire\cache\dependencies\gnatprove_11.2.3_cd184fa0\libexec\spark\bin\cvc4.exe: This is CVC4 version 1.8
compiled with GCC version 5.3.1 20160211
on Aug 25 2020 08:27:39

Copyright (c) 2009-2020 by the authors and their institutional
affiliations listed at http://cvc4.cs.stanford.edu/authors

CVC4 is open-source and is covered by the BSD license (modified).

THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.
USE AT YOUR OWN RISK.

CVC4 incorporates code from ANTLR3 (http://www.antlr.org).
See licenses/antlr3-LICENSE for copyright and licensing information.

This version of CVC4 is linked against the following non-(L)GPL'ed
third party libraries.

  SymFPU - The Symbolic Floating Point Unit
  See https://github.com/martin-cs/symfpu/tree/CVC4 for copyright information.

This version of CVC4 is linked against the following third party
libraries covered by the LGPLv3 license.
See licenses/lgpl-3.0.txt for more information.

  GMP - Gnu Multi Precision Arithmetic Library
  See http://gmplib.org for copyright information.

See the file COPYING (distributed with the source code, and with
all binaries) for the full CVC4 copyright, licensing, and (lack of)
warranty information.
C:\Users\Dan\.config\alire\cache\dependencies\gnatprove_11.2.3_cd184fa0\libexec\spark\bin\z3.exe: Z3 version 4.8.12 - 64 bit

When running gnatprove on a project, the error message does not appear but alt-ergo does not show up in the report. Here's an example summary report which shows that the CVC4, Trivial, and Z3 provers successfully proved some checks, but alt-ergo did not prove anything:

---------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total          Flow   CodePeer                                Provers   Justified    Unproved
---------------------------------------------------------------------------------------------------------------------------
Data Dependencies               899           899          .                                      .           .           .
Flow Dependencies               371           371          .                                      .           .           .
Initialization                 5053          4991          .                                      .          62           .
Non-Aliasing                    232           232          .                                      .           .           .
Run-time Checks               12318             .          .    12116 (CVC4 97%, Trivial 3%, Z3 0%)           .         202
Assertions                     1486             .          .     1453 (CVC4 93%, Trivial 5%, Z3 2%)           .          33
Functional Contracts           2183             .          .            2162 (CVC4 97%, Trivial 3%)           .          21
LSP Verification                  .             .          .                                      .           .           .
Termination                     114             .          .                             114 (CVC4)           .           .
Concurrency                       .             .          .                                      .           .           .
---------------------------------------------------------------------------------------------------------------------------
Total                         22656    6493 (29%)          .                            15845 (70%)     62 (0%)    256 (1%)

[Fabien-Chouteau]

Hi @damaki,

Thanks for the report, I will have a look and try to fix this for the next build.

[Fabien-Chouteau]

@damaki can you try again with this release https://github.com/alire-project/GNAT-FSF-builds/releases/tag/gnatprove-12.1.0-1 ?

Note that I can't reproduce this issue on my side.

[damaki]

I'm still able to reproduce this with gnatprove-12.1.0-1. I downloaded and unzipped it manually instead of using Alire, but the behaviour is the same as the original description when I run gnatprove --version.

I searched for zlib1.dll in the gnatprove-12.1.0-1 files, but I did not find any instance of it.

I should also note that I was able to get alt-ergo to work by copying a zlib1.dll from a previous GNAT Community installation, so the problem seems to be that zlib1.dll is simply missing from the gnatprove release.

Maybe you are not able to reproduce because that zlib1.dll is visible from another directory, via your system PATH?

[Fabien-Chouteau]

@damaki can you try again with: https://github.com/alire-project/GNAT-FSF-builds/releases/tag/gnatprove-12.1.0-1 ? (new builds)

[damaki]

That build works for me. I'm able to run gnatprove --version and alt-ergo directly without errors.