4 Maintainer: CSC <sacerdot@cs.unibo.it>
5 Build-Depends: debhelper (>= 9), ocaml-best-compilers, ocaml-findlib
6 Standards-Version: 3.9.3
10 Depends: ${shlibs:Depends}, ${misc:Depends}
11 Description: CerCo's Trusted Annotating C Compiler
12 CerCo's Annotating C Compiler is a C compiler for the 8051 microprocessor.
13 It produces both an Intel HEX code memory representation and an instrumented
14 version of the source code. The instrumented source code is a copy of the
15 original source code augmented with additional instructions to keep track of
16 the exact number of clock cycles spent by the microprocessor to execute the
17 program basic blocks. Combined with CerCo's Frama-C Cost Plugin it allows to
18 certify exact parametric time and stack bounds for the source code.
19 Limitations: the source code must all be in one .c file and it must not
20 contain external calls.
21 This version of the compiler has been certified for preservation of the
22 inferred costs using the interactive theorem prover Matita.