[Frama-C/WP] The history of internal state changes VC goal outcomes
Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: code/function-contract/contract/ex-3-alphabet-answer.c
)...
Start frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c
.
Right-click on the function prototype int alphabet_letter
and select Prove function annotations by WP
, the first VC (ensures
) should fail.
Right-click on the function prototype int alphabet_letter
a second time and select Prove function annotations by WP
, the first VC (ensures
) should succeed.
Expected behaviour
The order in which WP proof invocations should not change the VC goal outcomes if there is no change to the underlying code/annotations.
Actual behaviour
The history of WP proof invocations does seem to change the VC goal outcomes.
Contextual information
- Frama-C, Why3, Alt-Ergo installation mode: all via Opam
- Frama-C version: 25.0-beta (Manganese)
- Plug-in used: WP
- Why3 version: Why3 platform, version 1.5.0
- Alt-Ergo version: 2.4.1
- OS name: Ubuntu
- OS version: 21.10 (Impish)
- Number of CPU's: 2
- CPU speed: 2.80GHz
- RAM: 16Gb