2017-06-04 224 views
3

我試圖在Ubuntu 17.04(Zesty)上從repository(6aa64)安裝Frama-C gui Phosphorus。 Frama-C opam可以很好地工作,但是據我所知,它缺少GUI +我可能稍後想要修補frama-C,所以我希望能夠自己編譯它。ocamlfind:在Ubuntu上找不到包「lablgtk2.gnomecanvas」17.04

第一步:

./configure --enable-gui --enable-verbosemake 

生成輸出:

configure: ****************** 
configure: * CONFIGURE MAKE * 
configure: ****************** 
checking for make... make 
checking version of make... 4.1 
configure: ***************************** 
configure: * CONFIGURE OCAML COMPILERS * 
configure: ***************************** 
checking for ocamlc... ocamlc 
checking version of OCaml... 4.02.3 
checking OCaml library path... /usr/lib/ocaml 
checking for ocamlopt... ocamlopt 
checking ocamlopt version and standard library... ok 
checking for ocamlfind... ocamlfind 
configure: Distribution mode: all warnings are deactivated 
configure: ******************************************* 
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES * 
configure: ******************************************* 
checking for ocamldep... ocamldep 
checking for ocamllex... ocamllex 
checking for ocamllex.opt... ocamllex.opt 
checking for ocamlyacc... ocamlyacc 
checking for ocamlcp... ocamlcp 
checking for ocamlgraph... found 
checking for zarith... found 
configure: ****************************************** 
configure: * CONFIGURE OPTIONAL TOOLS AND LIBRARIES * 
configure: ****************************************** 
checking for ocamldoc... ocamldoc 
checking for ocamlmktop... ocamlmktop 
checking for otags... no 
checking for Apron... not found. The corresponding domains won't be available in Eva 
checking for Landmarks... not found. 
configure: ********************** 
configure: * CONFIGURE PLATFORM * 
configure: ********************** 
checking platform... Unix 
checking OCaml native threads... ok. 
checking for gcc... gcc 
checking whether the C compiler works... yes 
checking for C compiler default output file name... a.out 
checking for suffix of executables... 
checking whether we are cross compiling... no 
checking for suffix of object files... o 
checking whether we are using the GNU C compiler... yes 
checking whether gcc accepts -g... yes 
checking for gcc option to accept ISO C89... none needed 
checking how to run the C preprocessor... gcc -E 
checking for grep that handles long lines and -e... /bin/grep 
checking for egrep... /bin/grep -E 
checking for ANSI C header files... yes 
checking for sys/types.h... yes 
checking for sys/stat.h... yes 
checking for stdlib.h... yes 
checking for string.h... yes 
checking for memory.h... yes 
checking for strings.h... yes 
checking for inttypes.h... yes 
checking for stdint.h... yes 
checking for unistd.h... yes 
checking for stdlib.h... (cached) yes 
checking assert.h usability... yes 
checking assert.h presence... yes 
checking for assert.h... yes 
checking float.h usability... yes 
checking float.h presence... yes 
checking for float.h... yes 
checking math.h usability... yes 
checking math.h presence... yes 
checking for math.h... yes 
checking signal.h usability... yes 
checking signal.h presence... yes 
checking for signal.h... yes 
checking for unistd.h... (cached) yes 
checking how to run the C preprocessor... gcc -E 
/* Check whether comments are kept in output */ 
Default preprocessor is 'gcc -E -C -I.'. 
Default preprocessor supported architecture-related options: \"-m32\"; \"-m64\"; \"-m16\"; 
configure: *************************** 
configure: * WISHED FRAMA-C PLUG-INS * 
configure: *************************** 
checking for src/plugins/callgraph... yes 
callgraph... yes 
checking for src/plugins/constant_propagation... yes 
semantic_constant_folding... yes 
checking for src/plugins/from... yes 
from_analysis... yes 
checking for src/plugins/gui... yes 
gui... yes 
checking for src/plugins/impact... yes 
impact... yes 
checking for src/plugins/inout... yes 
inout... yes 
checking for src/plugins/metrics... yes 
metrics... yes 
checking for src/plugins/occurrence... yes 
occurrence... yes 
checking for src/plugins/pdg... yes 
pdg... yes 
checking for src/plugins/postdominators... yes 
postdominators... yes 
checking for src/plugins/rte... yes 
rtegen... yes 
checking for src/plugins/scope... yes 
scope... yes 
checking for src/plugins/slicing... yes 
slicing... yes 
checking for src/plugins/sparecode... yes 
sparecode... yes 
checking for src/plugins/users... yes 
users... yes 
checking for src/plugins/value... yes 
value_analysis... yes 
checking for src/plugins/aorai/Makefile.in... yes 
aorai... yes 
checking for ltl2ba... no 
checking for src/plugins/e-acsl/Makefile.in... yes 
e_acsl... yes 
checking for uname... uname 
checking stdio.h usability... yes 
checking stdio.h presence... yes 
checking for stdio.h... yes 
checking for doxygen... doxygen 
checking for dot... yes 
configure: creating ./config.status 
config.status: creating src/plugins/e-acsl/doc/doxygen/doxygen.cfg 
config.status: executing default commands 
configure: Configure libjemalloc 
autoconf 
./configure --enable-autogen --with-jemalloc-prefix=__e_acsl_native_ --with-private-namespace=__e_acsl_hidden_ 
checking for xsltproc... /usr/bin/xsltproc 
checking for gcc... gcc 
checking whether the C compiler works... yes 
checking for C compiler default output file name... a.out 
checking for suffix of executables... 
checking whether we are cross compiling... no 
checking for suffix of object files... o 
checking whether we are using the GNU C compiler... yes 
checking whether gcc accepts -g... yes 
checking for gcc option to accept ISO C89... none needed 
checking whether compiler supports -std=gnu99... yes 
checking whether compiler supports -Wall... yes 
checking whether compiler supports -Werror=declaration-after-statement... yes 
checking whether compiler supports -Wshorten-64-to-32... no 
checking whether compiler supports -Wsign-compare... yes 
checking whether compiler supports -pipe... yes 
checking whether compiler supports -g3... yes 
checking how to run the C preprocessor... gcc -E 
checking for grep that handles long lines and -e... /bin/grep 
checking for egrep... /bin/grep -E 
checking for ANSI C header files... yes 
checking for sys/types.h... yes 
checking for sys/stat.h... yes 
checking for stdlib.h... yes 
checking for string.h... yes 
checking for memory.h... yes 
checking for strings.h... yes 
checking for inttypes.h... yes 
checking for stdint.h... yes 
checking for unistd.h... yes 
checking whether byte ordering is bigendian... no 
checking size of void *... 8 
checking size of int... 4 
checking size of long... 8 
checking size of long long... 8 
checking size of intmax_t... 8 
checking build system type... x86_64-unknown-linux-gnu 
checking host system type... x86_64-unknown-linux-gnu 
checking whether pause instruction is compilable... yes 
checking for ar... ar 
checking malloc.h usability... yes 
checking malloc.h presence... yes 
checking for malloc.h... yes 
checking whether malloc_usable_size definition can use const argument... no 
checking whether __attribute__ syntax is compilable... yes 
checking whether compiler supports -fvisibility=hidden... yes 
checking whether compiler supports -Werror... yes 
checking whether tls_model attribute is compilable... yes 
checking whether compiler supports -Werror... yes 
checking whether alloc_size attribute is compilable... yes 
checking whether compiler supports -Werror... yes 
checking whether format(gnu_printf, ...) attribute is compilable... yes 
checking whether compiler supports -Werror... yes 
checking whether format(printf, ...) attribute is compilable... yes 
checking for a BSD-compatible install... /usr/bin/install -c 
checking for ranlib... ranlib 
checking for ld... /usr/bin/ld 
checking for autoconf... /usr/bin/autoconf 
checking for memalign... yes 
checking for valloc... yes 
checking whether compiler supports -O3... yes 
checking whether compiler supports -funroll-loops... yes 
checking configured backtracing method... N/A 
checking for sbrk... yes 
checking whether utrace(2) is compilable... no 
checking whether valgrind is compilable... yes 
checking whether a program using __builtin_ffsl is compilable... yes 
checking LG_PAGE... 12 
checking pthread.h usability... yes 
checking pthread.h presence... yes 
checking for pthread.h... yes 
checking for pthread_create in -lpthread... yes 
checking for library containing clock_gettime... none required 
checking for secure_getenv... yes 
checking for issetugid... no 
checking for _malloc_thread_cleanup... no 
checking for _pthread_mutex_init_calloc_cb... no 
checking for TLS... yes 
checking whether C11 atomics is compilable... no 
checking whether atomic(9) is compilable... no 
checking whether Darwin OSAtomic*() is compilable... no 
checking whether madvise(2) is compilable... yes 
checking whether to force 32-bit __sync_{add,sub}_and_fetch()... no 
checking whether to force 64-bit __sync_{add,sub}_and_fetch()... no 
checking for __builtin_clz... yes 
checking whether Darwin OSSpin*() is compilable... no 
checking whether glibc malloc hook is compilable... yes 
checking whether glibc memalign hook is compilable... yes 
checking whether pthreads adaptive mutexes is compilable... yes 
checking for stdbool.h that conforms to C99... yes 
checking for _Bool... yes 
configure: creating ./config.status 
config.status: creating Makefile 
config.status: creating jemalloc.pc 
config.status: creating doc/html.xsl 
config.status: creating doc/manpages.xsl 
config.status: creating doc/jemalloc.xml 
config.status: creating include/jemalloc/jemalloc_macros.h 
config.status: creating include/jemalloc/jemalloc_protos.h 
config.status: creating include/jemalloc/jemalloc_typedefs.h 
config.status: creating include/jemalloc/internal/jemalloc_internal.h 
config.status: creating test/test.sh 
config.status: creating test/include/test/jemalloc_test.h 
config.status: creating config.stamp 
config.status: creating bin/jemalloc-config 
config.status: creating bin/jemalloc.sh 
config.status: creating bin/jeprof 
config.status: creating include/jemalloc/jemalloc_defs.h 
config.status: include/jemalloc/jemalloc_defs.h is unchanged 
config.status: creating include/jemalloc/internal/jemalloc_internal_defs.h 
config.status: include/jemalloc/internal/jemalloc_internal_defs.h is unchanged 
config.status: creating test/include/test/jemalloc_test_defs.h 
config.status: test/include/test/jemalloc_test_defs.h is unchanged 
config.status: executing include/jemalloc/internal/private_namespace.h commands 
config.status: executing include/jemalloc/internal/private_unnamespace.h commands 
config.status: executing include/jemalloc/internal/public_symbols.txt commands 
config.status: executing include/jemalloc/internal/public_namespace.h commands 
config.status: executing include/jemalloc/internal/public_unnamespace.h commands 
config.status: executing include/jemalloc/internal/size_classes.h commands 
config.status: executing include/jemalloc/jemalloc_protos_jet.h commands 
config.status: executing include/jemalloc/jemalloc_rename.h commands 
config.status: executing include/jemalloc/jemalloc_mangle.h commands 
config.status: executing include/jemalloc/jemalloc_mangle_jet.h commands 
config.status: executing include/jemalloc/jemalloc.h commands 
checking for src/plugins/loop_analysis/Makefile.in... yes 
loop_analysis... yes 
checking for src/plugins/nonterm/Makefile.in... yes 
nonterm... yes 
checking for src/plugins/obfuscator/Makefile.in... yes 
obfuscator... yes 
checking for src/plugins/print_api... yes 
print_api... yes 
checking for src/plugins/report/Makefile.in... yes 
report... yes 
checking for src/plugins/security_slicing/Makefile.in... yes 
security_slicing... yes 
checking for src/plugins/variadic/Makefile.in... yes 
variadic... yes 
checking for src/plugins/wp/Makefile.in... yes 
wp... yes 
configure: ******************************************************* 
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS * 
configure: ******************************************************* 
Ocamlfind -> using +lablgtk2.(/usr/lib/ocaml/lablgtk2,/usr/lib/ocaml/lablgtk2) 
checking for /usr/lib/ocaml/lablgtk2/lablgtksourceview2.cmxa... yes 
checking for /usr/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa... yes 
checking for /usr/lib/ocaml/lablgtk2/lablgtk.cmxa... yes 
checking for dot... 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. 
checking for coqc... yes 
unsupported coqc version 8.6 
configure: ********************* 
configure: * CREATING MAKEFILE * 
configure: ********************* 
configure: creating ./config.status 
config.status: creating src/plugins/e-acsl/doc/doxygen/doxygen.cfg 
config.status: creating src/plugins/e-acsl/Makefile 
config.status: creating src/plugins/loop_analysis/Makefile 
config.status: creating src/plugins/nonterm/Makefile 
config.status: creating src/plugins/obfuscator/Makefile 
config.status: creating src/plugins/report/Makefile 
config.status: creating src/plugins/variadic/Makefile 
config.status: creating src/plugins/aorai/Makefile 
config.status: creating src/plugins/security_slicing/Makefile 
config.status: creating src/plugins/wp/Makefile 
config.status: creating share/Makefile.config 
config.status: executing default commands 
configure: ******************************* 
configure: * SUMMARY: PLUG-INS AVAILABLE * 
configure: ******************************* 
configure: callgraph: yes, dynamic 
configure: semantic_constant_folding: yes, dynamic 
configure: from_analysis: yes, dynamic 
configure: gui: yes 
configure: impact: yes, dynamic 
configure: inout: yes, dynamic 
configure: metrics: yes, dynamic 
configure: occurrence: yes, dynamic 
configure: pdg: yes, dynamic 
configure: postdominators: yes, dynamic 
configure: rtegen: yes, dynamic 
configure: scope: yes, dynamic 
configure: slicing: yes, dynamic 
configure: sparecode: yes, dynamic 
configure: users: yes, dynamic 
configure: value_analysis: yes, dynamic 
configure: aorai: partial, dynamic, ltl2ba missing 
configure: e_acsl: yes, dynamic 
configure: loop_analysis: yes, dynamic 
configure: nonterm: yes, dynamic 
configure: obfuscator: yes, dynamic 
configure: print_api: yes, dynamic 
configure: report: yes, dynamic 
configure: security_slicing: yes, dynamic 
configure: variadic: yes, dynamic 
configure: wp: yes, dynamic 

......這一次我運行make在結束了:

ocamlfind ocamlc -c -package findlib -package ocamlgraph -package num -package unix -package str -package dynlink -package bytes -package zarith -w -a -bin-annot -strict-sequence -safe-string -g -I src/plugins/slicing_types -I src/plugins/pdg_types -I src/plugins/value_types -I src/libraries/stdlib -I src/libraries/utils -I src/libraries/project -I src/libraries/datatype -I src/kernel_internals/parsing -I src/kernel_internals/typing -I src/kernel_internals/runtime -I src/kernel_services/parsetree -I src/kernel_services/ast_data -I src/kernel_services/ast_queries -I src/kernel_services/ast_printing -I src/kernel_services/cmdline_parameters -I src/kernel_services/plugin_entry_points -I src/kernel_services/abstract_interp -I src/kernel_services/visitors -I src/kernel_services/analysis -I src/kernel_services/ast_transformations -I src/plugins/gui -I /home/teto/framac/lib/plugins -I src/plugins/security_slicing -I /home/teto/framac/lib/plugins -package findlib -package ocamlgraph -package num -package unix -package str -package dynlink -package bytes -package zarith -w -a -bin-annot -strict-sequence -safe-string -g -I /home/teto/framac/src/plugins/slicing_types -I /home/teto/framac/src/plugins/pdg_types -I /home/teto/framac/src/plugins/value_types -I /home/teto/framac/src/libraries/stdlib -I /home/teto/framac/src/libraries/utils -I /home/teto/framac/src/libraries/project -I /home/teto/framac/src/libraries/datatype -I /home/teto/framac/src/kernel_internals/parsing -I /home/teto/framac/src/kernel_internals/typing -I /home/teto/framac/src/kernel_internals/runtime -I /home/teto/framac/src/kernel_services/parsetree -I /home/teto/framac/src/kernel_services/ast_data -I /home/teto/framac/src/kernel_services/ast_queries -I /home/teto/framac/src/kernel_services/ast_printing -I /home/teto/framac/src/kernel_services/cmdline_parameters -I /home/teto/framac/src/kernel_services/plugin_entry_points -I /home/teto/framac/src/kernel_services/abstract_interp -I /home/teto/framac/src/kernel_services/visitors -I /home/teto/framac/src/kernel_services/analysis -I /home/teto/framac/src/kernel_services/ast_transformations -I /home/teto/framac/src/plugins/gui -I /home/teto/framac/lib -package lablgtk2 -package lablgtk2.gnomecanvas -package lablgtk2.sourceview2 src/plugins/security_slicing/security_slicing_parameters.mli 
ocamlfind: Package `lablgtk2.gnomecanvas' not found 

我有libgnomecanvas2(*)安裝。這裏已經提到這個問題沒有解決方案: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2017-January/005200.html

我對ocaml瞭解不多,但似乎應該在/usr/lib/ocaml/lablgtk2/中找到gnomecanvas。我上傳這個文件夾的列表,如果它能夠幫助這裏https://transfer.sh/4lQol/listing(太大SO)

問候 馬特

+0

嘗試重新安裝lablgtk2並檢查安裝是否找到libgnomecanvas2。 – camlspotter

回答

4

出於某種原因(我們的郵資-C隊,不太懂) Debian偏離了上游的Labgltk2--因此Ubuntu軟件包也是如此。在這兩種發行版中,gnomecanvas的OCamlfind包稱爲lablgtk2-gnome.gnomecanvas,而不僅僅是lablgtk2.gnomecanvas。您可以相應地修補Frama-c的來源,但我建議您改爲執行Opam安裝。這將使事情變得更簡單。

+0

確實下面的補丁作品謝謝! diff -git a/share/Makefile.config.in b/share/Makefile.config.in index 31a8a9bd..353a60be 100644 --- a/share/Makefile.config.in +++ b/share /Makefile.config.in @@ -176,7 +176,7 @@ LIBRARY_NAMES + =地標landmarks.ppx ENDIF ifneq($(ENABLE_GUI),無) -LIBRARY_NAMES_GUI = lablgtk2 lablgtk2.gnomecanvas lablgtk2.sourceview2 + LIBRARY_NAMES_GUI = lablgtk2 lablgtk2-gnome.gnomecanvas lablgtk2.sourceview2 否則 LIBRARY_NAMES_GUI = ENDIF 我怎樣才能實現與OPAM GUI安裝的? – mattator

+0

在Opam中,您有兩個軟件包:'frama-c'和'frama-c-base'。 'frama-c'應該強制安裝GUI。 – byako

+0

Opam沒有安裝gui,可能是因爲ubuntu的packlages干擾。不過,該補丁已應用於此分支https://github.com/teto/Frama-C-snapshot/tree/ubuntu_fix – mattator