From 403951b7c27f6c178e008ca779405bf19d52350f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 30 Apr 2013 22:44:19 +0200 Subject: [PATCH] Control and copyright added. --- debian/control | 14 ++++++++++++-- debian/copyright | 7 ++++++- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/debian/control b/debian/control index a915c91..772cff9 100644 --- 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} -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 bbd36ad..68ea1f9 100644 --- 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. -- 2.39.2