[Pkg-ocaml-maint-commits] [frama-c] 14/20: Enhance package description

Mehdi Dogguy mehdi at moszumanska.debian.org
Wed Dec 21 10:15:22 UTC 2016


This is an automated email from the git hooks/post-receive script.

mehdi pushed a commit to branch master
in repository frama-c.

commit bc855963190d789235ad8d87ba6a6269e6a92889
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Thu Dec 8 11:30:28 2016 +0100

    Enhance package description
---
 debian/control | 58 ++++++++++++++++++++++++++++------------------------------
 1 file changed, 28 insertions(+), 30 deletions(-)

diff --git a/debian/control b/debian/control
index 7ff29d0..2453f7c 100644
--- a/debian/control
+++ b/debian/control
@@ -31,22 +31,21 @@ Depends:
  frama-c-base (= ${binary:Version}),
  graphviz,
  emacs | emacsen
-Description: Framework for source code analysis of software written in C
- Frama-C is a framework dedicated to the analysis of the source code
- of software written in C.
+Description: 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.
  .
- Frama-C gathers several static analysis techniques in a single
- collaborative framework. The collaborative approach of Frama-C allows
- static analyzers to build upon the results already computed by other
- analyzers in the framework. Thanks to this approach, Frama-C provides
- sophisticated tools, such as a slicer and dependency analysis.
- .
- It can be used to:
-   * Validate the source code formally
-   * Look for potential runtime errors
-   * Audit or review it
-   * Reverse engineer it to understand its structure
-   * Generate formal documentation
+ Thanks to this approach, Frama-C provides sophisticated tools, including:
+   * an analyzer based on abstract interpretation (Value 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);
+   * 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.
  .
  This package provides the graphical user interface of Frama-c and depends
  on frama-c-base.
@@ -61,22 +60,21 @@ Depends:
  gcc,
 Recommends:
  alt-ergo
-Description: Framework for C source code analysis (without gui)
- Frama-C is a framework dedicated to the analysis of the source code
- of software written in C.
- .
- Frama-C gathers several static analysis techniques in a single
- collaborative framework. The collaborative approach of Frama-C allows
- static analyzers to build upon the results already computed by other
- analyzers in the framework. Thanks to this approach, Frama-C provides
- sophisticated tools, such as a slicer and dependency analysis.
+Description: Platform dedicated to the analysis of source code written in C (without gui)
+ 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.
  .
- It can be used to:
-   * Validate the source code formally
-   * Look for potential runtime errors
-   * Audit or review it
-   * Reverse engineer it to understand its structure
-   * Generate formal documentation
+ Thanks to this approach, Frama-C provides sophisticated tools, including:
+   * an analyzer based on abstract interpretation (Value 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);
+   * 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.
  .
  This package provides the library of Frama-c which is useful to build
  plugins for Frama-c and the command-line tools.

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/frama-c.git



More information about the Pkg-ocaml-maint-commits mailing list