cao: CAO Compiler

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

CAO Compiler

[Skip to Readme]


Versions 0.1, 0.1.1, 0.1.1
Change log None available
Dependencies array, base (>=4 && <5), cmdargs, ConfigFile, containers, directory, dlist, filepath, language-c, mtl, pretty, process, yices [details]
License LicenseRef-GPL
Author Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
Maintainer Paulo Silva <>
Category Compiler, Cryptography, Language
Home page
Bug tracker
Uploaded by tfaoliveira at 2014-04-07T16:12:30Z


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for cao-0.1.1

[back to package description]
CAO Compiler

0. Dependencies
To build the CAO Compiler you need: 
 - happy 
 - alex
 - cabal package manager

We recommend the installation of the Haskell Platform which contains all the aforementioned dependencies: 

1. Build instructions
$ cabal configure
$ cabal build
$ cabal install

2. Run dependencies (optional)
To run the CAO Compiler you may need:
 - Yices SMT solver (version 1)

This SMT solver is used to check some more complex conditions when typechecking a CAO program. 
The compiler works without Yices but some conditions may not be verified. A warning is shown in these cases.

3. Backend library dependencies
To compile the generated code with the backend library you need:
 - NTL 
 - GMP (optional)

NTL is available from
GMP is available from

Information about how to compile NTL with GMP can be found here:

4. Run instructions
To see a description of all compiler options:
$ cao help

The basic compiler usage is:
$ cao comp [cao-file]

5. Example
In the 'example' directory you can find a CAO implementation of the SHA1 hash algorithm.
The Makefile provides an example of how a generated C program can be compiled and linked with the backend library.
You may have to adjust the script variable 'CAO_PATH' to the root directory of your installation.

Contact Information

Bugs/Suggestions please mail to:

Manuel Barbosa -
Paulo Silva    -


B�rbara Vieira -
David Castro   -
H�lder Pereira -
Manuel Barbosa -
Miguel Marques -
Nuno Rodrigues -
Paulo Silva    -
Tiago Oliveira -