GitLab

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.

Contextual information

• 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.c and open it. (maybe also click on a contract in the left source pane)
• Click Configure and run analyses.
• Activate the WP plugin.
• Click Cancel.
• Click Reparse source files, and replay anayses.
• The progress bar should appear and disappear right after.
• Check the Console tab 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 Console tab contents, press ctrl+a, and press ctrl+c.
  • 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.

Expected behaviour

The analyses upon opening should be executed again upon hitting the replay button. It should however be faster as most results should be cached.

Actual behaviour

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.

Fix ideas

None, sorry.

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.