Source: acc Section: devel Priority: optional Maintainer: CSC Build-Depends: debhelper (>= 9), ocaml-best-compilers, ocaml-findlib Standards-Version: 3.9.3 Package: acc Architecture: any Depends: ${shlibs:Depends}, ${misc:Depends} 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.