From 6bc253c73874a2ecbb844dd04dedba48321d5a55 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 8 Jun 2020 22:13:10 +0200
Subject: [PATCH] [opam] update description format according to opam
preferences
---
Makefile | 2 +-
headers/header_spec.txt | 1 -
opam/descr | 15 ---------------
opam/opam | 15 +++++++++++++++
opam/url | 2 --
5 files changed, 16 insertions(+), 19 deletions(-)
delete mode 100644 opam/descr
delete mode 100644 opam/url
diff --git a/Makefile b/Makefile
index 17e1df72b14..d6d044aebe2 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 593ff2ec4ba..402d65335a9 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 64c5f6eb0a0..00000000000
--- 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 9b605e44636..dc97b4ee787 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 3244fe4676d..00000000000
--- a/opam/url
+++ /dev/null
@@ -1,2 +0,0 @@
-http: "http://frama-c.com/download/frama-c-Chlorine-20180501.tar.gz"
-checksum: "2d61aa200ded2dd360a8310c9a03ac50"
--
GitLab