debian/control

   1 Source: acc
   2 Section: devel
   3 Priority: optional
   4 Maintainer: CSC <sacerdot@cs.unibo.it>
   5 Build-Depends: debhelper (>= 9), ocaml-best-compilers, ocaml-findlib
   6 Standards-Version: 3.9.3
   7
   8 Package: acc
   9 Architecture: any
  10 Depends: ${shlibs:Depends}, ${misc:Depends}
  11 Description: CerCo's 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.