[wp] Infinite loop related to WP cache.
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.
- Frama-C installation mode: Opam
- Frama-C version: 21.1 (Scandium)
- Plug-in used: WP
- OS name: Ubuntu 20.04.1 LTS (Focal)
- OS version: Linux xxxxx 5.4.0-47-generic #51 (closed)-Ubuntu SMP Fri Sep 4 19:50:52 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux
Please add specific information deemed relevant with regard to this issue.
Steps to reproduce the issue
- Extract the attached zip file: pillow_src.zip
- Run the following command in the root of the extracted folder:
rm -rf .frama-c/wp/cache; frama-c-gui -verbose 5 -debug 5 -wp -wp-rte -wp-out wp_out -wp-log a:wp.log -wp-timeout 10 -wp-cache update -wp-status-all -wp-par 8 -wp-model "+cast" -wp-prover coq,cvc4,alt-ergo,z3,script,tip "-cpp-extra-args=-I .frama-c-build " libImaging/FliDecode.c
- Wait for the verification to run.
- In the file list, scroll down to
libImaging/FLIDecode.cand open it. (maybe also click on a contract in the left source pane)
Configure and run analyses.
- Activate the
Reparse source files, and replay anayses.
- The progress bar should appear and disappear right after.
- Check the
Consoletab and scroll down for the repeating messages. Example contents: console_contents.txt
- Bonus steps:
- Wait. Check out all those messages!
- Wait longer. Get bored by all the messages.
- Now click the
Consoletab contents, press
ctrl+a, and press
- If nothing happens wait for more text to appear and try again (work within a minute for me).
- The terminal states something like:
The program 'frama-c-gui' received an X Window System error. This probably reflects a bug in the program. The error was 'BadWindow (invalid Window parameter)'. (Details: serial 19490411 error_code 3 request_code 18 minor_code 0) (Note to programmers: normally, X errors are reported asynchronously; that is, you will receive the error a while after causing it. To debug your program, run it with the --sync command line option to change this behavior. You can then get a meaningful backtrace from your debugger if you break on the gdk_x_error() function.)
It is quite hard to reproduce this consistently, so let me know if I need to try harder to create a proper example.
The analyses upon opening should be executed again upon hitting the replay button. It should however be faster as most results should be cached.
The verifier goes into an infinite loop after solving a few problems.
Not sure if the bonus steps are related to Frama-C, GTK, or my WM.
I suspect the WP cache is at fault, because deleting that made the crash more consistent.
Also there might be a difference between the
Configure and run analyses +
Execute and the
Reparse source files, and replay analyses, as the program only seems to crash when running the analyses using the reparse button. Also the number of goals generally differs between the two.