Hi all,
I’m using SLED11SP2 with gnome, for my work purpose, i was trying to install Frama-C. But due to some dependency problem, i failed to do this. Main dependency is lablGTK2 (for GUI).
Can someone please help me for this.
Hi
A home user on OBS has it packaged;
https://build.opensuse.org/package/show?project=home:Friseer:openSUSE&package=lablgtk2
http://download.opensuse.org/repositories/home:/Friseer:/openSUSE/GNOME_Apps_SLE_11_SP1/
–
Cheers Malcolm °¿° (Linux Counter #276890)
SUSE Linux Enterprise Desktop 11 (x86_64) Kernel 3.0.13-0.27-default
up 10:58, 2 users, load average: 0.01, 0.02, 0.05
CPU Intel i5 CPU M520@2.40GHz | Intel Arrandale GPU
Hi Malcolm,
Thanks for your help, but Frama-c didn’t enable GUI as because it didn’t detect any lablgtk2 package on my system.
Hi
So you installed the lablgtk2 from that repository ok?
Then you installed Frama-C, but the GUI never started? If so, can you
open a terminal and run the command to start Frama-C and post the error.
–
Cheers Malcolm °¿° (Linux Counter #276890)
SUSE Linux Enterprise Desktop 11 (x86_64) Kernel 3.0.13-0.27-default
up 14:16, 2 users, load average: 0.05, 0.07, 0.06
CPU Intel i5 CPU M520@2.40GHz | Intel Arrandale GPU
Hi Malcolm,
When i configuring the ocaml-3.12.1
it shows the following message
"The “labltk” library: not supported
** Objective Caml configuration completed successfully **"
But it successfully install
After i was trying to configure frama-c, & it was ok & successfully but gui not enabled, due to lablgtk2
naren_bishayee@linux-nxk1:~/Documents/Download/Frama-C/frama-c-Nitrogen-20111001> ./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 3.12.1: 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… no
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph… no
checking for ocamlgraph.tar.gz… yes
configure: unarchiving ocamlgraph.tar.gz
configure: configuring ocamlgraph…
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled
configure: ******************************************
configure: * CONFIGURE OPTIONAL 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 (2341.176 cycles per us)
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/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 why… no
checking for why-dp… no
checking for alt-ergo… no
./configure: line 7877: alt-ergo: command not found
configure: alt-ergo version is .
configure: alt-ergo’s array theory unsupported.
checking for coqc… no
configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
checking for /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa… no
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: WARNING: why not found
configure: WARNING: wp partially enabled because why missing.
configure: WARNING: why-dp not found
configure: WARNING: wp partially enabled because why-dp missing.
configure: WARNING: alt-ergo not found
configure: WARNING: wp partially enabled because alt-ergo missing.
configure: WARNING: coq not found
configure: WARNING: wp partially enabled because coqc missing.
configure: WARNING: lablgtk2/lablgtk.cmxa not found.
configure: WARNING: gui disabled because /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa missing.
configure: WARNING: impact only partially enabled because gui not enabled.
configure: WARNING: metrics only partially enabled because gui not enabled.
configure: WARNING: occurrence only partially enabled because gui not enabled.
configure: WARNING: scope only partially enabled because gui not enabled.
configure: WARNING: slicing only partially enabled because gui not enabled.
configure: WARNING: syntactic_callgraph only partially enabled because gui not enabled.
configure: WARNING: value_analysis only partially enabled because gui not enabled.
configure: WARNING: security_slicing only partially enabled because gui not enabled.
configure: WARNING: wp partially enabled because gui not enabled.
configure: *********************
configure: * CREATING MAKEFILE *
configure: *********************
configure: creating ./config.status
config.status: creating src/aorai/Makefile
config.status: creating src/report/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: semantic_constant_folding: yes
configure: from_analysis: yes
configure: gui: no, /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa missing
configure: impact: partial, gui not enabled
configure: inout: yes
configure: metrics: partial, gui not enabled
configure: occurrence: partial, gui not enabled
configure: pdg: yes
configure: postdominators: yes
configure: rte_annotation: yes
configure: scope: partial, gui not enabled
configure: semantic_callgraph: yes
configure: slicing: partial, gui not enabled
configure: sparecode: yes
configure: syntactic_callgraph: partial, gui not enabled
configure: users: yes
configure: value_analysis: partial, gui not enabled
configure: aorai: partial, dynamic, ltl2ba missing
configure: report: yes, dynamic
configure: security_slicing: partial, dynamic, gui not enabled
configure: wp: partial, dynamic, gui not enabled
naren_bishayee@linux-nxk1:~/Documents/Download/Frama-C/frama-c-Nitrogen-20111001>
Hi
The location needs to be added for it to find the files, see the error
configure: gui: no, /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa missingYou need to set a configure option or manually modify the makefile;
../configure --help
or
../configure --prefix=/usrThe location from the installed rpm should put it
in /usr/lib{64}/ocaml/lablgtk2.
–
Cheers Malcolm °¿° (Linux Counter #276890)
openSUSE 12.1 (x86_64) Kernel 3.1.9-1.4-desktop
up 18:53, 3 users, load average: 0.04, 0.04, 0.05
CPU Intel i5 CPU M520@2.40GHz | Intel Arrandale GPU
Hi malcolm,
When i configure ocaml using “./configure” i found the following lines for labltk
Configuring LablTk…
tcl.h and/or tk.h not found.
Configuration failed, LablTk will not be built.
BFD library not found, ‘objinfo’ will be unable to display info on .cmxs files
** Configuration summary **
Directories where Objective Caml will be installed:
binaries… /usr/bin
standard library… /usr/lib/ocaml
manual pages… /usr/man (with extension .1)
Configuration for the bytecode compiler:
C compiler used… gcc
options for compiling… -fno-defer-pop -Wall -D_FILE_OFFSET_BITS=64 -D_REENTRANT
options for linking… -Wl,-E -lm -ldl -lncurses -lpthread
shared libraries are supported
options for compiling… -fPIC -fno-defer-pop -Wall -D_FILE_OFFSET_BITS=64 -D_REENTRANT
command for building… gcc -shared -o lib.so -Wl,-rpath,/a/path objs
Configuration for the native-code compiler:
hardware architecture… i386
OS variant… linux_elf
C compiler used… gcc
options for compiling… -Wall -D_FILE_OFFSET_BITS=64 -D_REENTRANT
options for linking… -lm
assembler … as
preprocessed assembler … gcc -c
native dynlink … true
profiling with gprof … supported
Source-level replay debugger: supported
Additional libraries supported:
unix str num dynlink bigarray systhreads threads graph
Configuration for the “num” library:
target architecture … ia32 (asm level 2)
Configuration for the “graph” library:
options for compiling …
options for linking … -lX11
The “labltk” library: not supported
** Objective Caml configuration completed successfully **
naren_bishayee@linux-nxk1:~/Documents/Download/Frama-C/ocaml-3.12.1>
And i also tried to configure frama-C using --prefix=/usr, but same result
I also search the lablgtk2 directory, and i found it under /usr/lib/ocaml/lablgtk2,
After i copy using cp -r /usr/lib/ocaml/lablgtk2/ /usr/local/lib/ocaml/lablgtk2/
After i again configure the frama-c & it shows the following line
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: report: yes, dynamic
configure: security_slicing: yes, dynamic
configure: wp: partial, dynamic, coqc missing
naren_bishayee@linux-nxk1:~/Documents/Download/Frama-C/frama-c-Nitrogen-20111001>
Next i type make, and display the following lines
ocamlopt.opt -I src -I lib -a -o graph.cmxa graph.cmx
ocamlc.opt -c -I src -I lib -g -dtypes -I +lablgtk2 -I view_graph -I src -I lib -I . -I +lablgtk2 -I view_graph -I src -I lib -I . view_graph/viewGraph_core.mli
File “view_graph/viewGraph_core.mli”, line 1, characters 0-1:
Error: /usr/local/lib/ocaml/lablgtk2/gnoCanvas.cmi
is not a compiled interface
make[1]: *** [view_graph/viewGraph_core.cmi] Error 2
make[1]: Leaving directory `/home/naren_bishayee/Documents/Download/Frama-C/frama-c-Nitrogen-20111001/ocamlgraph’
make: *** [lib/graph.cmi] Error 2
linux-nxk1:/home/naren_bishayee/Documents/Download/Frama-C/frama-c-Nitrogen-20111001 #
Hi Malcolm,
Please help me, this application is very important for me, please.
Hi
Will try an have a further look today 
–
Cheers Malcolm °¿° (Linux Counter #276890)
openSUSE 12.1 (x86_64) Kernel 3.1.10-1.9-desktop
up 10:38, 4 users, load average: 0.01, 0.03, 0.05
CPU Intel i5 CPU M520@2.40GHz | Intel Arrandale GPU