[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:
- Click
Configure and run analyses
, select the-wp
tickbox, and pressCancel
. - Click
Configure and run analyses
, and note that the-wp
tickbox is still checked even though we pressedCancel
. PressCancel
again. - Press
Reparse source files, and replay analyses
. TheWP Goals
tab still/again shows the surely valid goal. - Press
Reparse source files, and replay analyses
. TheWP Goals
tab now shows nothing.
And now with the execute button.
- Click
Configure and run analyses
, select the-wp
tickbox, and pressExecute
. - The
WP Goals
tab still/again shows the surely valid goal. - Click
Configure and run analyses
, and note that the-wp
tickbox is not checked anymore.
Expected behaviour
- 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.
- The
Cancel
button should cancel, so NOT save the changes. - The
Reparse source files, and replay analyses
button should not undo configuration. - The
Execute
button should not undo configuration. - There should be an additional button in the configuration dialog to save the configuration.
Actual behaviour
- Commandline configuration is a one time deal. Not all options are still selected after startup.
- The
Cancel
button does not actually cancel. It saves the changes and closes the dialog. It currently behaves as aSave and close
button. - The
Reparse source files, and replay analyses
button reparses, replays the analyses, and undoes configuration. - 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:
- Have the buttons do exactly what they promise to do and nothing more.
- Change the text of the buttons to reflect the actual behaviour.