--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2009 ---
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