[WP] There is no obvious way to exit the Interactive Proof Editor (and return to the list of WP goals).
Steps to reproduce the issue
Running frama-c-gui apply WP to a function with multiple VCs and open the "WP Goals" and click on one of the VCs.
Expected behaviour
I expect to find a button or a right-click menu item which allows me to close the Interactive Proof Editor on the "current VC" and return to the List of WP Goals. (IE. I can find no way to switch from a detailed VC view back to the overall list of Goals view).
Actual behaviour
I can find no such button or right-click menu item while "inside" the Interactive Proof Editor.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 25.0-beta (Manganese)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 21.10 (Impish)
Additional information (optional)
I have found that:
-
I can switch between VCs in the Interactive Proof Editor by using the mouse to click on different ensures or asserts in the normalized code text.
-
I can recover the overall list of WP goals IF I manage to click on an ensure or assertion which is not in the "currently selected" "Not Proven (yet)" goals list... (If I have an assertion which has been proven).
Unfortunately I would like/expect a direct way to exit the Interactive Proof Editor and return to the list of WP Goals.