--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on July 2013 ---
Hello, I contact you because I can't manage to prove all the ensures clauses of the function in the attached file. What is happening is that I can only prove the ensures clauses about the last affection, even if I change the order of the three instructions. When I try to prove the others ensures clauses by WP, alt-Ergo fails and detects a syntax error in a file generated by frama-c. So I would like to know if there is a problem in my function that prevents frama-c from doing its job and how I can fix it, or if the problem comes from frama-c. Thank you for yours answers, Best regards Alice Tailliar -------------- next part -------------- A non-text attachment was scrubbed... Name: ranged_value.c Type: text/x-csrc Size: 609 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130711/e94318d3/attachment.c>