Skip to content

[GUI] Configuration is not permanent

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

Setup

Open an almost empty file (not that the contents really matter):

//@ ensures \result == 0;
int main() {
    return 0;
}

Use the following command to launch the GUI: frama-c-gui -wp -wp-rte -wp-status-all -wp-par 8 almost_empty.c

Open the WP Goals tab to see one surely valid goal.

Behaviour in question

Two ways to reproduce. First with the reparse button:

  1. Click Configure and run analyses, select the -wp tickbox, and press Cancel.
  2. Click Configure and run analyses, and note that the -wp tickbox is still checked even though we pressed Cancel. Press Cancel again.
  3. Press Reparse source files, and replay analyses. The WP Goals tab still/again shows the surely valid goal.
  4. Press Reparse source files, and replay analyses. The WP Goals tab now shows nothing.

And now with the execute button.

  1. Click Configure and run analyses, select the -wp tickbox, and press Execute.
  2. The WP Goals tab still/again shows the surely valid goal.
  3. Click Configure and run analyses, and note that the -wp tickbox is not checked anymore.

Expected behaviour

  1. Configuring should be something you do once. This would include the commandline arguments. There should be no need to turn on the WP plugin again and again.
  2. The Cancel button should cancel, so NOT save the changes.
  3. The Reparse source files, and replay analyses button should not undo configuration.
  4. The Execute button should not undo configuration.
  5. There should be an additional button in the configuration dialog to save the configuration.

Actual behaviour

  1. Commandline configuration is a one time deal. Not all options are still selected after startup.
  2. The Cancel button does not actually cancel. It saves the changes and closes the dialog. It currently behaves as a Save and close button.
  3. The Reparse source files, and replay analyses button reparses, replays the analyses, and undoes configuration.
  4. The Execute button replays the analyses, and undoes configuration.

Fix ideas

The current work-around is to reconfigure each time I make a change to the source file (which is a little annoying). There are two ways to fix this:

  1. Have the buttons do exactly what they promise to do and nothing more.
  2. Change the text of the buttons to reflect the actual behaviour.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information