0
我試圖從Ubuntu 14.04的源代碼安裝frama-c，但這是不可能的。在Ubuntu 14.04從源代碼安裝Frama-c鈉/氟
氟使錯誤：
[email protected]:~/Área de Trabalho/frama-c-Fluorine-20130601$ make
Generating src/lib/dynlink_common_interface.ml
Generating src/kernel/config.ml
Generating ptests/ptests_config.ml
Generating share/Makefile.kernel
Generating .depend
Ocamlc src/lib/dynlink_common_interface.cmo
Ocamlc src/kernel/config.cmo
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] Erro 2
鈉做出錯誤：
Makefile:2456: aviso: ignorando comandos antigos para o alvo `de'
Ocamlopt src/gui/property_navigator.cmx
ocamlopt.opt: don't know what to do with de.
Usage: ocamlopt <options> <files>
Options are:
-ffast-math Inline trigonometric and exponential functions
-a Build a library
-absname Show absolute filenames in error messages
-annot Save information in <filename>.annot
-bin-annot Save typedtree in <filename>.cmt
-c Compile only (do not link)
-cc <command> Use <command> as the C compiler and linker
-cclib <opt> Pass option <opt> to the C linker
-ccopt <opt> Pass option <opt> to the C compiler and linker
-compact Optimize code size rather than speed
-config Print configuration values and exit
-dtypes (deprecated) same as -annot
-for-pack <ident> Generate code that can later be `packed' with
ocamlopt -pack -o <ident>.cmx
-g Record debugging information for exception backtrace
-i Print inferred interface
-I <dir> Add <dir> to the list of include directories
-impl <file> Compile <file> as a .ml file
-inline <n> Set aggressiveness of inlining to <n>
-intf <file> Compile <file> as a .mli file
-intf-suffix <string> Suffix for interface files (default: .mli)
-labels Use commuting label mode
-linkall Link all modules, even unused ones
-no-app-funct Deactivate applicative functors
-noassert Do not compile assertion checks
-noautolink Do not automatically link C libraries specified in .cmxa files
-nodynlink Enable optimizations for code that will not be dynlinked
-nolabels Ignore non-optional labels in types
-nostdlib Do not add default directory to the list of include directories
-o <file> Set output file name to <file>
-output-obj Output a C object file instead of an executable
-p Compile and link with profiling support for "gprof"
(not supported on all platforms)
-pack Package the given .cmx files into one .cmx
-pp <command> Pipe sources through preprocessor <command>
-ppx <command> Pipe abstract syntax trees through preprocessor <command>
-principal Check principality of type inference
-rectypes Allow arbitrary recursive types
-runtime-variant <str> Use the <str> variant of the run-time system
-S Keep intermediate assembly file
-shared Produce a dynlinkable plugin
-short-paths Shorten paths in types
-strict-sequence Left-hand part of a sequence must have type unit
-thread Generate code that supports the system threads library
-unsafe Do not compile bounds checking on array and string access
-v Print compiler version and location of standard library and exit
-verbose Print calls to external commands
-version Print version and exit
-vnum Print version number and exit
-w <list> Enable or disable warnings according to <list>:
+<spec> enable warnings in <spec>
-<spec> disable warnings in <spec>
@<spec> enable warnings in <spec> and treat them as errors
<spec> can be:
<num> a single warning number
<num1>..<num2> a range of consecutive warning numbers
<letter> a predefined set
default setting is "+a-4-6-7-9-27-29-32..39-41..42-44-45"
-warn-error <list> Enable or disable error status for warnings according
to <list>. See option -w for the syntax of <list>.
Default setting is "-a"
-warn-help Show description of warning numbers
-where Print location of standard library and exit
-nopervasives (undocumented)
-dsource (undocumented)
-dparsetree (undocumented)
-dtypedtree (undocumented)
-drawlambda (undocumented)
-dlambda (undocumented)
-dclambda (undocumented)
-dcmm (undocumented)
-dsel (undocumented)
-dcombine (undocumented)
-dlive (undocumented)
-dspill (undocumented)
-dsplit (undocumented)
-dinterf (undocumented)
-dprefer (undocumented)
-dalloc (undocumented)
-dreload (undocumented)
-dscheduling (undocumented)
-dlinear (undocumented)
-dstartup (undocumented)
- <file> Treat <file> as a file name (even if it starts with `-')
-help Display this list of options
--help Display this list of options
make: ** [src/gui/property_navigator.cmx] Erro 2
您可以發佈與編譯鈉，當你得到錯誤'LC_ALL = C = VERBOSEMAKE是make'（'LC_ALL'是沒有必要的，但用英文而不是葡萄牙語'make'警告可能會得到更好的答案）？另外，請注意，安裝Frama-C的首選方式是通過opam（https://opam.ocaml.org） – Virgile 2015-04-02 15:13:38