--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp loop invariant problem




> But in the file "max_element2.c", in Line 47,
> I replace "loop invariant !(\exists integer k; 0 <= k < i && (a[max] <
> a[k]));"
> with "loop invariant IsMaximum(a, i, max);" which are the same.
> But in this case, Frama-C can not prove.

It's only a bug in Frama-C if Frama-C generates an obligation that is not provable. Did you look at the generated obligation?

It often happens that adding a layer of definition prevents automatic provers to conclude on a property that was provable when it was simple. Which automatic prover(s) did you use? 

Pascal