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
Reportersboldo 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000431: Dgraph.DGraphModel.read_dot
DescriptionHello,

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

File "src/gui/property_navigator.ml", 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...

Regards,

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: * CONFIGURE OCAML COMPILERS *
    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: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
    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: * CONFIGURE NON-MANDATORY TOOLS AND LIBRARIES *
    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/Makefile.in... yes
    aorai... yes
    checking for src/security_slicing/Makefile.in... yes
    security_slicing... yes
    checking for src/wp/Makefile.in... yes
    wp... yes
    configure: *******************************************************
    configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
    configure: *******************************************************
    checking for ltl2ba... no
    configure: WARNING: ltl2ba not found.
    plug-ins not fully functional:
      aorai
    
    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: * CHECKING FOR PLUG-IN DEPENDENCIES *
    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 +

-Relationships
+Relationships

-Notes

~0000734

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.

~0000735

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 ?

Regards,

Sylvie

~0000736

signoles (manager)

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

~0000737

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.

~0000738

signoles (manager)

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

~0000740

sboldo (reporter)

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

:-/

Sylvie

~0000741

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).

~0000743

sboldo (reporter)

It works now.

Thanks a lot!

Sylvie

~0000744

signoles (manager)

Fixed in svn release 8131.
+Notes

-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