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] Installing Frama-c from https://git.frama-c.com/pub/frama-c.git

  • Subject: [Frama-c-discuss] Installing Frama-c from https://git.frama-c.com/pub/frama-c.git
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Fri, 1 May 2020 09:31:10 +0000
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....