Bug 2249607
| Summary: | frama-c - Empty list of plugins | ||
|---|---|---|---|
| Product: | [Fedora] Fedora | Reporter: | Christophe GRENIER <grenier> |
| Component: | frama-c | Assignee: | Jerry James <loganjerry> |
| Status: | CLOSED ERRATA | QA Contact: | Fedora Extras Quality Assurance <extras-qa> |
| Severity: | high | Docs Contact: | |
| Priority: | unspecified | ||
| Version: | 39 | CC: | Andre.MARONEZE, loganjerry |
| Target Milestone: | --- | ||
| Target Release: | --- | ||
| Hardware: | x86_64 | ||
| OS: | Linux | ||
| Whiteboard: | |||
| Fixed In Version: | frama-c-27.1-5.fc39 | Doc Type: | If docs needed, set a value |
| Doc Text: | Story Points: | --- | |
| Clone Of: | Environment: | ||
| Last Closed: | 2023-11-23 01:23:52 UTC | Type: | --- |
| Regression: | --- | Mount Type: | --- |
| Documentation: | --- | CRM: | |
| Verified Versions: | Category: | --- | |
| oVirt Team: | --- | RHEL 7.3 requirements from Atomic Host: | |
| Cloudforms Team: | --- | Target Upstream Version: | |
| Embargoed: | |||
Thank you for the bug report, Christophe. We have always had to use a workaround to convince frama-c to install where we want it to go. It looks like our workaround broke in the most recent version. I have found a simpler way to resolve the issue and have fixed Rawhide. I will do the Fedora 39 builds next. It would be great if you could test them when they are ready and see if you find any other problems. FEDORA-2023-317ab4f66a has been submitted as an update to Fedora 39. https://bodhi.fedoraproject.org/updates/FEDORA-2023-317ab4f66a FEDORA-2023-317ab4f66a has been pushed to the Fedora 39 testing repository. Soon you'll be able to install the update with the following command: `sudo dnf upgrade --enablerepo=updates-testing --refresh --advisory=FEDORA-2023-317ab4f66a` You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2023-317ab4f66a See also https://fedoraproject.org/wiki/QA:Updates_Testing for more information on how to test updates. FEDORA-2023-317ab4f66a has been pushed to the Fedora 39 stable repository. If problem still persists, please make note of it in this bug report. |
I have updated from Fedora 38 to 39, so frama-c-26.1-2.fc38.x86_64 has been replaced by frama-c-27.1-4.fc39.x86_64 frama-c plugins aren't recognized anymore. $ frama-c -eva [kernel] User Error: option `-eva' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted: invalid user input. Reproducible: Always Steps to Reproduce: 1. frama-c -plugins Actual Results: Empty list Expected Results: Aorai verification of behavioral properties (experimental) (-aorai-h) Callgraph automatically compute the callgraph of the program. Using Eva might improve the precision of this plug-in (-cg-h) Dive An interactive imprecision graph generator for Eva. (-dive-h) Dominators Compute postdominators of statements (-dominators-h) E-ACSL Executable ANSI/ISO C Specification Language --- runtime assertion checker generator (-e-acsl-h) Eva automatically computes variation domains for the variables of the program (-eva-h) ... du -sBM /usr/lib64/ocaml/frama-c-eva 103M /usr/lib64/ocaml/frama-c-eva strace -e file frama-c -plugins execve("/usr/bin/frama-c", ["frama-c", "-plugins"], 0x7ffe1a143bc8 /* 75 vars */) = 0 access("/etc/ld.so.preload", R_OK) = -1 ENOENT (No such file or directory) openat(AT_FDCWD, "/etc/ld.so.cache", O_RDONLY|O_CLOEXEC) = 3 newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=224723, ...}, AT_EMPTY_PATH) = 0 openat(AT_FDCWD, "/lib64/libm.so.6", O_RDONLY|O_CLOEXEC) = 3 newfstatat(3, "", {st_mode=S_IFREG|0755, st_size=931288, ...}, AT_EMPTY_PATH) = 0 openat(AT_FDCWD, "/lib64/libyaml-0.so.2", O_RDONLY|O_CLOEXEC) = 3 newfstatat(3, "", {st_mode=S_IFREG|0755, st_size=131840, ...}, AT_EMPTY_PATH) = 0 openat(AT_FDCWD, "/lib64/libgmp.so.10", O_RDONLY|O_CLOEXEC) = 3 newfstatat(3, "", {st_mode=S_IFREG|0755, st_size=678152, ...}, AT_EMPTY_PATH) = 0 openat(AT_FDCWD, "/lib64/libc.so.6", O_RDONLY|O_CLOEXEC) = 3 newfstatat(3, "", {st_mode=S_IFREG|0755, st_size=2250400, ...}, AT_EMPTY_PATH) = 0 readlink("/proc/self/exe", "/usr/bin/frama-c", 256) = 16 newfstatat(AT_FDCWD, "/usr/bin/frama-c", {st_mode=S_IFREG|0755, st_size=43491032, ...}, 0) = 0 newfstatat(AT_FDCWD, "/usr/lib/frama-c/plugins", 0x7ffc40cc69b0, 0) = -1 ENOENT (No such file or directory) +++ exited with 0 +++ It looks like frama-c doesn't search for its plugins in the correct directory and stops. Workaround: # install -d -m 0755 /usr/lib/frama-c # ln -s /usr/lib64/ocaml/frama-c/plugins /usr/lib/frama-c/plugins