ObjMC - The Objective/MC compiler

1. Introduction

ObjMC is a compiler for the Objective/MC language, generating a DTMC PRISM model.

2. Usage

$ objmc [-d|-p|-s] FILE

where FILE is an Objective/MC source file.

Options

  • -d: enables debug mode. In "debug mode", all intermediate steps regarding the transformations of the Control Flow Graph are dumped into DOT files named "CFGRAPH*.dot".
  • -p: enables tracing mode for parser
  • -s: enables tracing mode for scanner

NOTE: the generated PRISM model is emitted on the standard output! Use a command like

$ objmc input.obm > output.prism

to redirect the output to the file "output.prism".

3. Compilation

ObjMC requires a C++14 compiler. It has been tested only on Ubuntu 15.10 (x86_64), using the following versions of tools/libraries:

  1. gcc (Ubuntu 5.2.1-22ubuntu2) 5.2.1 20151010
  2. Boost C++ Libraries 1.58
  3. flex 2.5.39
  4. bison (GNU Bison) 3.0.4

The source code can be compiled by executing the automake initialization script

$ ./autogen.sh

and by issuing:

$ ./configure && make

4. Drawing the Control Flow Graph

DOT files generated using the "-d" option can be drawn using Graphviz (http://www.graphviz.org). For example:

$ dot -Tsvg:svg:core CFGRAPH.dot > CFGRAPH.svg

5. Download

ObjMC version 0.12

6. Example models