--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on May 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Installing Frama-c from https://git.frama-c.com/pub/frama-c.git



Hello,

Feeling somewhat adventurous I tried to install Frama-C from the public git repository.

I used the following steps for a clean install under xubuntu-19.10 after removing .opam

opam init --yes --comp=4.06.1
opam install --yes depext
opam depext frama-c
opam pin add frama-c https://git.frama-c.com/pub/frama-c.git
 
Unfortunately, I received the error message below.
What should I do to be able to install Frama-C from this source?
A followup question is: What is the relationship between Frama-C 20.0 (released in December 2019) and this git version?
Is it closer to Frama-C 21 or Frama-C 20?

Regards

Jens 

#=== ERROR while compiling frama-c.20.0 =======================================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.06.1 | pinned(git+https://git.frama-c.com/pub/frama-c.git#92419510)
# path        ~/.opam/4.06.1/.opam-switch/build/frama-c.20.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/frama-c-14780-e4db2f.env
# output-file ~/.opam/log/frama-c-14780-e4db2f.out
### output ###
# [...]
# Ocamlc       src/plugins/wp/cfgWP.cmi
# Ocamlopt     src/kernel_internals/parsing/logic_lexer.cmx
# Ocamlc       src/plugins/wp/TacSplit.cmo
# Ocamlc       src/plugins/wp/TacChoice.cmo
# Ocamlc       src/plugins/wp/TacRange.cmo
# Ocamlc       src/plugins/wp/TacArray.cmo
# Ocamlc       src/plugins/wp/TacCompound.cmo
# Ocamlc       src/plugins/wp/TacUnfold.cmo
# File "src/plugins/wp/ProverWhy3.ml", line 259, characters 31-47:
# Error: Unbound value const_of_big_int
# make: *** [share/Makefile.generic:78: src/plugins/wp/ProverWhy3.cmo] Error 2
# make: *** Waiting for unfinished jobs....