I was trying to run through the tutorial here: https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf The first example on page 15 & 16 fails with: [wp] Running WP plugin... [wp] User Error: Prover 'alt-ergo' not found in why3.conf I couldn't get any further. What I tried was: - Install both why3 and alt-ergo. Why aren't they deps of frama-c? - Run /usr/lib64/why3/commands/why3config by hand (why isn't it in /usr/bin?), which creates $HOME/.why3.conf - stracing the program, it seems like it never attempts to open or run anything to do with alt.*ergo ~/.why3.conf contains: ---------------------------------------------------------------------- [detected_prover] exec_name = "alt-ergo" version = "2.0.0" [detected_prover] exec_name = "coqtop" version = "8.11.2" [main] default_editor = "emacs -nw %f" magic = 14 memlimit = 1000 running_provers_max = 2 timelimit = 5 ---------------------------------------------------------------------- $ rpm -q why3 frama-c alt-ergo coq why3-1.3.1-10.fc33.x86_64 frama-c-21.0-2.fc33.x86_64 alt-ergo-2.0.0-15.fc33.x86_64 coq-8.11.2-1.fc33.x86_64 Rich. -- Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones Read my programming and virtualization blog: http://rwmj.wordpress.com virt-p2v converts physical machines to virtual machines. Boot with a live CD or over the network (PXE) and turn machines into KVM guests. http://libguestfs.org/virt-v2v _______________________________________________ users mailing list -- users@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to users-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/users@xxxxxxxxxxxxxxxxxxxxxxx
