--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems proving bubble_sort



Hello,
 First I would like to thank you for your recent answers, today I have
another problem.
Recently I am trying to prove a bubble_sort function similar to the min_sort
function given in your documentation.

Proving this was no problem with the Lithium version.
But due to some changes, I cannot prove a safety relatet VC with Beryllium.

I would like you to test the appended algorithm and help me to understand
why the pointer relatet VC could not be solved.

I also would like you to help me to find out, why the one permutation
assertion fails.

And finally I would appreciate a hint, why it is so difficult to prove the
whole thing using assings clauses.

In the current version I have put them into comments, otherwise a
computation of the rest would fail.

I hope that is not too much at once.

Best wishes,


Christoph
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 7342 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091015/7c7c1f48/attachment.bin