--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] similar assertions not all validated



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