Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marche) · Fri, 03 Apr 2015 17:45:44 +0200

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                    |

Frama-C-discuss mailing list archives

[Frama-c-discuss] [Why-discuss] Install why3, why, frama-c and jessie on ubuntu 14.04