The purpose of this c2s tool is to provide code-to-code translations from
concurrent programs to sequential programs. We currently parse, print, and
translate Boogie code (with annotations denoting concurrent semantics), and
have partial (perhaps deprecated) support for Boolean programs as well.
To get going, simply build the sources..
./configure
make
make install
and run a demo, which parses simple Boogie program and prints it back out
c2s src/test/bpl/simple.bpl --print -
then look at the usage options
c2s
There are also ocmaldoc-generated API documentation if you like
make doc
which gets put into doc/index.html.
Contact the author, Michael Emmi.