package alt-ergo-plugin-ab-why3

  1. Overview
  2. Docs
An experimental Why3 frontend for Alt-Ergo

Install

Dune Dependency

Authors

Maintainers

Sources

alt-ergo-2.5.2.tbz
sha256=f460c17011f8f6c85e3b9023983b339cc11bc34252ae748e708211378d3f6895
sha512=cc4707f22596838dd242dc2e42b5d744dd0c44f5283c0a36074761d5b8c91e6f46fed2aebb5f6a96d50f94e5da2b74cd18447574668db255a19a6fb0cda9bbb7

LICENSE.md.html

Copyright

These software are distributed in the hope that they will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Please, do not use enclosed software until you have read and accepted the terms of the licensing below. The use of these software implies that you automatically agree with our terms and conditions. In case of doubt, please contact us to clarify licensing.

The resources are licensed as follows:

OCaml source files and Alt-Ergo preludes

Some of these files are Copyright (C) 2006-2013 --- CNRS - INRIA - Universite Paris Sud, and Copyright (C) 2013-2017 --- OCamlPro SAS. They are distributed under the terms of the Apache Software License version 2.0.

The other files that refer to a file 'License.OCamlPro' are Copyright (C) --- OCamlPro SAS. They are distributed under the terms of the license indicated in License.OCamlPro (with OCamlPro-Non-Commercial-License).

Note that some plugins may have different licenses. For instance the sources of the AB-Why3 plugin are governed by the GNU Lesser General Public License version 2.1, and are Copyright (C) 2010-2017 INRIA - CNRS - Paris-Sud University and Copyright (C) 2018 OCamlPro SAS (see the AB-Why3 README).

You may want to refer to the header of each file to know under which license it is distributed.

Binaries generated from the source files

The binaries (tools, plugins, ...) that are generated from the OCaml source files are Copyright (C) --- OCamlPro SAS. They are distributed under the terms of the license indicated in the file License.OCamlPro (with OCamlPro-Non-Commercial-License), except for the AB-Why3 plugin, which is distributed under the terms of the GNU Lesser General Public License version 2.1.

OCaml

Innovation. Community. Security.