diff --git a/Makefile b/Makefile index 17e1df72b14666417a70dd255a35c21dfc7f8a95..d6d044aebe2a88c183a3477078b4574087e5699d 100644 --- a/Makefile +++ b/Makefile @@ -311,7 +311,7 @@ DISTRIB_FILES:=\ bin/sed_get_make_major bin/sed_get_make_minor \ INSTALL.md README.md .make-clean \ .make-clean-stamp .force-reconfigure \ - opam/opam opam/descr \ + opam/opam \ # Test files to be included in the distribution (without header checking). # Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files. diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 593ff2ec4babcbe9806706009b5cb7f2621e32a4..402d65335a9b5ba5035e776a483ff14194759cd4 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -106,7 +106,6 @@ licenses/LGPLv2: .ignore licenses/LGPLv2.1: .ignore licenses/Q_MODIFIED_LICENSE: .ignore man/frama-c.1: CEA_LGPL -opam/descr: .ignore opam/opam: .ignore ptests/.gitignore: .ignore ptests/.merlin: .ignore diff --git a/opam/descr b/opam/descr deleted file mode 100644 index 64c5f6eb0a08982338443c999fd887cfe2b9ca11..0000000000000000000000000000000000000000 --- a/opam/descr +++ /dev/null @@ -1,15 +0,0 @@ -Platform dedicated to the analysis of source code written in C. - -Frama-C gathers several analysis techniques in a single collaborative -framework, based on analyzers (called "plug-ins") that can build upon the -results computed by other analyzers in the framework. -Thanks to this approach, Frama-C provides sophisticated tools, including: -- an analyzer based on abstract interpretation (Eva plug-in); -- a program proof framework based on weakest precondition calculus (WP plug-in); -- a program slicer (Slicing plug-in); -- a tool for verification of temporal (LTL) properties (Aoraï plug-in); -- a runtime verification tool (E-ACSL plug-in); -- several tools for code base exploration and dependency analysis - (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.). -These plug-ins communicate between each other via the Frama-C API -and via ACSL (ANSI/ISO C Specification Language) properties. diff --git a/opam/opam b/opam/opam index 9b605e446364306856d091ee5962932383269d85..dc97b4ee787cbdcb8bc5ac9c45c223ce217f2d48 100644 --- a/opam/opam +++ b/opam/opam @@ -1,6 +1,21 @@ opam-version: "2.0" name: "frama-c" synopsis: "Platform dedicated to the analysis of source code written in C" +description:""" +Frama-C gathers several analysis techniques in a single collaborative +framework, based on analyzers (called "plug-ins") that can build upon the +results computed by other analyzers in the framework. +Thanks to this approach, Frama-C provides sophisticated tools, including: +- an analyzer based on abstract interpretation (Eva plug-in); +- a program proof framework based on weakest precondition calculus (WP plug-in); +- a program slicer (Slicing plug-in); +- a tool for verification of temporal (LTL) properties (Aoraï plug-in); +- a runtime verification tool (E-ACSL plug-in); +- several tools for code base exploration and dependency analysis + (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.). +These plug-ins communicate between each other via the Frama-C API +and via ACSL (ANSI/ISO C Specification Language) properties. +""" version: "21.0-beta" maintainer: "francois.bobot@cea.fr" authors: [ diff --git a/opam/url b/opam/url deleted file mode 100644 index 3244fe4676d438649eb3e69b3b62dfc5926e8b2b..0000000000000000000000000000000000000000 --- a/opam/url +++ /dev/null @@ -1,2 +0,0 @@ -http: "http://frama-c.com/download/frama-c-Chlorine-20180501.tar.gz" -checksum: "2d61aa200ded2dd360a8310c9a03ac50"