GNAT-FSF-builds
GNAT-FSF-builds copied to clipboard
Missing zlib1.dll for gnatprove-11.2.0-3 on Windows
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%)