X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=debian%2Fcontrol;fp=debian%2Fcontrol;h=232c10e15bb9a17f8e261d2a0aad7f0ec8a5693a;hb=cf6ad53d0fcff8064b55a3ec23e5701c557b7ce1;hp=d309dc128e749acb05c4495c14d42eac93811be8;hpb=96576b1a433721d49eb9052aae268ee04ab633a8;p=pkg-cerco%2Facc.git

diff --git a/debian/control b/debian/control
index d309dc1..232c10e 100644
--- a/debian/control
+++ b/debian/control
@@ -8,5 +8,13 @@ Standards-Version: 3.9.3
 Package: acc
 Architecture: any
 Depends: ${shlibs:Depends}, ${misc:Depends}
-Description: fill me
- fill me
+Description: CerCo's Annotating C Compiler
+ CerCo's Annotating C Compiler is a C compiler for the 8051 microprocessor.
+ It produces both an Intel HEX code memory representation and an instrumented
+ version of the source code. The instrumented source code is a copy of the
+ original source code augmented with additional instructions to keep track of
+ the exact number of clock cycles spent by the microprocessor to execute the
+ program basic blocks. Combined with CerCo's Frama-C Cost Plugin it allows to
+ certify exact parametric time and stack bounds for the source code.
+ Limitations: the source code must all be in one .c file and it must not
+ contain external calls.