Source: acc-trusted
Section: devel
Priority: optional
Maintainer: CSC <sacerdot@cs.unibo.it>
Build-Depends: debhelper (>= 9), ocaml-best-compilers, ocaml-findlib
Standards-Version: 3.9.3

Package: acc-trusted
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}
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.