--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2015 ---
Since the error is in the compilation of Frama-C, you message should be sent to Frama-C list instead. In the first case, please try to execute VERBOSEMAKE=yes make to see more details In the second case: it is surprising that opam wants to install Frama-C 20130601 and not the most recent 20150201. Are you sure your opam is up to date ? try opam update - Claude Le 03/04/2015 16:42, Allberson Dantas a ?crit : > Hi everyone, > > Has someone already installed them on ubuntu 14.04? > > From the sources, I have installed why3 and why, but not Frama-c, > neither Sodium, nor Fluorine. Here comes Sodium error: > > Copying to src/lib/integer.ml <http://integer.ml> > Generating src/lib/dynlink_common_interface.ml > <http://dynlink_common_interface.ml> > Ocamllex cil/src/frontc/clexer.ml <http://clexer.ml> > 376 states, 4398 transitions, table size 19848 bytes > 3299 additional bytes used for bindings > Ocamlyacc cil/src/frontc/cparser.ml <http://cparser.ml> > 1 shift/reduce conflict. > Ocamllex cil/src/logic/logic_lexer.ml <http://logic_lexer.ml> > 145 states, 1840 transitions, table size 8230 bytes > 1915 additional bytes used for bindings > Ocamlyacc cil/src/logic/logic_parser.ml <http://logic_parser.ml> > Ocamllex cil/src/logic/logic_preprocess.ml <http://logic_preprocess.ml> > 116 states, 558 transitions, table size 2928 bytes > 2007 additional bytes used for bindings > Generating src/kernel/config.ml <http://config.ml> > Generating src/kernel/frama_c_config.ml <http://frama_c_config.ml> > Generating share/frama-c.rc > Generating share/Makefile.dynamic_config > Generating share/Makefile.kernel > 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 > > > > From opam, only why3 installs. Here goes the frama-c error in opam: > > The following actions will be performed: > - install frama-c.20130601 > 1 to install | 0 to reinstall | 0 to upgrade | 0 to downgrade | 0 to remove > > =-=-= Installing frama-c.20130601 =-=-= > Applying 4.01-compat.patch. > Building frama-c.20130601: > ./configure --prefix /home/hpe/.opam/4.01.0 > --sbindir=/home/hpe/.opam/4.01.0/lib/frama-c/sbin > --libexecdir=/home/hpe/.opam/4.01.0/lib/frama-c/libexec > --sysconfdir=/home/hpe/.opam/4.01.0/lib/frama-c/etc > --sharedstatedir=/home/hpe/.opam/4.01.0/lib/frama-c/com > --localstatedir=/home/hpe/.opam/4.01.0/lib/frama-c/var > --libdir=/home/hpe/.opam/4.01.0/lib/frama-c/lib > --includedir=/home/hpe/.opam/4.01.0/lib/frama-c/include > --datarootdir=/home/hpe/.opam/4.01.0/lib/frama-c/share > make > make install > [ERROR] The compilation of frama-c.20130601 failed. > Removing frama-c.20130601. > > > ===== ERROR while installing frama-c.20130601 ===== > # opam-version 1.1.1 > # os linux > # command make > # path /home/hpe/.opam/4.01.0/build/frama-c.20130601 > # compiler 4.01.0 > # exit-code 2 > # env-file > /home/hpe/.opam/4.01.0/build/frama-c.20130601/frama-c-2935-6d07ae.env > # stdout-file > /home/hpe/.opam/4.01.0/build/frama-c.20130601/frama-c-2935-6d07ae.out > # stderr-file > /home/hpe/.opam/4.01.0/build/frama-c.20130601/frama-c-2935-6d07ae.err > ### stdout ### > # ...[truncated] > # Ocamlc src/misc/bit_utils.cmi > # Ocamlc src/misc/bit_utils.cmo > # Ocamlc src/lib/setWithNearest.cmi > # Ocamlc src/ai/ival.cmi > # Ocamlc src/ai/lattice_Interval_Set.cmi > # Ocamlc src/ai/lattice_Interval_Set.cmo > # Ocamlc src/misc/subst.cmi > # Ocamlc src/misc/subst.cmo > # Ocamlc src/misc/service_graph.cmi > # Ocamlc src/misc/service_graph.cmo > ### stderr ### > # ...[truncated] > # Warning 41: Division_by_zero belongs to several types: alarm exn > # The first one was selected. Please disambiguate if this is wrong. > # File "src/kernel/alarms.ml <http://alarms.ml>", line 349, characters 4-20: > # Warning 41: Division_by_zero belongs to several types: alarm exn > # The first one was selected. Please disambiguate if this is wrong. > # File "src/kernel/messages.ml <http://messages.ml>", line 27, > characters 7-15: > # Warning 45: this open statement shadows the constructor Failure (which > is later used) > # File "src/misc/service_graph.ml <http://service_graph.ml>", line 301, > characters 8-193: > # Error: Some record fields are undefined: sg_parent > # make: ** [src/misc/service_graph.cmo] Erro 2 > > > > -- > Allberson Dantas > > [Doutorando em Ci?ncia da Computa??o - UFC] > [Analista de Sistemas do Serpro - Servi?o Federal de Processamento de Dados] > > > _______________________________________________ > Why-discuss mailing list > Why-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss > -- Claude March? | tel: +33 1 69 15 66 08 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |