I am trying to install the latest version of frama-c(Fluorine 3) in mac os x 10.9. Using brew i was able to fill the prerequisites of frama-c(Gtk, GtkSourceView, GnomeCanvas and Lablgtk2)
The result from the config file is the following:
$ ./configure
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 3.81: Good!
configure: *****************************
configure: * CONFIGURE OCAML COMPILERS *
configure: *****************************
checking for ocamlc... ocamlc
OCaml version is 4.01.0: good!
ocaml library path is /usr/local/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version and standard library... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version and standard library... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version and standard library... ok
configure: *******************************************
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
configure: *******************************************
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for /usr/local/lib/ocaml/ocamlgraph/graph.cmx... yes
configure: OcamlGraph 1.8.3 found: great!
configure: ******************************************
configure: * CONFIGURE OPTIONAL TOOLS AND LIBRARIES *
configure: ******************************************
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
checking for ocamlmktop... ocamlmktop
checking for ocamlcp... ocamlcp
checking for otags... no
checking for ocamlfind... ocamlfind
OCamlfind detected and enabled
checking for /Users/me/.opam/system/lib/zarith/zarith.cmxa... no
configure: WARNING: Zarith not found: will use the default less efficient library instead
configure: **********************
configure: * CONFIGURE PLATFORM *
configure: **********************
checking platform... Unix
Default preprocessor is gcc -C -E -I..
configure: ***************************
configure: * WISHED FRAMA-C PLUG-INS *
configure: ***************************
checking for src/constant_propagation... yes
semantic_constant_folding... yes
checking for src/from... yes
from_analysis... yes
checking for src/gui... yes
gui... yes
checking for src/impact... yes
impact... yes
checking for src/inout... yes
inout... yes
checking for src/metrics... yes
metrics... yes
checking for src/occurrence... yes
occurrence... yes
checking for src/pdg... yes
pdg... yes
checking for src/postdominators... yes
postdominators... yes
checking for src/rte... yes
rte_annotation... yes
checking for src/scope... yes
scope... yes
checking for src/semantic_callgraph... yes
semantic_callgraph... yes
checking for src/slicing... yes
slicing... yes
checking for src/sparecode... yes
sparecode... yes
checking for src/syntactic_callgraph... yes
syntactic_callgraph... yes
checking for src/users... yes
users... yes
checking for src/value... yes
value_analysis... yes
checking for src/aorai/Makefile.in... yes
aorai... yes
checking for ltl2ba... no
checking for src/obfuscator/Makefile.in... yes
obfuscator... yes
checking for src/report/Makefile.in... yes
report... yes
checking for src/security_slicing/Makefile.in... yes
security_slicing... yes
checking for src/wp/Makefile.in... yes
wp... yes
checking for coqc... no
configure: rerun configure to make wp using coq 8.4
configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
ocamlfind: Package `lablgtk2' not found
Ocamlfind -> using +lablgtk2.(,/usr/local/lib/ocaml/lablgtk2)
checking for /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa... yes
checking for /usr/local/lib/ocaml/lablgtk2/lablgtksourceview2.cmxa... yes
checking for /usr/local/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa... yes
checking for dot... yes
checking for /usr/local/lib/ocaml/dynlink.cmxa... yes
native dynlink works fine. Great.
configure: *************************************
configure: * CHECKING FOR PLUG-IN DEPENDENCIES *
configure: *************************************
configure: WARNING: ltl2ba not found.
configure: WARNING: aorai partially enabled because ltl2ba missing.
configure: *********************
configure: * CREATING MAKEFILE *
configure: *********************
configure: creating ./config.status
config.status: creating src/aorai/Makefile
config.status: creating src/obfuscator/Makefile
config.status: creating src/report/Makefile
config.status: creating src/security_slicing/Makefile
config.status: creating src/wp/Makefile
config.status: creating share/Makefile.config
configure: *******************************
configure: * SUMMARY: PLUG-INS AVAILABLE *
configure: *******************************
configure: semantic_constant_folding: yes
configure: from_analysis: yes
configure: gui: yes
configure: impact: yes
configure: inout: yes
configure: metrics: yes
configure: occurrence: yes
configure: pdg: yes
configure: postdominators: yes
configure: rte_annotation: yes
configure: scope: yes
configure: semantic_callgraph: yes
configure: slicing: yes
configure: sparecode: yes
configure: syntactic_callgraph: yes
configure: users: yes
configure: value_analysis: yes
configure: aorai: partial, dynamic, ltl2ba missing
configure: obfuscator: yes, dynamic
configure: report: yes, dynamic
configure: security_slicing: yes, dynamic
configure: wp: yes, dynamic
It seems to fill all the necessary prerequisites. But when running make i get the following error:
Ocamlc src/ai/abstract_interp.cmi
File "src/ai/abstract_interp.mli", line 166, characters 4-33:
Error: In this `with' constraint, the new definition of O
does not match its original definition in the constrained signature:
...
The field `find' is required but not provided
make: *** [src/ai/abstract_interp.cmi] Error 2
Can anyone tell me what i am doing wrong?
Frama-C Fluorine 3 is not compatible with OCaml 4.01. The Opam package of Frama-C contains the necessary patch at https://github.com/ocaml/opam-repository/blob/master/packages/frama-c/frama-c.20130601/files/4.01-compat.patch. You might also want to try Opam for installing OCaml software (as far as I know, Opam has support for Mac OS X).