"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?
ID0000614: This issue was created automatically from Mantis Issue 614. Further discussion may take place here.
|ID0000614||Frama-C||Plug-in > jessie||public||2010-10-22||2010-10-22|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||-|
See attached program. Jessie generates the proof obligation "(FORALL (int_P_alloc_table) (IMPLIES TRUE (<= (offset_min int_P_alloc_table aaa) 0)))" for the assert in line 8, and a similar one for offset_max. Neither of them can be proved by any automatic prover.
I guess, the reason is that the name "aaa" appears unbound in the conclusions of both obligations, but does not appear anywhere else in the file ftest1_why.sx, so nothing is known (by the provers) about it.
If I make "aaa" a local rather than a global variable, the generated proof obligations look completely different; I feel unable to summarize the differences.