Skip to content

frama-c-gui frozen and why3 not found

Problem Description

When running opam install alt-ergo, my terminal shows:

Package alt-ergo is already installed (current version is 2.4.2).

However, when running frama-c-gui -wp -rte -main.c, the terminal shows:

(frama-c-gui:4023): GLib-CRITICAL **: 09:36:25.664: Source ID 8 was not found when attempting to remove it. 

The GUI is opened but frozen. No clicking is responded and the console shows User Error: Prover 'alt-ergo' not found in why3.conf.

Steps to reproduce the issue

frama-c-gui -wp -rte -main.c

Expected behaviour

open the window of frama-c-gui and run normally

Actual behaviour

The GUI is opened but frozen. No clicking is responded and the console shows User Error: Prover 'alt-ergo' not found in why3.conf.

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: frama-c.26.1
  • Plug-in used: Plug-in used
  • OS name: Ubuntu
  • OS version: 22.04.2 LTS

Additional information (optional)

After running "opam upgrade", the following information appears:

Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).

The following packages are not being upgraded because the new versions conflict with other installed packages:

  - ocaml-config.3

  - ocplib-simplex.0.5

    ∗ alt-ergo-lib.2.4.2 is installed and requires ocplib-simplex (>= 0.4 & < 0.5)

  - why3.1.6.0

    ∗ frama-c.26.1 is installed and requires why3 (>= 1.5.1 & < 1.6~)

However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.

Nothing to do.

# Run eval $(opam env) to update the current shell environment
Edited by Andre Maroneze
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information