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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2548

Closed
Open
Created Mar 30, 2021 by Qix@Qix-1 of 3 tasks completed1/3 tasks

Error: Unbound value Why3.Whyconf.load_default_config_if_needed

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 old BTS (note: the old BTS is deprecated); (Can't tell; getting a database connection error)
  • you installed Frama-C as prescribed in the instructions. (Not exactly; I'm building from source within a Dockerfile)

Contextual information

  • Frama-C installation mode: from source
  • Frama-C version: c4d10fb9
  • Plug-in used: WP
  • OS name: Debian Buster
  • OS version: 20210326 (10.8)

Steps to reproduce the issue

Dockerfile:

FROM debian:buster-20210326 AS base

RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time

RUN cc --version
RUN c++ --version

WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect

ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo

Expected behaviour

Should build to completion.

Actual behaviour

File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 |       let config = Why3.Whyconf.load_default_config_if_needed config in
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2

Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the __fc_xxx.h headers directly.

I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.

However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get any verification to work.

Anyway this is the latest issue I've hit trying to get everything up to date.

Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.

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