GNAT-FSF-builds icon indicating copy to clipboard operation
GNAT-FSF-builds copied to clipboard

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

Open damaki opened this issue 2 years ago • 5 comments

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:

image

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%)

damaki avatar Jun 02 '22 11:06 damaki