Control and copyright added.

diff --git a/debian/control b/debian/control
index a915c9182cba32334e8aa6f93d747040f650c129..772cff93bb3db4bb1f248caa5fcbd93930461b1a 100644 (file)
--- a/debian/control
+++ b/debian/control
@@ -8,5 +8,15 @@ Standards-Version: 3.9.3
 Package: acc-trusted
 Architecture: any
 Depends: ${shlibs:Depends}, ${misc:Depends}
 Package: acc-trusted
 Architecture: any
 Depends: ${shlibs:Depends}, ${misc:Depends}

-Description: fill me
- fill me
+Description: CerCo's Trusted 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.
+ This version of the compiler has been certified for preservation of the
+ inferred costs using the interactive theorem prover Matita.

diff --git a/debian/copyright b/debian/copyright
index bbd36adb16721eaa7891df46d65c55e08d0999e4..68ea1f98b33b33ce10cf1b0d2e5a78f6609521d6 100644 (file)
--- a/debian/copyright
+++ b/debian/copyright
@@ -1 +1,6 @@
-fill me
+This software has been produced by the CerCo project: http://cerco.cs.unibo.it.
+
+Copyright © 2010-2013 CerCo consortium.
+The software is released under the terms of the GNU/GPL license.
+
+The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.