Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] [Why-discuss] Install why3, why, frama-c and jessie on ubuntu 14.04
- Subject: [Frama-c-discuss] [Why-discuss] Install why3, why, frama-c and jessie on ubuntu 14.04
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Fri, 03 Apr 2015 17:45:44 +0200
- In-reply-to: <CADH2bc8yddxe4oAa5_d2DX=CaqR06S_93KruDWyTWXvkDUfg9w@mail.gmail.com>
- References: <CADH2bc8yddxe4oAa5_d2DX=CaqR06S_93KruDWyTWXvkDUfg9w@mail.gmail.com>
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 |
- Prev by Date: [Frama-c-discuss] existential variables in ACSL spec in Frama-C/WP Sodium
- Next by Date: [Frama-c-discuss] Last Call for Papers, PxTP 2015
- Previous by thread: [Frama-c-discuss] existential variables in ACSL spec in Frama-C/WP Sodium
- Next by thread: [Frama-c-discuss] Last Call for Papers, PxTP 2015
- Index(es):