GitLab

Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information.

Before submitting the issue, please confirm (by adding a X in the [ ]):

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our BTS;
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: Frama-C version (as reported by frama-c -version) https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz
• Plug-in used: Plug-in used
• OS name: Xubuntu
• OS version: 20.04

Please add specific information deemed relevant with regard to this issue.

When installing Frama-C 22 (beta) I received the following error message

[ERROR] The compilation of frama-c failed at "/home/jens/.opam/opam-init/hooks/sandbox.sh build
        make -j7".

#=== ERROR while compiling frama-c.22.0-beta ==================================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.1 | pinned(https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz)
# path        ~/.opam/4.09.1/.opam-switch/build/frama-c.22.0-beta
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code   2
# env-file    ~/.opam/log/frama-c-1555-de8c6b.env
# output-file ~/.opam/log/frama-c-1555-de8c6b.out
### output ###
# [...]
# Ocamlopt     src/kernel_services/ast_data/alarms.cmx
# Ocamlopt     src/kernel_services/ast_data/statuses_by_call.cmx
# Ocamlopt     src/plugins/gui/gui_printers.cmx
# Ocamlopt     src/plugins/e-acsl/tests/print.cmx
# File "./src/plugins/wp/share/coqwp/Vlist.v", line 403, characters 8-11:
# Error:
# In nested Ltac calls to "lia" and "xlia (tactic)", last call failed.
# Tactic failure:  Cannot find witness.
# 
# Coqc         src/plugins/wp/share/coqwp/ArcTrigo.v
# make: *** [src/plugins/wp/share/Makefile.coqwp:39: src/plugins/wp/share/coqwp/Vlist.vo] Error 1
# make: *** Waiting for unfinished jobs....

Steps to reproduce the issue

Please indicate here steps to follow to get a minimal, complete, and verifiable example which reproduces the issue.

Here are my installation steps:

• opam init --yes --comp=4.09.1
• opam install --yes depext
• opam depext --yes frama-c
• opam install --yes alt-ergo why3
• opam install --yes why3-coq
• opam pin add --yes https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz

The final step failed with the message shown above