Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Frama-C unbound module Z build error

Tags:

ocaml

frama-c

Using Ubuntu 14.04, I downloaded the Neon Frama-C distribution, and installed the required tools: labgtk, sourceview, etc. I configured Frama-C no problem, but on building got:

File "external/unz.ml", line 39, characters 10-19:
Error: Unbound module Z
make: *** [external/unz.cmo] Error 2

The problem is

 let n = Z.of_bits str in

where Z denotes a module that is not imported (I guess). I do not know what Z is supposed to refer to so I have no way of trying to fix this.

like image 440
Jonathan Gallagher Avatar asked Mar 19 '23 12:03

Jonathan Gallagher


1 Answers

Have you installed the zarith library (libzarith-ocaml-dev under Ubuntu)? Frama-C can use two libraries for arbitrary precision integers: either Bignum, which is included in OCaml distribution (although I wouldn't be surprised that Debian/Ubuntu did manage to make it a separate package ), or Zarith, a newer, more efficient implementation. unz.ml is part of the code that binds Zarith to Frama-C, thus if you don't have Zarithinstalled, you will have some issues compiling it.

Normally, ./configure should take care of choosing the appropriate library. You can check what it has found in config.log. A possible issue is that you have package libzarith-ocaml installed but not libzarith-ocaml-dev. In this case, the library itself is installed (and presumably detected by ./configure), but not the headers needed to compile the code against it.

like image 76
Virgile Avatar answered Mar 27 '23 23:03

Virgile