--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on April 2012 ---
On 04/17/2012 03:42 PM, David MENTRE wrote: > Why on your initial code the loop invariants where proven valid? My > guess is that the invalid invariant or an unproven assertion was used > as hypothesis to prove the remaining VCs. But I let Frama-C experts > explain the precise reason. This is precisely the reason. Although, with the WP plug-in, the status will not be "valid", but "valid in a context which was not proven valid", which is more precise. Jessie unfortunately does not make the difference. > My advice would be to avoid using assertions. As they are taken as > hypothesis for following code, wrong assertions can lead to prove > incorrect logic annotations. Better is to write correct annotations > that are proved progressively, one line after the other. Assertions can be very useful. A better advice could be: look at the first unproved VC and fix it, before looking at the VC that come after. - Claude