Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #40
Closed
Open
Created Oct 29, 2020 by Jens Gerlach@gerlach3 of 3 tasks completed3/3 tasks

installing Frama-C 22 beta on Ubuntu 20.04 fails

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking