[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