[WP] save / load not saving strategies
Steps to reproduce the issue
On the attached examples : test.c
running the following command
frama-c test.c -wp -wp-prover=tip -wp-prop post
works perfectly, but when we use the save / load features with the following command (and after removing the existing scripts)
frama-c test.c -save tmp.sav ; frama-c -load tmp.sav -wp -wp-prover=tip -wp-prop post
it does not work anymore and, when we add option
-wp-strategy InstanceForall
,
Frama-C outputs
[wp] Warning: Invalid -wp-strategy 'InstanceForall' (undefined strategy name)
Expected behaviour
We would expect save / load to keep strategies available.
Actual behaviour
Strategies seems to not be correctly saved / loaded and when specified, they are declared undefined
by WP.
Contextual information
- Frama-C installation mode: opam install frama-c.28.0
- Frama-C version: 28.0
- Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 20.04
FYI: @nkosmatov