WP ignores some goal
ID0001588: This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.
|ID0001588||Frama-C||Plug-in > wp||public||2013-12-20||2014-03-13|
|Priority||normal||Severity||major||Reproducibility||have not tried|
|Product Version||Frama-C Fluorine-20130601||Target Version||-||Fixed in Version||Frama-C Neon-20140301|
On this example, WP ignore some of the goals. There should be 3 goals, but :
[wp] 1 goal scheduled [wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid
Loop invariant preservation and assertion are ignore.
Additional Information :
I simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
Steps To Reproduce :
frama-c wp.c -wp