Tuesday, 1 December 2009

Having trouble getting the Murphi verifier to compile?

I've spent quite a bit of time today getting the Murphi verification tool to compile. I thought I'd write down how I did it in case this is of use to others.

First, I found that the version here did not compile due to flex/yacc errors. I don't know how to solve these, but luckily the version here (which has the same version number!) didn't present those problems.

Instead, it gave me this error:
error.C:58:20: error: stream.h: No such file or directory
In file included from mu.h:441,
from error.C:56:

It seems that stream.h comes from the days before C++ include files didn't finish with ".h". This header file has been deprecated for some time, but it seems that with gcc 4.3.3, which I have, it is not even provided.

It turns out that GCC 4.2.2 comes with a folder called "backward", that has "stream.h" and related header files. Armed with these files (which I provide online), I was able to get Murphi to compile OK by changing one line in the makefile from:

CFLAGS = -O4 # options for g++

to

CFLAGS = -O4 -I /home/scratch/gcc4.2.2_backward/backward # options for g++

(this is where I put the "backward" files).

Happy Murphi-ing!

1 comment:

  1. my backward folder for 4.8.2 has no stream.h -- recommendations?

    ReplyDelete