Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000431Frama-CKernelpublic2010-04-13 15:33
Assigned Tosignoles 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000431: Dgraph.DGraphModel.read_dot

I try to compile the latest svn version (8087) but I can't. I have the following message:

File "src/gui/", line 50, characters 18-45:
Error: Unbound value Dgraph.DGraphModel.read_dot
make: *** [src/gui/property_navigator.cmo] Error 2

What my .configure gives is as attached file.
Probably a Makefile problem...


Sylvie Boldo

TagsNo tags attached.
Attached Files
  • ? file icon toto (4,889 bytes) 2010-03-19 16:24 -
    configure: ******************
    configure: * CONFIGURE MAKE *
    configure: ******************
    checking for make... make
    make version is GNU Make 3.81: Good!
    configure: *****************************
    configure: *****************************
    checking for ocamlc... ocamlc
    ocaml version is 3.11.1: Good!
    ocaml library path is /usr/lib/ocaml
    checking for ocamlopt... ocamlopt
    checking ocamlopt version and standard library... ok
    checking for ocamlc.opt... no
    checking for ocamlopt.opt... no
    configure: *******************************************
    configure: *******************************************
    checking for ocamldep... ocamldep
    checking for ocamldep.opt... no
    checking for ocamllex... ocamllex
    checking for ocamllex.opt... no
    checking for ocamlyacc... ocamlyacc
    checking for /usr/lib/ocaml/ocamlgraph... yes
    configure: ocamlgraph 1.3 is incompatible with Frama-C. Will switch to a local version.
    configure: Switching to local ocamlgraph
    checking for ocamlgraph... yes
    checking for ocamlgraph.tar.gz... yes
    checking for ocamlgraph/Makefile... yes
    configure: ***********************************************
    configure: ***********************************************
    checking for ocamldoc... ocamldoc
    checking for ocamlmktop... ocamlmktop
    checking for otags... no
    configure: **********************
    configure: * CONFIGURE PLATFORM *
    configure: **********************
    checking platform... Unix
    checking whether performance counters are usable... ok (3242.857 cycles per us)
    configure: ***************************
    configure: * WISHED FRAMA-C PLUG-INS *
    configure: ***************************
    checking for src/constant_propagation... yes
    constant_propagation... yes
    checking for src/from... yes
    from... 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... 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... yes
    checking for src/aorai/ yes
    aorai... yes
    checking for src/security_slicing/ yes
    security_slicing... yes
    checking for src/wp/ yes
    wp... yes
    configure: *******************************************************
    configure: *******************************************************
    checking for ltl2ba... no
    configure: WARNING: ltl2ba not found.
    plug-ins not fully functional:
    checking for why... yes
    checking for alt-ergo... yes
    checking for /usr/lib/ocaml/lablgtk2/lablgtk.cmxa... yes
    checking for /usr/lib/ocaml/lablgtk2/lablgtksourceview2.cmxa... yes
    checking for /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa... no
    configure: WARNING: lablgnomecanvas.cmxa not found
    plug-ins not fully functional:
      syntactic_callgraph wp
    checking for dot... yes
    checking for /usr/lib/ocaml/dynlink.cmxa... yes
    checking for lablgtk2's custom tree model... yes
    configure: *************************************
    configure: *************************************
    configure: *********************
    configure: * CREATING MAKEFILE *
    configure: *********************
    configure: creating ./config.status
    config.status: creating src/aorai/Makefile
    config.status: creating src/security_slicing/Makefile
    config.status: creating src/wp/Makefile
    config.status: creating cil/ocamlutil/perfcount.c
    config.status: creating share/Makefile.config
    configure: *******************************
    configure: * SUMMARY: PLUG-INS AVAILABLE *
    configure: *******************************
    configure: constant_propagation: yes
    configure: from: yes
    configure: gui: yes
    configure: impact: yes
    configure: inout: yes
    configure: metrics: yes
    configure: occurrence: yes
    configure: pdg: yes
    configure: postdominators: yes
    configure: rte: yes
    configure: scope: yes
    configure: semantic_callgraph: yes
    configure: slicing: yes
    configure: sparecode: yes
    configure: syntactic_callgraph: partial (see warning about /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa)
    configure: users: yes
    configure: value: yes
    configure: aorai: partial, dynamic (see warning about ltl2ba)
    configure: security_slicing: yes, dynamic
    configure: wp: partial, dynamic (see warning about /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa)
    ? file icon toto (4,889 bytes) 2010-03-19 16:24 +




signoles (manager)

Hello Sylvie,

The result of your configure looks quite good :).
Try to do 'make rebuild'.
If any error occurs, please give me the output of this command.


sboldo (reporter)

An error did occur, but not the same ^^

Ocamlc src/kernel/boot.cmo
make[1]: *** No rule to make target `src/buckx/mybigarray.o', needed by `bin/toplevel.byte'. Stop.
make: *** [rebuild] Error 2

BTW, am I supposed to update Frama-C or absolutely not ?




signoles (manager)

This error is a true Makefile bug.
Will investigate as soon as possible...


signoles (manager)

Workaround: just type 'make' works. Don't know what is the issue with "make rebuild".

BTW update Frama-C if you want. The current svn version is not known as broken.


signoles (manager)

svn release r8130 fixes this issue.
Could you please confirm that your problem is solved?


sboldo (reporter)

'make' gives the same error about Dgraph.DGraphModel.read_dot
'make rebuild' also gives the same error




signoles (manager)

Found the difference between our configurations. You haven't lablgnomecanvas on your system.

Since a quite recent change, the Frama-C GUI (not gwhy though) now requires lablgnomecanvas. That was not checked by configure nor documented. This is now fixed.

Please do:
$ svn up
$ rm -rf autom4te.cache
$ autoconf
$ ./configure
$ make

Are you able to compile now?

If you want to compile the Frama-C GUI, please install lablgnomecanvas (for Ubuntu: sudo apt-get install liblablgtk2-gnome-ocaml-dev).


sboldo (reporter)

It works now.

Thanks a lot!



signoles (manager)

Fixed in svn release 8131.

-Issue History
Date Modified Username Field Change
2010-03-19 16:24 sboldo New Issue
2010-03-19 16:24 sboldo File Added: toto
2010-03-23 15:03 signoles Status new => assigned
2010-03-23 15:03 signoles Assigned To => signoles
2010-03-23 15:14 signoles Note Added: 0000734
2010-03-23 15:14 signoles Status assigned => feedback
2010-03-24 09:51 sboldo Note Added: 0000735
2010-03-24 09:59 signoles Note Added: 0000736
2010-03-24 09:59 signoles Status feedback => confirmed
2010-03-24 10:10 signoles Note Added: 0000737
2010-03-24 11:11 signoles Note Added: 0000738
2010-03-24 11:11 signoles Status confirmed => feedback
2010-03-24 11:29 sboldo Note Added: 0000740
2010-03-24 13:29 signoles Note Added: 0000741
2010-03-24 15:34 sboldo Note Added: 0000743
2010-03-24 16:25 signoles Note Added: 0000744
2010-03-24 16:25 signoles Status feedback => resolved
2010-03-24 16:25 signoles Fixed in Version => Frama-C svn, precise the release id
2010-03-24 16:25 signoles Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version Frama-C svn, precise the release id => Frama-C Boron
+Issue History